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