let V be Z_Module; :: thesis: for W being Submodule of V holds ((0). V) /\ W = (0). V
let W be Submodule of V; :: thesis: ((0). V) /\ W = (0). V
0. V in W by Th33;
then 0. V in the carrier of W ;
then {(0. V)} c= the carrier of W by ZFMISC_1:31;
then A1: {(0. V)} /\ the carrier of W = {(0. V)} by XBOOLE_1:28;
the carrier of (((0). V) /\ W) = the carrier of ((0). V) /\ the carrier of W by Def15
.= {(0. V)} /\ the carrier of W by Def10 ;
hence ((0). V) /\ W = (0). V by A1, Def10; :: thesis: verum