let V be Z_Module; :: thesis: for W being strict Submodule of V holds ((0). V) + W = W
let W be strict Submodule of V; :: thesis: ((0). V) + W = W
(0). V is Submodule of W by Th54;
then the carrier of ((0). V) c= the carrier of W by Def9;
hence ((0). V) + W = W by Lm7; :: thesis: verum