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

Let $V$ together with $\langle\cdot,\cdot\rangle$ be a \reftext{def:complex-inner-product-space-2026a}{complex inner product space} with \reftext{lem:vector-space-basic-identities-2026a}{zero vector} $0_{V}$, and suppose that $V$ is \reftext{def:finite-dimensional-vector-space-2026b}{finite-dimensional} and $V\ne\{0_{V}\}$. Then the following hold.

\textbf{1. (Existence)} There are a \reftext{def:natural-numbers-2026a}{natural number} $n$ and an \reftext{def:finite-tuple-power-2026a}{$n$-tuple} $e\in V^{n}$ that is an \reftext{def:orthonormal-basis-2026b}{orthonormal basis} of $V$.

\textbf{2. (Invariance)} If $m$ and $m'$ are natural numbers and $b\in V^{m}$ and $b'\in V^{m'}$ are \reftext{def:finite-basis-2026a}{bases} of $V$, then $m=m'$.