Finite inner product space containing maximal orthonormal subset

I want to prove the following theorem.

Let $$V$$ be an $$n$$-dimensional inner product space and $$S$$ be a maximal orthonormal subset of $$V$$. Then show that $$S$$ consists of exactly $$n$$ elements.

Followings are my trial; Naively, For inner product space, via Gram-Schmidt process one can always make orthonormal basis. The maximal orthonormal subset should be that particular one. But how one prove this rigoursly?

$$\dim(V) =n$$

$$S\subset V$$ maximal orthonormal set.

Claim : $$|S|=n$$

Suppose, $$|S|=m

And $$S=\{x_1,x_2,...,x_m\}$$

Clearly $$S$$ is linearly independent.

$$span(S)$$ is a proper closed linear subspace of $$V$$ (Hilbert space) . Hence, $$\exists x_0 \in V\setminus span(S)$$ with $$\|x_0\|=1$$ such that $$x_0 \perp span(S)$$ .

(In that case it is easy to find explicit $$x_0$$)

$$x_0 = \frac{x_0 -\sum_{i=0}^{m} \langle x_0,x_i \rangle x_i}{\| {x_0 -\sum_{i=0}^{m} \langle x_0,x_i \rangle x_i}\| }$$

$$x_0 \perp span(S) \implies x_0 \perp S$$

Hence, $$S'=\{x_1,x_2,...,x_m,x_0\}$$ is an orthonormal set of vectors contradicting the maximality of $$S$$ as $$S$$ is proper subset of $$S'$$.

Your intuition is good. If you have some basis $$e_1, ..., e_n$$ of $$V$$ and an orthonormal family $$v_1, ..., v_{n-1}$$, we can define: $$\tilde{v}_n := e_n - \sum_{k = 1}^{n-1} v_k\langle e_n, v_k \rangle$$ Then for any $$j \in \lbrace 1, ..., n-1 \rbrace$$ we can use orthonormality: $$\langle \tilde{v}_n, v_j \rangle = \langle e_n, v_j \rangle - \left \langle \sum_{k = 1}^{n-1}v_k\langle e_n, v_k \rangle, v_j \right \rangle = \langle e_n, v_j \rangle - \sum_{k = 1}^{n-1}\langle e_n, v_k \rangle\langle v_k, v_j \rangle = \langle e_n, v_j \rangle - \sum_{k=1}^{n-1} \langle e_n, v_k \rangle \delta_{kj} = \langle e_n, v_j \rangle - \langle e_n, v_j \rangle = 0$$ So this yields that $$v_1, ..., v_n$$ is still an orthogonal family. Then just compute $$v_n := \frac{\tilde{v}_n}{\langle \tilde{v}_n, \tilde{v}_n \rangle}$$ and then $$v_1, ..., v_{n-1}, v_n$$ is the orthonormal family we seek.

Now let us prove that this is maximal. We do this by just proving that any orthonormal family is indeed linear independent. So assume this were not the case, i.e. there are some $$\lambda_1, ..., \lambda_n$$ with at least one of it non-zero such that $$\sum_{j = 1}^{n} \lambda_j v_j = 0$$ Let us say that $$\lambda_k \neq zero$$ where $$k \in \lbrace 1, ..., n\rbrace$$. Then it follows: $$0 = \left \langle \sum_{j = 1}^n \lambda_j v_j, v_k \right \rangle = \sum_{j = 1}^n \lambda_j \langle v_j, v_k \rangle = \lambda_k \langle v_k , v_k \rangle >0$$ So there is a contradiction.

The maximal linear independent system does of course have cardinality $$n$$.