[proofplan]
We build the extension on an increasing sequence of subspaces by processing the dense sequence one vector at a time. Dependent stages require no new value, while independent stages use the supplied located interval to choose an admissible scalar and extend across a one-dimensional direct sum. The finite-stage functionals are compatible and uniformly bounded by $M$, so their union defines a bounded linear functional on a dense subspace of $X$. Finally, boundedness gives [uniform continuity](/page/Uniform%20Continuity) on that dense subspace, and the functional extends uniquely to all of $X$ by completion along approximating sequences.
[/proofplan]
[step:Construct the finite-stage functionals along the dense sequence]
We define recursively linear functionals
\begin{align*}
F_n:E_n\to\mathbb{R}
\end{align*}
such that
\begin{align*}
|F_n(e)|\leq M\|e\|_X
\end{align*}
for every $e\in E_n$.
At stage $0$, set $E_0:=Y$ and $F_0:=f$. The asserted bound for $F_0$ is exactly the hypothesis on $f$.
Assume $F_n:E_n\to\mathbb{R}$ has been constructed and satisfies the bound. If the dependence data certify $x_{n+1}\in E_n$, define
\begin{align*}
E_{n+1}:=E_n
\end{align*}
and
\begin{align*}
F_{n+1}:=F_n.
\end{align*}
Then $F_{n+1}$ is linear and has the same bound.
If the dependence data certify $x_{n+1}\notin E_n$, define $z_n:=x_{n+1}$ and
\begin{align*}
E_{n+1}:=E_n+\operatorname{span}(z_n).
\end{align*}
By the hypothesis on the located interval, choose the real number $a_n\in I_n$ selected by the approximation procedure; the procedure supplies arbitrarily accurate rational approximations to this selected value. Define
\begin{align*}
F_{n+1}:E_{n+1}\to\mathbb{R}
\end{align*}
by the rule
\begin{align*}
F_{n+1}(e+t z_n):=F_n(e)+t a_n
\end{align*}
for $e\in E_n$ and $t\in\mathbb{R}$.
Since $z_n\notin E_n$, every element of $E_{n+1}$ has a unique representation $e+t z_n$ with $e\in E_n$ and $t\in\mathbb{R}$. Thus $F_{n+1}$ is well-defined. Linearity follows from uniqueness of this decomposition and linearity of $F_n$. Since $a_n\in I_n$, for every $e\in E_n$ and $t\in\mathbb{R}$ we have
\begin{align*}
|F_{n+1}(e+t z_n)|=|F_n(e)+t a_n|\leq M\|e+t z_n\|_X.
\end{align*}
Hence the bound is preserved at the independent stage.
[guided]
We proceed by induction because the construction only knows how to decide one dense-sequence vector at a time.
At the initial stage, the domain is
\begin{align*}
E_0=Y
\end{align*}
and the functional is
\begin{align*}
F_0=f:Y\to\mathbb{R}.
\end{align*}
The required estimate
\begin{align*}
|F_0(e)|\leq M\|e\|_X
\end{align*}
for $e\in E_0$ is exactly the assumed estimate for $f$.
Now assume that, for some $n\geq 0$, we have already constructed a [linear map](/page/Linear%20Map)
\begin{align*}
F_n:E_n\to\mathbb{R}
\end{align*}
with
\begin{align*}
|F_n(e)|\leq M\|e\|_X
\end{align*}
for every $e\in E_n$.
There are two cases. First suppose the dependence data certify that $x_{n+1}\in E_n$. Then no new vector is being added to the domain. We set
\begin{align*}
E_{n+1}=E_n
\end{align*}
and
\begin{align*}
F_{n+1}=F_n.
\end{align*}
This is important constructively: assigning a new scalar to $x_{n+1}$ would be meaningless, because $x_{n+1}$ already has its value determined by $F_n$. Keeping the same functional preserves linearity and the same estimate.
Second suppose the dependence data certify that $x_{n+1}\notin E_n$. Define
\begin{align*}
z_n:=x_{n+1}
\end{align*}
and enlarge the domain by
\begin{align*}
E_{n+1}=E_n+\operatorname{span}(z_n).
\end{align*}
Because $z_n\notin E_n$, this sum is a direct one-dimensional extension in the following concrete sense: if
\begin{align*}
e_1+t_1z_n=e_2+t_2z_n
\end{align*}
with $e_1,e_2\in E_n$ and $t_1,t_2\in\mathbb{R}$, then
\begin{align*}
e_1-e_2=(t_2-t_1)z_n.
\end{align*}
If $t_2-t_1\neq 0$, this would imply
\begin{align*}
z_n=\frac{1}{t_2-t_1}(e_1-e_2)\in E_n,
\end{align*}
contradicting the independence certificate. Therefore $t_1=t_2$, and then $e_1=e_2$. Thus each element of $E_{n+1}$ has a unique expression $e+t z_n$.
The hypothesis supplies a located interval
\begin{align*}
I_n=\{a\in\mathbb{R}: |F_n(e)+ta|\leq M\|e+t z_n\|_X \text{ for all } e\in E_n \text{ and all } t\in\mathbb{R}\}
\end{align*}
and a procedure selecting an exact real number $a_n\in I_n$. We use that selected value to define
\begin{align*}
F_{n+1}:E_{n+1}\to\mathbb{R}
\end{align*}
by
\begin{align*}
F_{n+1}(e+t z_n)=F_n(e)+t a_n.
\end{align*}
The uniqueness just proved shows that this formula gives one value for each element of $E_{n+1}$.
We verify linearity. Let $u=e_1+t_1z_n$ and $v=e_2+t_2z_n$ be elements of $E_{n+1}$, with $e_1,e_2\in E_n$ and $t_1,t_2\in\mathbb{R}$. For scalars $\alpha,\beta\in\mathbb{R}$,
\begin{align*}
\alpha u+\beta v=(\alpha e_1+\beta e_2)+(\alpha t_1+\beta t_2)z_n.
\end{align*}
Since $E_n$ is a linear subspace, $\alpha e_1+\beta e_2\in E_n$. Therefore
\begin{align*}
F_{n+1}(\alpha u+\beta v)=F_n(\alpha e_1+\beta e_2)+(\alpha t_1+\beta t_2)a_n.
\end{align*}
Using linearity of $F_n$ gives
\begin{align*}
F_{n+1}(\alpha u+\beta v)=\alpha F_n(e_1)+\beta F_n(e_2)+\alpha t_1a_n+\beta t_2a_n.
\end{align*}
Hence
\begin{align*}
F_{n+1}(\alpha u+\beta v)=\alpha F_{n+1}(u)+\beta F_{n+1}(v).
\end{align*}
Finally we verify the norm bound. Let $u\in E_{n+1}$. Write $u=e+t z_n$ with $e\in E_n$ and $t\in\mathbb{R}$. Since $a_n\in I_n$, the defining property of $I_n$ gives
\begin{align*}
|F_n(e)+ta_n|\leq M\|e+t z_n\|_X.
\end{align*}
By the definition of $F_{n+1}$, this is exactly
\begin{align*}
|F_{n+1}(u)|\leq M\|u\|_X.
\end{align*}
Thus the induction step is complete.
[/guided]
[/step]
[step:Define a compatible functional on the increasing union]
Define the linear subspace
\begin{align*}
E:=\bigcup_{n=0}^{\infty}E_n\subset X.
\end{align*}
For $u\in E$, choose any $n\geq 0$ with $u\in E_n$ and define
\begin{align*}
G:E\to\mathbb{R}
\end{align*}
by
\begin{align*}
G(u):=F_n(u).
\end{align*}
This definition is independent of the chosen $n$. Indeed, the construction gives $E_n\subset E_{n+1}$ for every $n$, and in both the dependent and independent cases the map $F_{n+1}$ restricts to $F_n$ on $E_n$. Therefore, by induction, $F_m|_{E_n}=F_n$ whenever $m\geq n$.
To prove linearity, let $u,v\in E$ and $\alpha,\beta\in\mathbb{R}$. Choose $N\geq 0$ such that $u,v\in E_N$. Since $E_N$ is a linear subspace, $\alpha u+\beta v\in E_N$, and hence
\begin{align*}
G(\alpha u+\beta v)=F_N(\alpha u+\beta v)=\alpha F_N(u)+\beta F_N(v)=\alpha G(u)+\beta G(v).
\end{align*}
Thus $G$ is linear. Also, if $u\in E$ and $u\in E_n$, then
\begin{align*}
|G(u)|=|F_n(u)|\leq M\|u\|_X.
\end{align*}
So $G$ is bounded on $E$ with bound $M$.
[/step]
[step:Show that the union domain is dense in $X$]
For every $k\geq 1$, the vector $x_k$ belongs to $E_k$. Indeed, at stage $k-1$, either $x_k\in E_{k-1}$ already, in which case $E_k=E_{k-1}$ and $x_k\in E_k$, or $x_k\notin E_{k-1}$, in which case $x_k$ is added to $E_k$ by construction. Hence
\begin{align*}
\{x_k:k\geq 1\}\subset E.
\end{align*}
Since $(x_k)_{k\geq 1}$ is dense in $X$ and is supplied with approximation data, for every $x\in X$ and every $j\geq 1$ there is an index $k(x,j)\geq 1$ such that
\begin{align*}
\|x_{k(x,j)}-x\|_X\leq \frac{1}{j}.
\end{align*}
Because $x_{k(x,j)}\in E$, these data give explicit approximants from $E$ to every point of $X$. Thus $E$ is dense in $X$.
[/step]
[step:Extend the bounded functional from the dense subspace to all of $X$]
For each $x\in X$, use the approximation data from the dense sequence to define a sequence $(u_j(x))_{j\geq 1}$ in $E$ by
\begin{align*}
u_j(x):=x_{k(x,j)}.
\end{align*}
Then
\begin{align*}
\|u_j(x)-x\|_X\leq \frac{1}{j}
\end{align*}
for every $j\geq 1$. Define
\begin{align*}
F:X\to\mathbb{R}
\end{align*}
by
\begin{align*}
F(x):=\lim_{j\to\infty}G(u_j(x)).
\end{align*}
The limit exists because $(G(u_j(x)))_{j\geq 1}$ is a [Cauchy sequence](/page/Cauchy%20Sequence) in $\mathbb{R}$. For $j,\ell\geq 1$,
\begin{align*}
|G(u_j(x))-G(u_\ell(x))|=|G(u_j(x)-u_\ell(x))|
\end{align*}
and
\begin{align*}
|G(u_j(x))-G(u_\ell(x))|\leq M\|u_j(x)-u_\ell(x)\|_X.
\end{align*}
The triangle inequality gives
\begin{align*}
\|u_j(x)-u_\ell(x)\|_X\leq \|u_j(x)-x\|_X+\|u_\ell(x)-x\|_X
\end{align*}
and therefore
\begin{align*}
\|u_j(x)-u_\ell(x)\|_X\leq \frac{1}{j}+\frac{1}{\ell}.
\end{align*}
Thus $(G(u_j(x)))_{j\geq 1}$ is Cauchy, with an explicit Cauchy modulus obtained from the displayed estimate. Since the theorem is formulated in the complete Cauchy-real setting, this Cauchy sequence with its displayed modulus determines a real limit, so the limit defining $F(x)$ exists.
The value $F(x)$ is independent of the chosen rate-controlled approximating sequence. If $(v_j)_{j\geq 1}$ is another sequence in $E$ with $\|v_j-x\|_X\leq 1/j$, then
\begin{align*}
|G(u_j(x))-G(v_j)|=|G(u_j(x)-v_j)|\leq M\|u_j(x)-v_j\|_X.
\end{align*}
Again,
\begin{align*}
\|u_j(x)-v_j\|_X\leq \|u_j(x)-x\|_X+\|v_j-x\|_X\leq \frac{2}{j},
\end{align*}
so $G(u_j(x))-G(v_j)\to 0$ in $\mathbb{R}$. This follows directly from the displayed estimate, since for every $\varepsilon>0$ choosing $j>2M/\varepsilon$ gives $|G(u_j(x))-G(v_j)|<\varepsilon$ when $M>0$, and the case $M=0$ is immediate. Therefore both rate-controlled sequences define the same limit.
We verify linearity of $F$. Let $x,w\in X$ and $\alpha,\beta\in\mathbb{R}$. For each $j\geq 1$, set
\begin{align*}
r_j:=\max\{1,\lceil 2j(|\alpha|+|\beta|)\rceil\}.
\end{align*}
Since $E$ is a linear subspace, the sequence $(s_j)_{j\geq 1}$ in $E$ defined by
\begin{align*}
s_j:=\alpha u_{r_j}(x)+\beta u_{r_j}(w)
\end{align*}
is well-defined. The triangle inequality and homogeneity of the norm give
\begin{align*}
\|s_j-(\alpha x+\beta w)\|_X\leq |\alpha|\|u_{r_j}(x)-x\|_X+|\beta|\|u_{r_j}(w)-w\|_X
\end{align*}
and therefore
\begin{align*}
\|s_j-(\alpha x+\beta w)\|_X\leq \frac{1}{j}.
\end{align*}
Thus $(s_j)_{j\geq 1}$ is a rate-controlled approximating sequence for $\alpha x+\beta w$. By the independence of the defining limit from the chosen rate-controlled approximating sequence,
\begin{align*}
F(\alpha x+\beta w)=\lim_{j\to\infty}G(s_j).
\end{align*}
Using linearity of $G$,
\begin{align*}
G(s_j)=\alpha G(u_{r_j}(x))+\beta G(u_{r_j}(w)).
\end{align*}
The subsequences $(G(u_{r_j}(x)))_{j\geq 1}$ and $(G(u_{r_j}(w)))_{j\geq 1}$ have the same limits as the convergent sequences defining $F(x)$ and $F(w)$, respectively. By the continuity of addition and scalar multiplication in $\mathbb{R}$,
\begin{align*}
F(\alpha x+\beta w)=\alpha F(x)+\beta F(w).
\end{align*}
Thus $F$ is linear.
The bound passes to the limit. For $x\in X$, use the defining sequence $(u_j(x))_{j\geq 1}$. Since $G(u_j(x))\to F(x)$ in $\mathbb{R}$, the elementary inequality $||r|-|s||\leq |r-s|$ for $r,s\in\mathbb{R}$ gives the continuity of absolute value, and hence
\begin{align*}
|F(x)|=\lim_{j\to\infty}|G(u_j(x))|.
\end{align*}
For every $j\geq 1$,
\begin{align*}
|G(u_j(x))|\leq M\|u_j(x)\|_X.
\end{align*}
The [reverse triangle inequality](/theorems/2300) gives $|\|u_j(x)\|_X-\|x\|_X|\leq \|u_j(x)-x\|_X$, so the displayed estimate $\|u_j(x)-x\|_X\leq 1/j$ implies $\|u_j(x)\|_X\to\|x\|_X$. Therefore
\begin{align*}
|F(x)|\leq M\|x\|_X.
\end{align*}
Thus $\|F\|\leq M$.
[/step]
[step:Verify that the extension agrees with the original functional]
Let $y\in Y$. Since $Y=E_0\subset E$, the constant sequence
\begin{align*}
u_j:=y
\end{align*}
belongs to $E$ and converges to $y$ in the norm $\|\cdot\|_X$. By the independence of the defining limit from the chosen rate-controlled approximating sequence, the constant sequence may be used to compute $F(y)$. Hence
\begin{align*}
F(y)=\lim_{j\to\infty}G(y)=G(y).
\end{align*}
Since $G|_{E_0}=F_0=f$, we obtain
\begin{align*}
F(y)=f(y).
\end{align*}
Thus $F|_Y=f$, and the previously proved estimate gives $|F(x)|\leq M\|x\|_X$ for every $x\in X$. This completes the construction of the required bounded linear extension.
[/step]
