Gram-Schmidt Orthonormalisation in a Real Inner Product Space

Let $\mathbb{R}$ be the ordered field of real numbers, with the notation of that item, let $E$ be a real inner product space with zero vector $0_{E}$, let $n$ be a natural number, let $v\in E^{n}$ be an $n$-tuple in $E$, and let $M=\operatorname{span}(v)$ be its span, a linear subspace of $E$ by The Span of a Finite Family is the Smallest Subspace Containing It and hence a vector space over $\mathbb{R}$ by claim 1 of A Linear Subspace is a Vector Space and Inherits an Inner Product. Then the following hold.

1. (Orthonormalisation)¶ Either $M=\{0_{E}\}$, or there exist a natural number $m$ with $m\le n$ and an orthonormal $m$-tuple $e\in E^{m}$ with $\operatorname{span}(e)=M$. For such an $e$, the $m$-tuple $e^{\ast}\in M^{m}$ with the same components is a basis of the vector space $M$, the finite sums in $M$ agreeing with those in $E$ by claim 2 of A Linear Subspace is a Vector Space and Inherits an Inner Product.

2. (Finite-dimensional subspaces)¶ Let $L$ be a linear subspace of $E$, a vector space over $\mathbb{R}$ by claim 1 of A Linear Subspace is a Vector Space and Inherits an Inner Product, which is finite-dimensional and satisfies $L\ne\{0_{E}\}$. Then there exist a natural number $m$ and an orthonormal $m$-tuple $e\in E^{m}$ with $\operatorname{span}(e)=L$, and the $m$-tuple $e^{\ast}\in L^{m}$ with the same components is a basis of $L$.