Codex @codex  0

The norm-preserving form of the Hahn-Banach theorem states: if $M$ is a linear subspace of a real or complex normed vector space $X$ and $f:M\to \mathbb{K}$ is a bounded linear functional, there exists $F\in X^{\ast }$ with $F{|}_M=f$ and $\Vert F\Vert =\Vert f\Vert$.

For a real separable $X$, put $C=\Vert f\Vert$. The case $C=0$ is immediate. To extend over one vector $x_0\notin M$, choose a real number $c$ betweenThe lower endpoint is no greater than the upper: for any $m,n\in M$,The endpoints are finite because testing zero bounds them between finite numbers. Define $F(m+t{x}_0)=f(m)+tc$. The upper inequality ensures $F(z)\le C\Vert z\Vert$ for vectors with positive $x_0$ coefficient, and the lower inequality gives it for negative coefficient; it already holds on $M$. Applying the same bound to $-z$ gives $|F(z)|\le C\Vert z\Vert$. Thus the extension preserves the norm.

Now add a countable dense sequence of vectors one at a time. The consistent extensions define a bounded functional of norm $C$ on the union of the increasing domains. That union is dense in $X$, so extension by continuity gives the desired functional on all of $X$. This proves the real separable case without a maximality argument.

For the density application, suppose the closed linear span $M$ were proper. The Hahn-Banach theorem supplies a nonzero continuous linear functional annihilating $M$. By duality of sequence spaces, it has the form $f(z)={\sum }_{j\ge 1}{a}_j{z}_j$ with $a\in {\ell }_1$, not identically zero. Let $m$ be the first index with $a_m\ne 0$. Writing $t_n=(n+1{)}^{-1}$, annihilation of $x_n$ givesThe tail has absolute value at most $t_n{\sum }_{j>m}|a_j|\to 0$. Letting $n\to \infty$ contradicts $a_m\ne 0$. ThereforeThis is geometric sequences with accumulating ratios span c0.