:: deftheorem defines 0_Funcs LMOD_XX1:def 14 :
for R being Ring
for M, N being LeftMod of R holds 0_Funcs (M,N) = ZeroMap (M,N);