let R be Ring; :: thesis: for V being RightMod of R
for W1, W2, W3 being Submodule of V holds W1 + (W2 + W3) = (W1 + W2) + W3
let V be RightMod of R; :: thesis: for W1, W2, W3 being Submodule of V holds W1 + (W2 + W3) = (W1 + W2) + W3
let W1, W2, W3 be Submodule of V; :: thesis: W1 + (W2 + W3) = (W1 + W2) + W3
set A = { (v + u) where u, v is Vector of V : ( v in W1 & u in W2 ) } ;
set B = { (v + u) where u, v is Vector of V : ( v in W2 & u in W3 ) } ;
set C = { (v + u) where u, v is Vector of V : ( v in W1 + W2 & u in W3 ) } ;
set D = { (v + u) where u, v is Vector of V : ( v in W1 & u in W2 + W3 ) } ;
A1: the carrier of (W1 + (W2 + W3)) = { (v + u) where u, v is Vector of V : ( v in W1 & u in W2 + W3 ) } by Def1;
A2: { (v + u) where u, v is Vector of V : ( v in W1 + W2 & u in W3 ) } c= { (v + u) where u, v is Vector of V : ( v in W1 & u in W2 + W3 ) }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (v + u) where u, v is Vector of V : ( v in W1 + W2 & u in W3 ) } or x in { (v + u) where u, v is Vector of V : ( v in W1 & u in W2 + W3 ) } )
assume x in { (v + u) where u, v is Vector of V : ( v in W1 + W2 & u in W3 ) } ; :: thesis: x in { (v + u) where u, v is Vector of V : ( v in W1 & u in W2 + W3 ) }
then consider u, v being Vector of V such that
A3: x = v + u and
A4: v in W1 + W2 and
A5: u in W3 ;
v in the carrier of (W1 + W2) by A4;
then v in { (v + u) where u, v is Vector of V : ( v in W1 & u in W2 ) } by Def1;
then consider u2, u1 being Vector of V such that
A6: v = u1 + u2 and
A7: u1 in W1 and
A8: u2 in W2 ;
u2 + u in { (v + u) where u, v is Vector of V : ( v in W2 & u in W3 ) } by A5, A8;
then u2 + u in the carrier of (W2 + W3) by Def1;
then A9: u2 + u in W2 + W3 ;
v + u = u1 + (u2 + u) by A6, RLVECT_1:def 3;
hence x in { (v + u) where u, v is Vector of V : ( v in W1 & u in W2 + W3 ) } by A3, A7, A9; :: thesis: verum

end;

{ (v + u) where u, v is Vector of V : ( v in W1 & u in W2 + W3 ) } c= { (v + u) where u, v is Vector of V : ( v in W1 + W2 & u in W3 ) }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (v + u) where u, v is Vector of V : ( v in W1 & u in W2 + W3 ) } or x in { (v + u) where u, v is Vector of V : ( v in W1 + W2 & u in W3 ) } )
assume x in { (v + u) where u, v is Vector of V : ( v in W1 & u in W2 + W3 ) } ; :: thesis: x in { (v + u) where u, v is Vector of V : ( v in W1 + W2 & u in W3 ) }
then consider u, v being Vector of V such that
A10: x = v + u and
A11: v in W1 and
A12: u in W2 + W3 ;
u in the carrier of (W2 + W3) by A12;
then u in { (v + u) where u, v is Vector of V : ( v in W2 & u in W3 ) } by Def1;
then consider u2, u1 being Vector of V such that
A13: u = u1 + u2 and
A14: u1 in W2 and
A15: u2 in W3 ;
v + u1 in { (v + u) where u, v is Vector of V : ( v in W1 & u in W2 ) } by A11, A14;
then v + u1 in the carrier of (W1 + W2) by Def1;
then A16: v + u1 in W1 + W2 ;
v + u = (v + u1) + u2 by A13, RLVECT_1:def 3;
hence x in { (v + u) where u, v is Vector of V : ( v in W1 + W2 & u in W3 ) } by A10, A15, A16; :: thesis: verum

end;

then { (v + u) where u, v is Vector of V : ( v in W1 & u in W2 + W3 ) } = { (v + u) where u, v is Vector of V : ( v in W1 + W2 & u in W3 ) } by A2;
hence W1 + (W2 + W3) = (W1 + W2) + W3 by A1, Def1; :: thesis: verum