:: deftheorem defines multcomplex SEQ_4:def 4 :
for c being Complex holds c multcomplex = multcomplex [;] (c,(id COMPLEX));