Complete Inner Product Decomposition
Let $(V, F)$ be a complete inner product space.
Let $M$ be a closed subspace.
Then
\[ H = M \oplus M^\perp . \]
That is for all $x \in V$, there exists unique $z \in M$ and $q \in M^\perp $ such that $x = z + w$.