Theorem: Every non-zero Euclidean vector space V (with inner product I) has an orthonormal basis.

Lemma: Given an orthonormal system B := (b1, b2, ..., bk) in V and a vector a in V, the vector

P(a) := I(a,b1)*b1 + I(a,b2)*b2 + ... + I(a,bk)*bk

is a member of the span of B with the property that the vector a - P(a) is orthogonal to every vector in the span of B.

Proof of Lemma:
We must check that I(a-P(a), b)=0 for every b in the span of B. I will show that a-P(a) is orthogonal to each of the vectors in B, (b1, b2, ..., bk). The result follows directly.
For brevity, let ci := I(a,bi). Thus, P(a) = c1*b1+c2*b2+...+ck*bk.
Let some n in {1,2,...k} be given. By bilinearity of the inner product, we have

I(a-P(a), bn) = I(a,bn)-I(P(a),bn) = cn-I(c1*b1+c2*b2+...+cn*bn,bn) = cn-c1*I(b1,bn)-c2*I(b2,bn)-...-cn*I(bn,bn)

But since B is orthonormal, I(bi,bj) = 0 if i is different from j, and I(bi,bi)=1, so we have:
I(a-P(a),bn) = cn-cn = 0.

Proof of Theorem:
Since V is not zero, we may choose a unit vector b1 (i.e. choose b1 such that I(b1,b1)=1). If V = span of (b1), then B := b1 is an orthonormal basis for V. Otherwise, we may choose a vector a' not in the span of (b1), and by the lemma, we may construct from a' a vector b2 such that (b1, b2) is orthonormal. Continuing in this way, construct b3, b4,...,bn where n=dim V. By the definition of dimension, we may choose a basis B':=(b'1,b'2,...,b'n) which, of course, spans V. By the Steinitz Exchange Lemma (see Noether's Dimension of a Vector Space writeup for proof), B must also span V. Thus, B is an orthonormal basis for V.


Cool Man Eddie just told me this writeup had been C!'ed, so I came back to look at it, and, to be honest, I was as struck by the gruesome formula-filled proof as it seems rp was. The above proof is valid, but, as Yuri Prime mentions below, not very informative/illuminating, especially for someone who didn't already know basic ideas behind the proof. Yuri's writeup below has what mine lacks (i.e. a conceptual explanation), and s/he's done a better job with that than I ever could.