:: deftheorem defines ZERO MOD_2:def 6 :
for R being Ring
for G, H being LeftMod of R holds ZERO (G,H) = LModMorphismStr(# G,H,(ZeroMap (G,H)) #);