:: deftheorem defines 0_Hom LMOD_XX1:def 21 :
for R being comRing
for M, N being LeftMod of R holds 0_Hom (M,N) = ZeroMap (M,N);