This is a lemma that authors Amann/Escher of textbook Analysis I consider clear.
Let $K$ be a ring with unity. Then $K[X_1, \ldots, X_{m+1}]$ and $K[X_1, \ldots, X_{m}][X]$ are isomorphic.
I typed carefully authors' definitions of ring of formal power series and that of polynomials in this question.
My attempt:
If $p \in K[X_1, \ldots, X_{m+1}]$ then $p$ is a function from $\Bbb N^{m+1}$ to $K$. If $p' \in K[X_1, \ldots, X_{m}][X]$ then $p'$ is a function from $\Bbb N$ to $K[X_1, \ldots, X_{m}]$.
We define a function $\mathcal F:K[X_1, \ldots, X_{m+1}] \to K[X_1, \ldots, X_{m}][X]$ by $\mathcal F (p) = p'$.
At this point, I am stuck at matching which $p$ to which $p'$. Please shed me some light!
I have figured out a proof and posted it here. If your are interested, please help me verify it. Thank you for your dedicated help!
If $f \in K[X_1, \ldots, X_{m}][X]$ then $f$ is a function from $\Bbb N$ to $K[X_1, \ldots, X_{m}]$. If $h \in K[X_1, \ldots, X_{m+1}]$ then $h$ is a function from $\Bbb N^{m+1}$ to $K$.
We define a function $\mathcal F: K[X_1, \ldots, X_{m}][X] \to K[X_1, \ldots, X_{m+1}]$ by $\mathcal F (f) = h$ where $h(n_1,n_2,\dots,n_{m+1}) = f(n_1)(n_2,\dots,n_{m+1})$.
It is easy to verify that $\mathcal F$ is bijective. Let $f_1,f_2 \in K[X_1, \ldots, X_{m}][X]$ and $(n_1,n_2,\dots,n_{m+1}) \in \Bbb N^{m+1}$.
We have
$\begin{aligned} & \mathcal F (f_1 + f_2) (n_1,n_2,\dots,n_{m+1})\\ = &(f_1+f_2)(n_1)(n_2,\dots,n_{m+1}) \\ = & (f_1(n_1)+f_2(n_1))(n_2,\dots,n_{m+1})\\ = & f_1(n_1)(n_2,\dots,n_{m+1}) + f_2(n_1)(n_2,\dots,n_{m+1})\\ = & \mathcal F (f_1) + \mathcal F (f_2) \end{aligned}$
and
$\begin{aligned} & \mathcal F (f_1 \cdot f_2) (n_1,n_2,\dots,n_{m+1})\\ = & (f_1 \cdot f_2)(n_1)(n_2,\dots,n_{m+1}) \\ = & \left( \sum_{k \le n_1} (f_1(k) \cdot f_2(n_1-k)) \right) (n_2,\dots,n_{m+1})\\ = & \sum_{k \le n_1} ((f_1(k) \cdot f_2(n_1-k))(n_2,\dots,n_{m+1})) \\ = & \sum_{k \le n_1} \left( \sum_{\bar n \le (n_2,\dots,n_{m+1})} ( f_1(k)(\bar n) \cdot f_2(n_1-k)((n_2,\dots,n_{m+1}) -\bar n)) \right) \\ = & \sum_{k \le n_1} \sum_{\bar n \le (n_2,\dots,n_{m+1})} ( f_1(k)(\bar n) \cdot f_2(n_1-k)((n_2,\dots,n_{m+1}) -\bar n)) \\ = & \sum_{(p_1,\dots,p_{m+1}) \le (n_1,\dots,n_{m+1})} ( f_1(p_1)(p_2,\dots,p_{m+1}) \cdot f_2(n_1-p_1)((n_2,\dots,n_{m+1}) - (p_2,\dots,p_{m+1}))) \\ = & \sum_{(p_1,\dots,p_{m+1}) \le (n_1,\dots,n_{m+1})} ( f_1(p_1)(p_2,\dots,p_{m+1}) \cdot f_2(n_1-p_1)(n_2 -p_2,\dots,n_{m+1}-p_{m+1})) \\ = & \sum_{(p_1,\dots,p_{m+1}) \le (n_1,\dots,n_{m+1})} (\mathcal F(f_1)(p_1,\dots,p_{m+1}) \cdot \mathcal F(f_2) ((n_1,\dots,n_{m+1}) - (p_1,\dots,p_{m+1}))) \\ = & (\mathcal F(f_1) \cdot \mathcal F(f_2))(n_1,\dots,n_{m+1}) \end{aligned}$
As a result, $\mathcal F$ is an isomorphism.