:: deftheorem defines g_rat_mult GAUSSINT:def 13 :
g_rat_mult = multcomplex || G_RAT_SET;