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