theorem Th11: :: RUSUB_2:11

for V being RealUnitarySpace
for W being Subspace of V holds
( ((Omega). V) + W = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) & W + ((Omega). V) = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) )