Gram-Schmidt Orthonormalisation

Let $V$ together with $\langle\cdot,\cdot\rangle$ be a \reftext{def:complex-inner-product-space-2026a}{complex inner product space}, let $m$ be a \reftext{def:natural-numbers-2026a}{natural number}, and let $b\in V^{m}$ be an \reftext{def:finite-tuple-power-2026a}{$m$-tuple} in $V$ that is \reftext{def:linear-independence-finite-family-2026a}{linearly independent}. For $k\in[m]$, with $[k]$ the \reftext{def:initial-segment-natural-numbers-2026a}{initial segment} determined by $k$, write $x|_{[k]}$ for the restriction of a tuple $x$ to $[k]$.

Then there is an \reftext{def:orthonormal-family-2026b}{orthonormal} tuple $e\in V^{m}$ with

the \reftext{def:span-finite-family-2026b}{span} being that of a finite tuple.