reconsider V1 = the carrier of W1, V2 = the carrier of W2 as Subset of V by RUSUB_1:def 1;
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 object ; :: 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 ;
A1: 0. V = (0. V) + (0. V) by RLVECT_1:4;
( 0. V in W1 & 0. V in W2 ) by RUSUB_1:11;
then A2: 0. V in VS by A1;
A3: VS = { (v + u) where u, v is VECTOR of V : ( v in V1 & u in V2 ) }

proof

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

proof

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

end;

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

end;

( V1 is linearly-closed & V2 is linearly-closed ) by RUSUB_1:28;
hence ex b₁ being strict Subspace of V st the carrier of b₁ = { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } by A2, A3, RLSUB_1:6, RUSUB_1:29; :: thesis: verum