Dimension of a Finite-Dimensional Complex 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}\}$.

The dimension of $V$, written $\dim V$, is the natural number $n$ for which there is an $n$-tuple in $V$ that is a basis of $V$; exactly one natural number has this property, by Orthonormal Bases and Basis Size in a Finite-Dimensional Inner Product Space.