theorem Th36: :: RUSUB_1:36

for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of V holds
( 0. V in v + W iff v in W )