:: deftheorem defines Zero_ ZMODUL02:def 2 :
for R being Ring
for V being LeftMod of R
for a being Element of R holds Zero_ (a,V) = 0. V;