For a subspace $W$ of a finite-dimensional inner product space, $V=W\oplus W^{\perp }$

By [L1], choose a basis $(w_0,\dots ,w_{s-1})$ of $W$ and extend it to a basis $(w_0,\dots ,w_{s-1},v_s,\dots ,v_{n-1})$ of $V$. Empty initial or terminal blocks cover $W=0$ and $W=V$.

Apply [L2] to this basis, obtaining an orthonormal basis $(e_0,\dots ,e_{n-1})$ with $W=\mathrm{span}(e_0,\dots ,e_{s-1})$. Put $U=\mathrm{span}(e_s,\dots ,e_{n-1})$. Orthonormality and [L3] give $U\subseteq W^{\perp }$.

The orthonormal basis splits every vector as a sum of a vector in $W$ and a vector in $U$, so $V=W+U\subseteq W+W^{\perp }$. The reverse inclusion is automatic.

If $x\in W\cap W^{\perp }$, then [L3] gives $⟨x,x⟩=0$, and positive definiteness gives $x=0$. With step 3.1 this is exactly the pair of conditions in [L4], so $V=W\oplus W^{\perp }$. The decomposition of each $x$ is unique: if $w+u=w^{\mathrm{\prime }}+u^{\mathrm{\prime }}$ with $w,w^{\mathrm{\prime }}\in W$ and $u,u^{\mathrm{\prime }}\in W^{\perp }$, then $w-w^{\mathrm{\prime }}=u^{\mathrm{\prime }}-u$ lies in $W\cap W^{\perp }=\{0_V\}$, so $w=w^{\mathrm{\prime }}$ and $u=u^{\mathrm{\prime }}$.