Lemma 3

For every integer $m \geq 0$ let $c_m$ be the ideal of the algebra $A[[X]]^{sym}$ consisting of all symmetric formal power series of order $\geq m$. The sequence $(c_m)_{m \geq 0}$ is a fundamental system of neighbourhoods of $0$ in $A[[X]]^{sym}$.

The lemma clearly holds when $I$ is finite, so let us assume that $I$ is infinite. For every finite subset $J$ of $I$, consisting of $m$ elements, denote by $\tilde{J}$ the set of elements of $N^{(1)}$ of length $< m$ and with support in $J$. Further denote by $a_J'$ the set of formal power series containing no term $aX^\alpha$ with $a \in \tilde{J}$. Since $\tilde{J}$ is a finite subset of $N^{(1)}$ and every finite subset of $N^{(1)}$ is contained in a set of the form $\tilde{J}$, the family $(a_J')$ is a base of neighbourhoods of $0$ in $A[[X]]$ (IV, p. 26). Now Lemma 1 implies the relation $a_J' \cap A[[X]]^{sym} = c_m$ for every subset $J$ with $m$ elements, and this proves Lemma 3.

Since there are only a finite number of monomials of a given weight in the $S_k$, every formal power series $f \in B$ may be written in a unique way as $f = \sum_{r \geq 0} P_r$, where $P_r$ is an isobaric polynomial of weight $r$ in $B \cap A[S]$. For every integer $m \geq 0$ let $b_m$ be the ideal of $B$ consisting of all formal power series of the above type such that $P_r = 0$ for $0 \leq r < m$. The sequence $(b_m)_{m \geq 0}$ is a base of neighbourhoods of $0$ in $B$.

With the above notation $\psi_1(P_r)$ is a symmetric formal power series in the $X_i$, homogeneous of degree $r$, and so this is the homogeneous component of degree $r$ of $\psi_1(f)$. Lemma 2 shows that $\psi_1$ is an algebra homomorphism of $B$ onto $A[[X]]^{sym}$, mapping $b_m$ to $c_m$ for every integer $m \geq 0$; now Lemma 3 shows $\psi_1$ to be bicontinuous, and this completes the proof of Theorem 2.