Cardinal interpolation functions are polynomials of the stated degrees

For $k\mathrm{\ne }j$, strict ordering of the nodes gives $x_j-x_k\mathrm{\ne }0$. The denominator product in $w_j$ is nonzero by [F6], so its inverse $w_j$ exists and is nonzero by [F5]. List the omitted-node indices in increasing order and put $P_j(X)={\prod }_{k\mathrm{\ne }j}(X-x_k)$; [F2] makes this a monic formal polynomial of degree $n$. For an arbitrary real $x$, apply [F7] to the real numerators $x-x_k$ and denominators $x_j-x_k$ in that list. It gives ${\mathrm{\ell }}_j(x)=P_j(x)\mathrm{/}{\prod }_{k\mathrm{\ne }j}(x_j-x_k)=w_j{P}_j(x)$, also when $n=0$ by the empty-product convention. Scale the coefficient list $(a_0,\dots ,a_n)$ of $P_j$ by $w_j$; the resulting vector has final coefficient $w_j\mathrm{\ne }0$. By [F3] and [F4] it represents a formal polynomial of degree $n$, and [F8] gives its evaluation $w_j{P}_j(x)={\mathrm{\ell }}_j(x)$ for every real $x$.

If $i=j$, each factor in ${\mathrm{\ell }}_j(x_i)$ is $d\mathrm{/}d=1$ for a nonzero difference $d=x_j-x_k$. Induction [F13] on the list length shows their product is $1$: the empty product is $1$, and appending a factor $1$ leaves it unchanged by [F12] and the field identity [F5]. This includes the empty list. If $i\mathrm{\ne }j$, the omitted-node list contains $x_i$: its index is $i$ when $i<j$ and $i-1$ when $i>j$. The corresponding quotient factor is $0$ because its numerator is $x_i-x_i=0$, its denominator is nonzero, and [F11] gives $0$ times its inverse equal to $0$. Splitting the finite product before and after that factor by [F10] writes ${\mathrm{\ell }}_j(x_i)$ as a prefix product times $0$ times a suffix product, which is $0$ by commutativity [F5] and [F11].

The product lemma [F2] applied to $x_0,\dots ,x_n$ gives a monic polynomial of degree $n+1$ evaluating to ${\omega }_n$, with degree and leading coefficient understood from the formal list [F4].

If $x$ differs from every node, each factor $x-x_j$ is nonzero by [F5], so the product lemma [F6] gives ${\omega }_n(x)\mathrm{\ne }0$.

For each $j$, let $(a_{j,0},\dots ,a_{j,n})$ be the coefficient vector of the degree-$n$ representative from step 1.1. Define $b_k={\sum }_{j<n+1}{y}_j{a}_{j,k}$ for $k<n+1$. For every real $x$, finite-sum scaling [F8], field distributivity, and double-sum interchange [F9] give ${\sum }_{k<n+1}{b}_k{x}^k={\sum }_{k<n+1}{\sum }_{j<n+1}{y}_j{a}_{j,k}{x}^k={\sum }_{j<n+1}{y}_j{\sum }_{k<n+1}{a}_{j,k}{x}^k={\sum }_{j<n+1}{y}_j{\mathrm{\ell }}_j(x)=I_{n}y(x)\mathrm{.}$ The vector $(b_0,\dots ,b_n)$ therefore gives, by [F3], a formal polynomial of degree at most $n$ evaluating to $I_{n}y$.