reconsider V1 = the carrier of W1, V2 = the carrier of W2 as Subset of M by VECTSP_4:def 2;
set VS = { (v + u) where u, v is Element of M : ( v in W1 & u in W2 ) } ;
{ (v + u) where u, v is Element of M : ( v in W1 & u in W2 ) } c= the carrier of M

proof

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

end;

then reconsider VS = { (v + u) where u, v is Element of M : ( v in W1 & u in W2 ) } as Subset of M ;
A1: 0. M = (0. M) + (0. M) by RLVECT_1:4;
( 0. M in W1 & 0. M in W2 ) by VECTSP_4:17;
then A2: 0. M in VS by A1;
A3: VS = { (v + u) where v, u is Element of M : ( v in V1 & u in V2 ) }

proof

thus VS c= { (v + u) where v, u is Element of M : ( v in V1 & u in V2 ) } :: according to XBOOLE_0:def 10 :: thesis: { (v + u) where v, u is Element of M : ( 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 v, u is Element of M : ( v in V1 & u in V2 ) } )
assume x in VS ; :: thesis: x in { (v + u) where v, u is Element of M : ( v in V1 & u in V2 ) }
then consider u, v being Element of M 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 v, u is Element of M : ( 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 v, u is Element of M : ( v in V1 & u in V2 ) } or x in VS )
assume x in { (v + u) where v, u is Element of M : ( v in V1 & u in V2 ) } ; :: thesis: x in VS
then consider v, u being Element of M 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 VECTSP_4:33;
hence ex b₁ being strict Subspace of M st the carrier of b₁ = { (v + u) where u, v is Element of M : ( v in W1 & u in W2 ) } by A2, A3, VECTSP_4:6, VECTSP_4:34; :: thesis: verum