Solution (source code)

= Solution

The <Lagrange interpolation polynomial> constructs existence explicitly:
$$
\ell_j(x)=\prod_{\substack{0\leq k\leq n\\k\ne j}}\frac{x-x_k}{x_j-x_k},\qquad p(x)=\sum_{j=0}^n f_j\ell_j(x).
$$
Distinct nodes make every denominator nonzero, and $\ell_j(x_k)=\delta_{jk}$, so $p(x_k)=f_k$ and $p$ has degree at most $n$. If two such <polynomials> existed, their difference would have degree at most $n$ but at least $n+1$ distinct roots. The root bound for a nonzero <polynomial> forces that difference to vanish. Thus \b[the interpolating <polynomial> exists and is unique].