Solution (source code)

= Solution

A <norm> on a <complex vector space> is a map $\|\cdot\|:X\to[0,\infty)$ that vanishes only at zero, satisfies $\|\lambda x\|=|\lambda|\|x\|$, and obeys the <triangle inequality>. The space is Banach when every <Cauchy sequence> in the resulting <metric> converges in $X$.

If $X$ is Banach and $\sum_j\|x_j\|<\infty$, the estimate $\|\sum_{j=m}^nx_j\|\leq\sum_{j=m}^n\|x_j\|$ shows that its <partial sums> are Cauchy, hence converge. Conversely let every such <series> converge and take a <Cauchy sequence> $(y_n)$. Choose a subsequence with $\|y_{n_{k+1}}-y_{n_k}\|<2^{-k}$. The <series> consisting of $y_{n_1}$ followed by these successive differences is absolutely summable in <norm>, so converges by hypothesis; its <partial sums> are exactly this subsequence. A <Cauchy sequence> with a convergent subsequence converges to the same limit, proving \b[the <absolute-series criterion for completeness>].

On the <absolutely summable sequence space> $\ell^1$, coordinatewise addition and scalar multiplication preserve membership, and summing the scalar <triangle inequality> verifies its <norm> axioms. To prove <completeness> using the criterion, let $x^{(k)}=(x_j^{(k)})\in\ell^1$ with $\sum_k\|x^{(k)}\|_1<\infty$. For each $j$ the sum $x_j=\sum_kx_j^{(k)}$ converges absolutely, and the permitted interchange of nonnegative double sums gives
$$
\sum_j|x_j|\leq\sum_j\sum_k|x_j^{(k)}|=\sum_k\|x^{(k)}\|_1<\infty.
$$
Thus $x\in\ell^1$. Moreover
$$
\left\|x-\sum_{k=1}^Nx^{(k)}\right\|_1\leq\sum_{k>N}\|x^{(k)}\|_1\to0.
$$
Every absolutely <norm>-summable <series> therefore converges in $\ell^1$, proving \b[$\ell^1$ is a <Banach space>].