set VS = { (v + u) where v, u is Vector of V : ( v in W1 & u in W2 ) } ;
{ (v + u) where v, u is Vector of V : ( v in W1 & u in W2 ) } c= the carrier of V

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (v + u) where v, u is Vector of V : ( v in W1 & u in W2 ) } or x in the carrier of V )
assume x in { (v + u) where v, u is Vector of V : ( v in W1 & u in W2 ) } ; :: thesis: x in the carrier of V
then ex v1, v2 being Vector of V st
( x = v1 + v2 & v1 in W1 & v2 in W2 ) ;
hence x in the carrier of V ; :: thesis: verum

end;

then reconsider VS = { (v + u) where v, u is Vector of V : ( v in W1 & u in W2 ) } as Subset of V ;
( 0. V in W1 & 0. V in W2 & 0. V = (0. V) + (0. V) ) by RLVECT_1:def 7, RMOD_2:25;
then A1: 0. V in VS ;
reconsider V1 = the carrier of W1, V2 = the carrier of W2 as Subset of V by RMOD_2:def 2;
A2: VS = { (v + u) where v, u is Vector of V : ( v in V1 & u in V2 ) }

proof

thus VS c= { (v + u) where v, u is Vector of V : ( v in V1 & u in V2 ) } :: according to XBOOLE_0:def 10 :: thesis: { (v + u) where v, u is Vector of V : ( v in V1 & u in V2 ) } c= VS

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in VS or x in { (v + u) where v, u is Vector of V : ( v in V1 & u in V2 ) } )
assume x in VS ; :: thesis: x in { (v + u) where v, u is Vector of V : ( v in V1 & u in V2 ) }
then consider v, u being Vector of V such that
A3: x = v + u and
A4: ( v in W1 & u in W2 ) ;
( v in V1 & u in V2 ) by A4, STRUCT_0:def 5;
hence x in { (v + u) where v, u is Vector of V : ( v in V1 & u in V2 ) } by A3; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (v + u) where v, u is Vector of V : ( v in V1 & u in V2 ) } or x in VS )
assume x in { (v + u) where v, u is Vector of V : ( v in V1 & u in V2 ) } ; :: thesis: x in VS
then consider v, u being Vector of V such that
A5: x = v + u and
A6: ( v in V1 & u in V2 ) ;
( v in W1 & u in W2 ) by A6, STRUCT_0:def 5;
hence x in VS by A5; :: thesis: verum

end;

( V1 is linearly-closed & V2 is linearly-closed ) by RMOD_2:41;
then VS is linearly-closed by A2, RMOD_2:9;
hence ex b₁ being strict Submodule of V st the carrier of b₁ = { (v + u) where v, u is Vector of V : ( v in W1 & u in W2 ) } by A1, RMOD_2:42; :: thesis: verum