let R be Ring; :: thesis: for V being RightMod of R
for W1, W2 being Submodule of V
for v being Vector of V st ( v in W1 or v in W2 ) holds
v in W1 + W2
let V be RightMod of R; :: thesis: for W1, W2 being Submodule of V
for v being Vector of V st ( v in W1 or v in W2 ) holds
v in W1 + W2
let W1, W2 be Submodule of V; :: thesis: for v being Vector of V st ( v in W1 or v in W2 ) holds
v in W1 + W2
let v be Vector of V; :: thesis: ( ( v in W1 or v in W2 ) implies v in W1 + W2 )
assume A1: ( v in W1 or v in W2 ) ; :: thesis: v in W1 + W2

now :: thesis: v in W1 + W2

per cases ( v in W1 or v in W2 ) by A1;

suppose A2: v in W1 ; :: thesis: v in W1 + W2

( v = v + (0. V) & 0. V in W2 ) by RLVECT_1:def 4, RMOD_2:17;
hence v in W1 + W2 by A2, Th1; :: thesis: verum

end;

suppose A3: v in W2 ; :: thesis: v in W1 + W2

( v = (0. V) + v & 0. V in W1 ) by RLVECT_1:def 4, RMOD_2:17;
hence v in W1 + W2 by A3, Th1; :: thesis: verum

end;

end;

end;

hence v in W1 + W2 ; :: thesis: verum