let R be Ring; :: thesis:
let V be RightMod of R; :: thesis:
let W, W9, W1 be Submodule of V; :: thesis:
assume A1: the carrier of W = the carrier of W9 ; :: thesis:

let v be Vector of V; :: thesis:
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:

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

end;

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

end;

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