theorem Th42: :: RLSUB_1:42
for V being RealLinearSpace
for v being VECTOR of V
for W being Subspace of V holds
( 0. V in v + W iff v in W )