Theorem 9.6.2 (Hahn-Banach, Analytic Form [Theorem 5.6, 5.7, Fol99]). Let $E$ be a vector space over $K \in \RC$, $\rho: E \to \real$ be a sublinear functional, $F \subsetneq E$ be a subspace,
For any $\phi \in \hom(F; \real)$ with $\phi \le \rho|_{F}$, there exists $\Phi \in \hom(E; \real)$ such that $\Phi \le \rho$ and $\Phi|_{F} = \phi$.
If $\rho$ is a seminorm, then for any $\phi \in \hom(F; \complex)$ with $\abs{\phi}\le \rho|_{F}$, there exists $\Phi \in \hom(E; \complex)$ such that $\abs{\Phi}\le \rho$ and $\Phi|_{F} = \phi$.
Proof. (1): Let $x_{0} \in E \setminus F$, then by Lemma 9.6.1, there exists $\lambda \in \real$ such that if
then $\phi_{x_0, \lambda}(x) \le \rho(x)$ for all $x \in F + \real x_{0}$. Thus for any $F \subsetneq E$, $\phi$ admits an extension to a subspace that strictly contains $F$.
Let
For any $\Phi, \Phi' \in \mathbf{F}$, define $\Phi \le \Phi'$ if $\Phi'$ is an extension of $\Phi$. Let $\cf \subset \mathbf{F}$ be a chain. For any $\Phi \in \cf$, let $\cd(\Phi)$ be its domain. Since $\bigcup_{\phi \in \cf}\cd(\Phi)$ is a subspace and $\cf$ is a chain, by Lemma 2.0.12, there exists $\Phi \in \hom\paren{\bigcup_{\Phi' \in \cf}\cd(\Phi'); \real}$ such that $\Phi|_{\cd(\Phi')}= \Phi'$ for all $\Phi' \in \cf$. Thus $\Phi \in \mathbf{F}$ is an upper bound of $\cf$.
By Zorn’s lemma, $\mathbf{F}$ admits a maximal element $\Phi$. If $\cd(\Phi) \subsetneq E$, then $\Phi$ is not maximal by the preceding discussion. Therefore $\cd(\Phi) = E$ and $\Phi$ is a desired extension.
(2): Given that $\rho$ is a seminorm, for any $u \in \hom(E; \real)$, $u \le \rho$ if and only if $\abs{u}\le \rho$.
Let $u = \re{\phi}$, then $u \in \hom(E; \real)$ by Proposition 8.4.1. By (1), there exists $U \in \hom(E; \real)$ such that $\abs{U}\le \rho$ and $U|_{F} = u$. For each $x \in E$, let $\Phi(x) = U(x) - iU(ix)$, then $\Phi \in \hom(E; \complex)$ and $\Phi|_{F} = \phi$ by Proposition 8.4.1. In addition, for any $x \in E$, if $\alpha = \overline{\sgn(\Phi(x))}$, then
so $\abs{\Phi}\le \rho$.$\square$