The Exercise

Let $V$ be a vector space with an inner product and let $|w_1\rangle, |w_2\rangle, \ldots$ be a basis of $V$, its vectors taken in a fixed order. The Gram-Schmidt procedure removes from each basis vector in turn its components along the vectors already made, and scales what is left to unit length: $$|v_1\rangle = \frac{|w_1\rangle}{\bigl\| |w_1\rangle \bigr\|}, \qquad |v_{k+1}\rangle = \frac{|w_{k+1}\rangle - \sum_{i=1}^{k} \langle v_i|w_{k+1}\rangle\,|v_i\rangle} {\bigl\| |w_{k+1}\rangle - \sum_{i=1}^{k} \langle v_i|w_{k+1}\rangle\,|v_i\rangle \bigr\|}.$$(1) The exercise is to show that these vectors span $V$: every vector of $V$ is a linear combination of the $|v_k\rangle$.

The Claim

What Is Checked

The claim is stated over a basis of $V$ in a fixed order and over the normalized Gram-Schmidt vectors (1) made from that basis. What the library shows about these vectors is that they span $V$, as in (2).^✦