:: deftheorem defines F_Rat GAUSSINT:def 14 :
F_Rat = doubleLoopStr(# RAT,addrat,multrat,(In (1,RAT)),(In (0,RAT)) #);