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

A2: now

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

proof

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

end;

assume v in W1 + W' ; :: thesis: v in W1 + W
then v in the carrier of (W1 + W') by STRUCT_0:def 5;
then v in { (v1 + v2) where v1, v2 is Element of M : ( v1 in W1 & v2 in W' ) } by Def1;
then consider v1, v2 being Element of M such that
A6: v = v1 + v2 and
A7: v1 in W1 and
A8: v2 in W' ;
v2 in the carrier of W by A1, A8, STRUCT_0:def 5;
then v2 in W by STRUCT_0:def 5;
then v in { (v1 + v2) where v1, v2 is Element of M : ( v1 in W1 & v2 in W ) } by A6, A7;
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 + W' by VECTSP_4:38; :: thesis: W + W1 = W' + W1
( W1 + W = W + W1 & W1 + W' = W' + W1 ) by Lm1;
hence W + W1 = W' + W1 by A2, VECTSP_4:38; :: thesis: verum