theorem Lm62: :: ALGNUM_1:51

for x being Element of F_Complex
for a being Element of (FQ_Ring x) ex g being Element of (Polynom-Ring F_Rat) st a = (hom_Ext_eval (x,F_Rat)) . g