Proof of Orthonormal Bases and Basis Size in a Finite-Dimensional Inner Product Space

Observation. Let $q$ be a natural number and let $c\in V^{q}$ be a basis of $V$. Then there is an orthonormal basis $f\in V^{q}$ of $V$.

Indeed, $c$ is linearly independent, so Gram-Schmidt Orthonormalisation provides an orthonormal tuple $f\in V^{q}$ whose partial spans agree with those of $c$; taking the index $q$, and noting that the restriction of a $q$-tuple to $[q]$ is the tuple itself, gives $\operatorname{span}(f)=\operatorname{span}(c)$. Since $c$ spans $V$, every $u\in V$ lies in $\operatorname{span}(c)$, so $\operatorname{span}(f)=V$ and therefore $f$ spans $V$ as well. By claim 3 of Elementary Properties of an Orthonormal Family the tuple $f$ is linearly independent, so it is a basis of $V$, and being orthonormal it is an orthonormal basis of $V$.

Claim 1. As $V$ is finite-dimensional and $V\ne\{0_{V}\}$, the second alternative of Finite-Dimensional Vector Space must hold, so there are a natural number $n$ and a basis $c\in V^{n}$ of $V$. The observation applied to $c$ yields an orthonormal basis $e\in V^{n}$ of $V$.

Claim 2. The observation applied to $b$ and to $b'$ yields orthonormal bases $f\in V^{m}$ and $f'\in V^{m'}$ of $V$. By Any Two Orthonormal Bases of a Complex Inner Product Space Have the Same Size, $m=m'$.