[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.[/step]

[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: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]