theorem Th41: :: RUSUB_1:41

for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of V holds
( 0. V in v + W iff v + W = the carrier of W ) by Th36, Lm3;