theorem :: RLSUB_2:10

for V being RealLinearSpace holds
( ((0). V) + ((Omega). V) = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) & ((Omega). V) + ((0). V) = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) ) by Th9;