unique polynomial with degree n for n+1 many values

Let \(K\) be a field and \((x_i,y_i) \in K\) be \(n+1\) many pairs wiht \(x_i \neq x_j\) for \(i \neq j\).
Then there exists a unique polynomial \(f \in K[X]_{\leq n}\) with degree at most \(n\) such that \(f(x_i) = y_i\)

consider the evaluation homomorphism for polynomial rings

\begin{align*} \mathrm{ev}_{(x_i)}: K[X]_{\leq n} \rightarrow& K^{n+1} \\ f \mapsto& (f(x_i))_{i} \end{align*}

It is a vectorspace-homomorphism between vector spaces of the same dimension, namely \(\mathrm{dim}(K^{n+1}) = \mathrm{dim}(K[X]_{\leq n}) = n+1\) (todo).

We want to show that \(\mathrm{ev}_{(x_i)}\) is a Bijection, so using since both vector spaces have the same finite dimension it suffices to show that it is a monomorphism.

Now let \(f \in \mathrm{ker}(\mathrm{ev}_{(x_i)}) \subseteq K[X]_{\leq n}\) and assume that \(f \neq 0\).
Then \(f\) has at least \(n+1\) many roots, namely \(x_0,...,x_n\) and using polynomial division we get \(f = \prod_{i=0}^{n} (x - x_i) \cdot h\).
This shows \(\mathrm{deg}(f) \geq n+1\) but by assumption \(\mathrm{deg}(f) \leq n\), so contradiction.
Therefore \(f\) is a monomorphism resp. even an isomorphism.

The existence of a unique polynomial satisfyng the conditions is furthermore just a rephrasement of bijectivity of \(\mathrm{ev}_{(x_i)}\)