:: deftheorem defines Rat-Module ZMODUL07:def 3 :
Rat-Module = ModuleStr(# the carrier of F_Rat, the addF of F_Rat, the ZeroF of F_Rat,(Int-mult-left F_Rat) #);