theorem Th11: :: RLSUB_2:11

for V being RealLinearSpace
for W being Subspace of V holds
( ((Omega). V) + W = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) & W + ((Omega). V) = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) )