:: deftheorem defines FQ_Ring ALGNUM_1:def 15 :
for x being Element of F_Complex holds FQ_Ring x = doubleLoopStr(# (FQ x),(FQ_add x),(FQ_mult x),(In ((1. F_Complex),(FQ x))),(In ((0. F_Complex),(FQ x))) #);