let V be Z_Module; for W being Submodule of V holds (0). W = (0). V
let W be Submodule of V; (0). W = (0). V
( the carrier of ((0). W) = {(0. W)} & the carrier of ((0). V) = {(0. V)} )
by Def10;
then A1:
the carrier of ((0). W) = the carrier of ((0). V)
by Def9;
(0). W is Submodule of V
by Th42;
hence
(0). W = (0). V
by A1, Th45; verum