let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis:
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; :: thesis:
let W, W9, W1 be Subspace of M; :: thesis:
assume A1: the carrier of W = the carrier of W9 ; :: thesis:

let v be Element of M; :: thesis:
set W1W9 = { (v1 + v2) where v2, v1 is Element of M : ( v1 in W1 & v2 in W9 ) } ;
set W1W = { (v1 + v2) where v2, v1 is Element of M : ( v1 in W1 & v2 in W ) } ;
thus ( v in W1 + W implies v in W1 + W9 ) :: thesis:

assume v in W1 + W ; :: thesis:
then v in the carrier of (W1 + W) by STRUCT_0:def 5;
then v in { (v1 + v2) where v2, v1 is Element of M : ( v1 in W1 & v2 in W ) } by Def1;
then consider v2, v1 being Element of M such that
A3: ( v = v1 + v2 & v1 in W1 ) and
A4: v2 in W ;
v2 in the carrier of W9 by A1, A4, STRUCT_0:def 5;
then v2 in W9 by STRUCT_0:def 5;
then v in { (v1 + v2) where v2, v1 is Element of M : ( v1 in W1 & v2 in W9 ) } by A3;
then v in the carrier of (W1 + W9) by Def1;
hence v in W1 + W9 by STRUCT_0:def 5; :: thesis:

end;

assume v in W1 + W9 ; :: thesis:
then v in the carrier of (W1 + W9) by STRUCT_0:def 5;
then v in { (v1 + v2) where v2, v1 is Element of M : ( v1 in W1 & v2 in W9 ) } by Def1;
then consider v2, v1 being Element of M such that
A5: ( v = v1 + v2 & v1 in W1 ) and
A6: v2 in W9 ;
v2 in the carrier of W by A1, A6, STRUCT_0:def 5;
then v2 in W by STRUCT_0:def 5;
then v in { (v1 + v2) where v2, v1 is Element of M : ( v1 in W1 & v2 in W ) } by A5;
then v in the carrier of (W1 + W) by Def1;
hence v in W1 + W by STRUCT_0:def 5; :: thesis:

end;

hence W1 + W = W1 + W9 by VECTSP_4:30; :: thesis:
( W1 + W = W + W1 & W1 + W9 = W9 + W1 ) by Lm1;
hence W + W1 = W9 + W1 by A2, VECTSP_4:30; :: thesis: