:: deftheorem defines Sc_Mult GAUSSINT:def 5 :
Sc_Mult = multcomplex | [: the carrier of INT.Ring,G_INT_SET:];