let R be Ring; :: thesis: for V being RightMod of R
for W being strict Submodule of V holds
( ((0). V) + W = W & W + ((0). V) = W )
let V be RightMod of R; :: thesis: for W being strict Submodule of V holds
( ((0). V) + W = W & W + ((0). V) = W )
let W be strict Submodule of V; :: thesis: ( ((0). V) + W = W & W + ((0). V) = W )
(0). V is Submodule of W by RMOD_2:39;
then the carrier of ((0). V) c= the carrier of W by RMOD_2:def 2;
hence ((0). V) + W = W by Lm3; :: thesis: W + ((0). V) = W
hence W + ((0). V) = W by Lm1; :: thesis: verum