theorem :: DUALSP04:34

for X being RealUnitarySpace
for M being Subspace of X
for x, y1, y2, z1, z2 being Point of X st y1 in M & y2 in M & z1 in Ort_Comp M & z2 in Ort_Comp M & x = y1 + z1 & x = y2 + z2 holds
( y1 = y2 & z1 = z2 )