:: deftheorem defines FQ ALGNUM_1:def 12 :
for x being Element of F_Complex holds FQ x = rng (hom_Ext_eval (x,F_Rat));