= Solution
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^*$ with $F|_M=f$ and $\|F\|=\|f\|$.
For a real <separable> $X$, put $C=\|f\|$. The case $C=0$ is immediate. To extend over one vector $x_0\notin M$, choose a real number $c$ between
$$
\sup_{m\in M}\bigl(f(m)-C\|m-x_0\|\bigr)
\quad\text{and}\quad
\inf_{n\in M}\bigl(C\|n+x_0\|-f(n)\bigr).
$$
The lower endpoint is no greater than the upper: for any $m,n\in M$,
$$
f(m)+f(n)=f(m+n)\leq C\|m+n\|\leq C\|m-x_0\|+C\|n+x_0\|.
$$
The endpoints are finite because testing zero bounds them between finite numbers. Define $F(m+tx_0)=f(m)+tc$. The upper inequality ensures $F(z)\leq C\|z\|$ 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)|\leq C\|z\|$. 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\geq1}a_jz_j$ with $a\in\ell_1$, not identically zero. Let $m$ be the first index with $a_m\ne0$. Writing $t_n=(n+1)^{-1}$, annihilation of $x_n$ gives
$$
0=t_n^{-m}f(x_n)=a_m+\sum_{j>m}a_jt_n^{j-m}.
$$
The tail has absolute value at most $t_n\sum_{j>m}|a_j|\to0$. Letting $n\to\infty$ contradicts $a_m\ne0$. Therefore
$$
\boxed{\overline{\operatorname{span}}\{x_n:n\geq1\}=c_0.}
$$
This is <geometric sequences with accumulating ratios span c0>.
Back to article page
