Real and complex $c_0$ are Banach

Fix $n\in \mathbb{N}$. Since $\mathrm{\mid }{x}_n^{(m)}-x_n^{(k)}\mathrm{\mid }\le \mathrm{\parallel }{x}^{(m)}-x^{(k)}{\mathrm{\parallel }}_{\mathrm{\infty }},$ the scalar sequence $(x_n^{(m)}{)}_m$ is Cauchy. By [F2] it has a unique limit, say $x_n\in \mathbb{K}$. The formula sending $n$ to the ordered pair $(n,x_n)$ is single-valued, so [F3] collects these pairs into the graph of one scalar sequence $x=(x_n{)}_{n\in \mathbb{N}}$. This uses uniqueness and Replacement, not a choice of one limit from each of many non-singleton sets.

The sequence $x$ is bounded. Choose $M$ so that $\mathrm{\parallel }{x}^{(m)}-x^{(M)}{\mathrm{\parallel }}_{\mathrm{\infty }}<1$ whenever $m\ge M$. For every coordinate $n$, letting $m$ tend to infinity in $\mathrm{\mid }{x}_n^{(m)}-x_n^{(M)}\mathrm{\mid }<1$ gives $\mathrm{\mid }{x}_n-x_n^{(M)}\mathrm{\mid }\le 1$. Therefore $\mathrm{\mid }{x}_n\mathrm{\mid }\le 1+\mathrm{\parallel }{x}^{(M)}{\mathrm{\parallel }}_{\mathrm{\infty }}$ for every $n$.

In fact $x^{(m)}\to x$ in the supremum norm. Given $\eta >0$, choose $M$ so that $\mathrm{\parallel }{x}^{(m)}-x^{(k)}{\mathrm{\parallel }}_{\mathrm{\infty }}<\eta \mathrm{/}2$ for all $m,k\ge M$. Fix $m\ge M$ and $n$. Passing to the coordinatewise limit as $k\to \mathrm{\infty }$ yields $\mathrm{\mid }{x}_n^{(m)}-x_n\mathrm{\mid }\le \eta \mathrm{/}2$. Taking the supremum over $n$ gives $\mathrm{\parallel }{x}^{(m)}-x{\mathrm{\parallel }}_{\mathrm{\infty }}\le \eta \mathrm{/}2<\eta \mathrm{.}$

The uniform limit $x$ still tends to zero. Given $\epsilon >0$, use step 3.1 with tolerance $\epsilon \mathrm{/}2$ to fix an $m$ with $\mathrm{\parallel }x-x^{(m)}{\mathrm{\parallel }}_{\mathrm{\infty }}<\epsilon \mathrm{/}2$. Since $x^{(m)}\in c_0$, [F1] gives $N$ such that $\mathrm{\mid }{x}_n^{(m)}\mathrm{\mid }<\epsilon \mathrm{/}2$ for all $n\ge N$. Hence $\mathrm{\mid }{x}_n\mathrm{\mid }\le \mathrm{\mid }{x}_n-x_n^{(m)}\mathrm{\mid }+\mathrm{\mid }{x}_n^{(m)}\mathrm{\mid }<\epsilon (n\ge N)\mathrm{.}$ Together with boundedness from step 2.1, this says $x\in c_0(\mathbb{K})$.

Thus every supremum-norm Cauchy sequence in real or complex $c_0$ converges in that norm to an element of $c_0$. By [F4], both spaces are Banach. The construction in step 1.1 used the unique scalar limits and Replacement, and no choice principle entered any step.