:: deftheorem defines Add_ ZMODUL02:def 3 :
for R being Ring
for V being LeftMod of R
for a being Element of R holds Add_ (a,V) = the addF of V | [:(a * V),(a * V):];