Solution (source code)

= Solution

Apply the <Gram-Schmidt process> explicitly. Start with $f_1=e_1/\|e_1\|$, and for $i\geq2$ set
$$
v_i=e_i-\sum_{j=1}^{i-1}\langle e_i,f_j\rangle f_j,\qquad f_i=v_i/\|v_i\|.
$$
Assume inductively that the previous $f_j$ form an <orthonormal basis> for the span of $e_1,\ldots,e_{i-1}$. <Inner products> give $\langle v_i,f_j\rangle=0$ for every $j<i$. Moreover $v_i\ne0$: otherwise $e_i$ would lie in the span of its predecessors, contradicting that the $e_j$ form a <basis>. Thus $f_i$ is well defined and has unit <norm>. The definition expresses $f_i$ in the span of $e_1,\ldots,e_i$, and also expresses $e_i$ in the span of $f_1,\ldots,f_i$. The two spans therefore agree at each stage. Induction proves \b[the required orthonormal, span-preserving basis].