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

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

1. (Existence) There are a natural number $n$ and an $n$-tuple $e\in V^{n}$ that is an orthonormal basis of $V$.

2. (Invariance) If $m$ and $m'$ are natural numbers and $b\in V^{m}$ and $b'\in V^{m'}$ are bases of $V$, then $m=m'$.