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