Gram-Schmidt Orthonormalization of a Finite Family of Vectors

Let $n$ and $r$ be natural numbers and let $x_1,\dots,x_r$ be vectors in the Euclidean space $\mathbb{R}^{n}$, with the dot product. Then either every $x_i$ is the zero vector, or there exist a natural number $p\le r$ and an orthonormal family $e_1,\dots,e_p$ in $\mathbb{R}^{n}$ such that:

1. (Expansion) For every $1\le i\le r$,

2. (Span) For every $1\le u\le p$ there are real numbers $c_{u1},\dots,c_{ur}$ with