Proof explanation: Hahn-Banach Theorem in Stein's functional analysis 
Theorem: Let $V$ be a linear space and $V_{0}$ is its subspace. Also let $p$ be a finite convex functional in $V$ and $l_{0}$ is linear functional in $V_{0}$.
  While $l_{0}(v)\le p(v),v\in V_{0}$
  Then exists linear functional $l$ defined in $V$, which is extension of functional $l_{0}$ and
  $l(v)\le p(v),v\in V$ 

Stein's proof in functional analysis page$_{21}$ :

......
  Well-order all vectors in $V$ that do not belongs to $V_0$ , and denote this ordering by $\lt$ . Among these vectors we call a vector $v$ "extendable"if the linear functional $l_0$ has an extension of the kind desired to the subspace spanned by $V_0 , v$ and all vectors $\lt v$ . What we want to prove is in effect that all vectors not in $V_0$ are extendable .
  ......  

Since we can not apply well-ordering principle to find the largest element in $V$ . If we have proved all vectors not in $V_0$ is extendable , then how to show $V$ is extendable ? 
 A: I think your concerns about the proof are correct. Let me try to offer a repaired version of the proof. 
Well-order $V \setminus V_0$. Let $v_1$ be the least element of $V \setminus V_0$. Let $S_{\leq v}$ denote the span of $V_0 \cup \{ w: w \leq v \}$. 
Let $S_{< v}$ denote the span of $V_0 \cup \{ w: w < v \}$. 
We use (transfinite) recursion to define, for each $v \in V \setminus V_0$, a linear functional $\ell_v$ on $S_{\leq v}$ that is dominated by $p$, that extends $\ell_0$, and that extends $\ell_u$ for each $u < v$. It is then immediate that defining $\ell$ on $V$ by $\ell(v) = \ell_v(v)$ gives the desired functional (to verify linearity use that $\ell_v$ is extended by $\ell_w$ whenever $v<w$). 
For the basis step, define a linear functional $\ell_{v_1}$ on $S_{\leq v_1}$ that is dominated by $p$ and extends $\ell_0$ in the usual way. For the inductive step, suppose that for each $u < v$ we have defined a linear functional $\ell_u$ on $S_{\leq w}$ that is $p$-dominated and extends $\ell_0$. Suppose also that $\ell_t = \ell_u$ for each $t \leq u < v$. Define $\ell'_v$ on the span of $S_{< v}$ as follows. For each $u$ in $S_{<v}$, choose $u'<v$ such that $u \in S_{\leq u'}$ and define $\ell'_v(u) = \ell_{u'}(u)$. 
It is clear that $\ell'_v$ is dominated by $p$ and that $\ell'_v$ extends $\ell_u$ for each $u < v$. Using this last fact, it is easy to check that $\ell'_v$ is linear. Now extend $\ell'_v$ to a linear functional $\ell_v$ on $S_{\leq v}$ in the usual way. This completes the recursive definition. 
