theorem Th9: :: RLSUB_2:9

for V being RealLinearSpace
for W being strict Subspace of V holds
( ((0). V) + W = W & W + ((0). V) = W )