:: deftheorem defines Mult_INT* ZMODUL02:def 16 :
for X being LeftMod of INT.Ring holds Mult_INT* X = the lmult of X;