Orthogonal basis of complete Euclidean space friends! I read that any complete Euclidean, complex or real, space $R$ has a (normalized) orthogonal basis. By orthogonal basis an orthogonal system of vectors such that the smallest closed subspace containing them is $R$.
In the assumptions there isn't the separability of the space, which would permit to apply the Gram-Schmidt process to any everywhere dense system after removing its linearly dependent elements, so I have no idea how to give myself a proof of the statement.
Thank you all!!!

One uses Zorn's lemma to have the existence of a maximal orthonormal set $\mathscr{B}$ in $R$.
It remains to see that $\mathscr{B}$ is an orthonormal basis (not a basis in the algebraic sense, unless $R$ is finite-dimensional), i.e. $S := \overline{\operatorname{span} \mathscr{B}}$ is the whole space $R$.
Clearly, the maximality of $\mathscr{B}$ implies that $S^\perp = \{0\}$, since otherwise we could extend $\mathscr{B}$ by any unit vector in $S^\perp$ to an orthonormal system properly containing $\mathscr{B}$ in contradiction to its maximality.
Since (see below) we have $R = S \oplus S^\perp$, the triviality of $S^\perp$ implies $S = R$, as desired.
The decomposition $R = S \oplus S^\perp$ is a consequence of the
Projection lemma: Let $E$ be an inner product space, and $C\subset E$ be a nonempty complete convex set. Then there is a (continuous) projection $P_C \colon E \to C$ mapping each point $x\in E$ to the unique point $y\in C$ with
$$\lVert x-y\rVert = \operatorname{dist}(x,C) := \inf \{ \lVert x-c\rVert : c\in C\}.$$
Proof: We first show the existence of an $y\in C$ with $\lVert x-y\rVert = \operatorname{dist}(x,C)$. By definition of the infimum, there is a sequence $(y_n)_{n\in\mathbb{N}}$ in $C$ with $\lVert x-y_n\rVert \to d := \operatorname{dist}(x,C)$. By the parallelogram identity, we have
$$\lVert y_n - y_m\rVert^2 + \lVert (x-y_n) + (x-y_m)\rVert^2 = 2\lVert x-y_n\rVert^2 + 2\lVert x-y_m\rVert^2$$
for all $m,n\in\mathbb{N}$. Given $\varepsilon > 0$, there is an $N(\varepsilon)$ such that $\lVert x-y_k\rVert^2 < d^2 + \frac{\varepsilon^2}{4}$ for $k \geqslant N(\varepsilon)$, and since $\frac{1}{2}(y_n+y_m)\in C$ for all $m,n$ by convexity, we have
$$\begin{align}
\lVert y_n-y_m\rVert^2 &= 2\lVert x-y_n\rVert^2 + 2\lVert x-y_m\rVert^2 - 4 \left\lVert x - \tfrac{1}{2}(y_n+y_m)\right\rVert^2\\
&\leqslant 4d^2 +\varepsilon^2 - 4 \left\lVert x - \tfrac{1}{2}(y_n+y_m)\right\rVert^2\tag{1}\\
&\leqslant \varepsilon^2
\end{align}$$
for all $m,n\geqslant N(\varepsilon)$. So $(y_n)$ is a Cauchy sequence, and since $C$ is complete, there is an $y\in C$ with $y_n \to y$. By the continuity of the norm, we have $\lVert x-y\rVert = d$. The argument also implies the uniqueness of $y\in C$ realising the distance: If $y_1,y_2\in C$ with $\lVert x-y_1\rVert = \lVert x-y_2\rVert = d$, then setting $m = 1,\,n = 2$ in $(1)$ shows $\lVert y_1 - y_2\rVert^2 \leqslant 0$.
We omit the proof of the continuity of $P_C$, since we don't need that for the orthogonal decomposition $R = S \oplus S^\perp$, but we note that $P_C(x)$ is characterised by the condition
$$\bigl(\forall y \in C\bigr)\bigl(\operatorname{Re} \langle x-P_C(x), y-P_C(x)\rangle \leqslant 0\bigr).$$
For, given any $y\in C$, the point $y_t := (1-t)\cdot P_C(x) + t\cdot y$ belongs to $C$ for all $t\in [0,1]$ by convexity, and
$$\begin{align}
\lVert x- y_t\rVert^2 &= \lVert (x-P_C(x)) - t(y-P_C(x))\rVert^2\\
&= \lVert x-P_C(x)\rVert^2 - 2t\operatorname{Re} \langle x-P_C(x),y-P_C(x)\rangle + t^2 \lVert y-P_C(x)\rVert^2.
\end{align}$$
Since $P_C(x)$ minimises the distance to $x$ in $C$ it follows that the derivative of $\lVert x- y_t\rVert^2$ in $0$ is non-negative, and that derivative is $-2\operatorname{Re} \langle x-P_C(x),y-P_C(x)\rangle$.
Conversely, if $P_C(x)\in C$ is a point with $\operatorname{Re}\langle x-P_C(x),y-P_C(x)\rangle \leqslant 0$ for all $y\in C$, it follows that $\lVert x-y\rVert = \lVert x-y_1\rVert \geqslant \lVert x-P_C(x)\rVert$ for all $y\in C$, and so $P_C(x)$ minimises the distance to $x$ in $C$.
Now, if $C$ is a complete linear subspace of $E$, then $\{ y- P_C(x) : y \in C\} = C$, so
$$\operatorname{Re} \langle x-P_C(x),y\rangle \leqslant 0$$
for all $y\in C$, and since $-y\in C$ (and $\pm i y\in C$ if the scalar field is $\mathbb{C}$) for $y\in C$, it follows that $x-P_C(x) \in C^\perp$.
So we have the decomposition $E = C \oplus C^\perp$ for every complete subspace $C$ of an inner product space $E$.
In our setting, $S$ is a closed subspace of the complete space $R$, hence complete, and the decomposition $R = S \oplus S^\perp$ follows.
