reconsider V1 = the carrier of W1, V2 = the carrier of W2 as Subset of V by RLSUB_1:def 2;

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

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

A1: 0. V = (0. V) + (0. V) ;

( 0. V in W1 & 0. V in W2 ) by RLSUB_1:17;

then A2: 0. V in VS by A1;

A3: VS = { (v + u) where u, v is Element of V : ( v in V1 & u in V2 ) }

hence ex b_{1} being strict Subspace of V st the carrier of b_{1} = { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 ) }
by A2, A3, RLSUB_1:6, RLSUB_1:35; :: thesis: verum

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

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

proof

then reconsider VS = { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 ) } as Subset of V ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 ) } or x in the carrier of V )

assume x in { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 ) } ; :: thesis: x in the carrier of V

then ex v2, v1 being VECTOR of V st

( x = v1 + v2 & v1 in W1 & v2 in W2 ) ;

hence x in the carrier of V ; :: thesis: verum

end;assume x in { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 ) } ; :: thesis: x in the carrier of V

then ex v2, v1 being VECTOR of V st

( x = v1 + v2 & v1 in W1 & v2 in W2 ) ;

hence x in the carrier of V ; :: thesis: verum

A1: 0. V = (0. V) + (0. V) ;

( 0. V in W1 & 0. V in W2 ) by RLSUB_1:17;

then A2: 0. V in VS by A1;

A3: VS = { (v + u) where u, v is Element of V : ( v in V1 & u in V2 ) }

proof

( V1 is linearly-closed & V2 is linearly-closed )
by RLSUB_1:34;
thus
VS c= { (v + u) where u, v is Element of V : ( v in V1 & u in V2 ) }
:: according to XBOOLE_0:def 10 :: thesis: { (v + u) where u, v is Element of V : ( v in V1 & u in V2 ) } c= VS

assume x in { (v + u) where u, v is Element 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;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (v + u) where u, v is Element of V : ( v in V1 & u in V2 ) } or x in VS )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in VS or x in { (v + u) where u, v is Element of V : ( v in V1 & u in V2 ) } )

assume x in VS ; :: thesis: x in { (v + u) where u, v is Element of V : ( v in V1 & u in V2 ) }

then consider u, v 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 Element of V : ( v in V1 & u in V2 ) } by A4; :: thesis: verum

end;assume x in VS ; :: thesis: x in { (v + u) where u, v is Element of V : ( v in V1 & u in V2 ) }

then consider u, v 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 Element of V : ( v in V1 & u in V2 ) } by A4; :: thesis: verum

assume x in { (v + u) where u, v is Element 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

hence ex b