:: deftheorem defines modetrans ZMODUL02:def 15 :
for R being Ring
for X being LeftMod of R holds modetrans X = ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,(Mult_INT* X) #);