for X being RealUnitarySpace
for M being Subspace of X
for x being Point of X st x in the carrier of M /\ the carrier of (Ort_Comp M) holds
x = 0. X