In my textbook Analysis I by Amann/Escher: A formal power series in $m$ indeterminates over $K$ is a function from $\Bbb N^m$ to $K$.
There is a lemma as follows:
$p=\sum_{\alpha} p_{\alpha} X^{\alpha} \in K\left[X_{1}, \ldots, X_{m}\right]$ can be written in the form $p=\sum_{j=0}^{n} q_{j} X_{m}^{j}$ for suitable $n \in \mathbb{N}$ and $q_{j} \in K\left[X_{1}, \ldots, X_{m-1}\right]$.
From another post in MSE, I am assured that $p=\sum_{\alpha} p_{\alpha} X^{\alpha} \in K\left[X_{1}, \ldots, X_{m}\right]$ and $p=\sum_{j=0}^{n} q_{j} X_{m}^{j} \in K[X_1, \ldots, X_{m - 1}][X_{m}]$. Thus $p=\sum_{\alpha} p_{\alpha} X^{\alpha}$ and $p=\sum_{j=0}^{n} q_{j} X_{m}^{j}$ are different objects.
My questions:
Is it correct that $K\left[X_{1}, \ldots, X_{m}\right] \ni\sum_{\alpha} p_{\alpha} X^{\alpha} \neq \sum_{j=0}^{n} q_{j} X_{m}^{j} \in K[X_1, \ldots, X_{m - 1}][X_{m}]$?
Does the lemma mean that there is an isomorphism $f:K\left[X_{1}, \ldots, X_{m}\right] \to K[X_1, \ldots, X_{m - 1}][X_{m}]$ that sends $\sum_{\alpha} p_{\alpha} X^{\alpha} \in K\left[X_{1}, \ldots, X_{m}\right]$ to $\sum_{j=0}^{n} q_{j} X_{m}^{j} \in K[X_1, \ldots, X_{m - 1}][X_{m}]$?
Thank you for your help!