:: deftheorem defines RSc_Mult GAUSSINT:def 15 :
RSc_Mult = multcomplex | [: the carrier of F_Rat,G_RAT_SET:];