let R be Ring; :: thesis: for V being RightMod of R
for W, W9, W1 being Submodule of V st the carrier of W = the carrier of W9 holds
( W1 + W = W1 + W9 & W + W1 = W9 + W1 )
let V be RightMod of R; :: thesis: for W, W9, W1 being Submodule of V st the carrier of W = the carrier of W9 holds
( W1 + W = W1 + W9 & W + W1 = W9 + W1 )
let W, W9, W1 be Submodule of V; :: 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 Vector of V holds
( ( v in W1 + W implies v in W1 + W9 ) & ( v in W1 + W9 implies v in W1 + W ) )

let v be Vector of V; :: 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 Vector of V : ( v1 in W1 & v2 in W9 ) } ;
set W1W = { (v1 + v2) where v2, v1 is Vector of V : ( 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) ;
then v in { (v1 + v2) where v2, v1 is Vector of V : ( v1 in W1 & v2 in W ) } by Def1;
then consider v2, v1 being Vector of V such that
A3: ( v = v1 + v2 & v1 in W1 ) and
A4: v2 in W ;
v2 in the carrier of W9 by A1, A4;
then v2 in W9 ;
then v in { (v1 + v2) where v2, v1 is Vector of V : ( v1 in W1 & v2 in W9 ) } by A3;
then v in the carrier of (W1 + W9) by Def1;
hence v in W1 + W9 ; :: thesis: verum

end;

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

end;

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