The Schauder coefficient space is Banach

The displayed formula is a norm on $E$: definiteness follows because its [given, L2] value zero forces every partial sum, hence every coefficient since $e_n\mathrm{\ne }0$, to vanish. Linearity of $E$ and the remaining norm axioms follow termwise from the norm axioms in $X$.

Let $(a^{(k)})$ be Cauchy in $E$. For fixed $n$, apply the $n$th coordinate [given, L1, step 1.1] map on $\mathrm{span}\{e_1,\dots ,e_n\}$ to ${\sum }_{j\le n}(a_j^{(k)}-a_j^{(\mathrm{\ell })})e_j$. By [L1], $(a_n^{(k)}{)}_k$ is Cauchy, so it has a scalar limit $a_n$.

Given $\epsilon >0$, choose $k_0$ so $\mathrm{\parallel }{a}^{(k)}-a^{(\mathrm{\ell })}{\mathrm{\parallel }}_E<\epsilon$ for $k,\mathrm{\ell }\ge k_0$. Fix $k\ge k_0$ and $N$, and let $\mathrm{\ell }\to \mathrm{\infty }$ in the finite sum. Coordinatewise convergence and continuity of finite sums give

Fix $k\ge k_0$. Since $a^{(k)}\in E$, its series has Cauchy tails. For [given, step 3.1] $M>N$, step 3.1 applied to the two partial sums bounds the corresponding finite block for $a-a^{(k)}$ by $2\epsilon$. Hence the partial sums for $a$ are Cauchy in the Banach space $X$, so $a\in E$. Step 3.1 then yields $\mathrm{\parallel }{a}^{(k)}-a{\mathrm{\parallel }}_E\le \epsilon$; thus $E$ is complete.

For $a\in E$, norm continuity gives [given, L2, step 4.1] $\mathrm{\parallel }Sa\mathrm{\parallel }={\lim }_N\mathrm{\parallel }{\sum }_{n\le N}{a}_n{e}_n\mathrm{\parallel }\le \mathrm{\parallel }a{\mathrm{\parallel }}_E$, so $S$ is bounded. Surjectivity and injectivity are respectively existence and uniqueness in [L2].