Editing Hahn–Banach theorem (section)

===Example from Fredholm theory===
To illustrate an actual application of the Hahn–Banach theorem, we will now prove a result that follows almost entirely from the Hahn–Banach theorem.

{{Math theorem
| name = Proposition
| math_statement = Suppose <math>X</math> is a Hausdorff locally convex TVS over the field <math>\mathbf{K}</math> and <math>Y</math> is a vector subspace of <math>X</math> that is [[TVS isomorphism|TVS–isomorphic]] to <math>\mathbf{K}^I</math> for some set <math>I.</math> 
Then <math>Y</math> is a closed and [[Complemented subspace|complemented]] vector subspace of <math>X.</math>
}}

{{Math proof|drop=hidden|proof=
Since <math>\mathbf{K}^I</math> is a complete TVS so is <math>Y,</math> and since any complete subset of a Hausdorff TVS is closed, <math>Y</math> is a closed subset of <math>X.</math> 
Let <math>f = \left(f_i\right)_{i \in I} : Y \to \mathbf{K}^I</math> be a TVS isomorphism, so that each <math>f_i : Y \to \mathbf{K}</math> is a continuous surjective linear functional. 
By the Hahn–Banach theorem, we may extend each <math>f_i</math> to a continuous linear functional <math>F_i : X \to \mathbf{K}</math> on <math>X.</math> 
Let <math>F := \left(F_i\right)_{i \in I} : X \to \mathbf{K}^I</math> so <math>F</math> is a continuous linear surjection such that its restriction to <math>Y</math> is <math>F\big\vert_Y = \left(F_i\big\vert_Y\right)_{i \in I} = \left(f_i\right)_{i \in I} = f.</math> 
Let <math>P := f^{-1} \circ F : X \to Y,</math> which is a continuous linear map whose restriction to <math>Y</math> is <math>P\big\vert_Y = f^{-1} \circ F\big\vert_Y = f^{-1} \circ f = \mathbf{1}_Y,</math> where <math>\mathbb{1}_Y</math> denotes the [[identity map]] on <math>Y.</math> 
This shows that <math>P</math> is a continuous [[linear projection]] onto <math>Y</math> (that is, <math>P \circ P = P</math>). 
Thus <math>Y</math> is complemented in <math>X</math> and <math>X = Y \oplus \ker P</math> in the category of TVSs. <math>\blacksquare</math>
}}

The above result may be used to show that every closed vector subspace of <math>\R^{\N}</math> is complemented because any such space is either finite dimensional or else TVS–isomorphic to <math>\R^{\N}.</math>