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