:: deftheorem defines FQ_add ALGNUM_1:def 13 :
for x being Element of F_Complex holds FQ_add x = addcomplex || (FQ x);