Existence and uniqueness of the cardinal-polynomial interpolant

By [F2], choose a formal polynomial $P$ of degree at most $n$ (allowing the zero polynomial) whose evaluation $p(t):=P(t)$ equals the function $I_{n}y(t)$ for every real $t$. At node $x_i$, [F1, F2] give $P(x_i)=p(x_i)={\sum }_{j=0}^n{y}_j{\mathrm{\ell }}_j(x_i)=y_i$. Thus the formal polynomial $P$ is an interpolant.

Let $Q$ be any formal polynomial of degree at most $n$ (allowing zero) with $Q(x_i)=y_i$, and denote its evaluation by $q(t):=Q(t)$. Extend the actual coefficient lists of $P$ and $Q$ by zeros through index $n$ (using all-zero vectors for zero polynomials), obtaining vectors $(a_k)$ and $(b_k)$; these describe their evaluations $p$ and $q$, not padded formal objects. The vector $c_k=a_k-b_k$ defines by [F3] a formal polynomial $r$ of degree at most $n$; [F5] gives $r(t)=p(t)-q(t)$ for every real $t$. Since $p$ and $q$ agree at all nodes by step 1.1 and the choice of $q$, $r$ has the $n+1$ distinct roots $x_0,\dots ,x_n$. If $r$ were nonzero, [F4] would give at most $\mathrm{deg}r\le n$ roots, a contradiction. Hence $r$ is the zero formal polynomial; by [F3], every $a_k-b_k=0$. The canonical coefficient lists of $P$ and $Q$ are therefore identical (or both objects are zero), so $P=Q$, and consequently $p=q$ as evaluation functions.

This proves that the interpolant from step 1.1 is the unique formal polynomial of degree at most $n$ satisfying the node values.