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