:: deftheorem defines FQ_mult ALGNUM_1:def 14 :
for x being Element of F_Complex holds FQ_mult x = multcomplex || (FQ x);