:: deftheorem defines Mult_INT* ZMODUL02:def 14 :
for X being Z_Module holds Mult_INT* X = the lmult of X;