This is a lemma from textbook Analysis I by Amann/Escher. I present my attempt below. Does it look fine or contain gaps/errors? Thank you for your verification!
Let $K$ be a ring. Then $K[X_1,X_2] \cong K[X_1][X_2]$.
My attempt:
We define a mapping $\psi: K[X_1,X_2] \to K[X_1][X_2]$ by $\psi(f)=g$ where $g(n)(m) := f(n,m)$ for $(n,m) \in \Bbb N^2$. It is not hard to verify that $\psi$ is bijective.
Let $f_,f_2 \in K[X_1,X_2]$ and $(n,m) \in \Bbb N^2$.
We have
$$\begin{align}\psi(f_1 + f_2)(n)(m) &= (f_1 + f_2)(n,m)\\ &= f_1(n,m) + f_2(n,m)\\ &= g_1(n)(m) + g_2(n)(m)\\ &= (g_1(n)+g_2(n))(m)\\ &= (g_1+g_2)(n)(m) \\ &= (\psi(f_1) + \psi(f_2))(n)(m)\end{align}$$
Thus $\psi(f_1 + f_2) = \psi(f_1) + \psi(f_2)$.
Moreover,
$$\begin{align}\psi(f_1 \cdot f_2)(n)(m) &= (f_1 \cdot f_2)(n,m)\\ &= \sum_{(p,q) \le (n,m)}[f_1(p,q) + f_2((n,m) - (p,q))]\\ &= \sum_{(p,q) \le (n,m)}[g_1(p)(q) + g_2(n-p)(m-q)]\\ &= \\ &= \sum_{p \le n} \sum_{q \le m}[g_1(p)(q) + g_2(n-p)(m-q)]\\ &= \sum_{p \le n} [(g_1(p) \cdot g_2(n-p))(m)]\\ &=\left(\sum_{p \le n}[g_1(p) \cdot g_2(n-p)]\right)(m)\\ &= (g_1 \cdot g_2)(n)(m) \\ &=(\psi(f_1) \cdot \psi(f_2))(n)(m)\end{align}$$
Thus $\psi(f_1 \cdot f_2) = \psi(f_1) \cdot \psi(f_2)$.
As a result, $\psi$ is an isomorphism.