for X being RealHilbertSpace
for M being Subspace of X
for N being Subset of X
for x being Point of X st N = the carrier of M & N is closed holds
ex y, z being Point of X st
( y in M & z in Ort_Comp M & x = y + z )