let R be Ring; :: thesis: for V being RightMod of R
for W being Submodule of V holds (0). W = (0). V
let V be RightMod of R; :: thesis: for W being Submodule of V holds (0). W = (0). V
let W be Submodule of V; :: thesis: (0). W = (0). V
( the carrier of ((0). W) = {(0. W)} & the carrier of ((0). V) = {(0. V)} ) by Def3;
then A1: the carrier of ((0). W) = the carrier of ((0). V) by Def2;
(0). W is Submodule of V by Th26;
hence (0). W = (0). V by A1, Th29; :: thesis: verum