let V be RealLinearSpace; :: thesis: 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 #) )
let W be Subspace of V; :: thesis: ( ((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 #) )
the carrier of W c= the carrier of V by RLSUB_1:def 2;
then W + ((Omega). V) = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) by Lm3;
hence ( ((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 #) ) by Lm1; :: thesis: verum