let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF
for W, W9, W1 being Subspace of M st the carrier of W = the carrier of W9 holds
( W1 + W = W1 + W9 & W + W1 = W9 + W1 )
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; :: thesis: for W, W9, W1 being Subspace of M st the carrier of W = the carrier of W9 holds
( W1 + W = W1 + W9 & W + W1 = W9 + W1 )
let W, W9, W1 be Subspace of M; :: thesis: ( the carrier of W = the carrier of W9 implies ( W1 + W = W1 + W9 & W + W1 = W9 + W1 ) )
assume A1: the carrier of W = the carrier of W9 ; :: thesis: ( W1 + W = W1 + W9 & W + W1 = W9 + W1 )

A2: now :: thesis: for v being Element of M holds
( ( v in W1 + W implies v in W1 + W9 ) & ( v in W1 + W9 implies v in W1 + W ) )

let v be Element of M; :: thesis: ( ( v in W1 + W implies v in W1 + W9 ) & ( v in W1 + W9 implies v in W1 + W ) )
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: ( v in W1 + W9 implies v in W1 + W )

proof

assume v in W1 + W ; :: thesis: v in W1 + W9
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: verum

end;

assume v in W1 + W9 ; :: thesis: v in W1 + W
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: verum

end;

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