A simple proof that Every finite dimensional Hilbert space has orthonormal basis The proof that Every Hilbert space has orthogonal basis requires Zorn's Lemma. But if the Hilbert Space is finite dimensional, does it still require? If it doesn't, how could I prove in simple terms that Every finite dimensional Hilbert space has orthogonal basis? Thanks!

Here is a proof that an orthonormal basis exists without using Gramm-Schmidt.  We proceed by induction on $n$, the dimension of the Hilbert space $H$.  If $n=1$, then we choose our basis to consist of a single vector with norm 1.
Now for the inductive step.  Let $H$ be an $n$ dimensional Hilbert space.  Choose $v\in H$ of norm 1.  Let $H'=\{w\in H\mid \langle v,w\rangle=0\}$.  Then $H'$ is a Hilbert space of dimension $n-1$.  By induction, it has an orthonormal basis $\{v_1,\ldots,v_{n-1}\}$.  Now it's easy to check that the the set $\{v,v_1,\ldots,v_{n-1}\}$ is orthonormal.  It is therefore a basis for $H$ as it is linearly independent and contains $n$ elements.
Edit in response to a comment: By definition, a Hilbert space $H$ is a vector space with an inner product in which the distance defined by the inner product makes $H$ into a complete metric space.  It's clear that $H'$ is a vector space with an inner product.  Also, $\langle v, \_ \rangle\colon H\to \mathbb{R}$ is continuous, so $H'$ is the inverse image of a closed set ($\{0\}$) under a continuous function, making $H'$ closed.  Closed subsets of complete metric spaces are complete.  It's straightforward to verify that the distance defined by the restricted inner product agrees on $H'$ with the distance defined on $H$.  So the only thing that remains is to verify that $H'$ has dimension $n-1$; that is a fact about vector spaces and has nothing to do with Hilbert spaces.
