let x be Element of F_Complex; :: thesis: 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
let a be Element of (FQ_Ring x); :: thesis: ex g being Element of (Polynom-Ring F_Rat) st a = (hom_Ext_eval (x,F_Rat)) . g
ex g1 being object st
( g1 in dom (hom_Ext_eval (x,F_Rat)) & a = (hom_Ext_eval (x,F_Rat)) . g1 ) by FUNCT_1:def 3;
hence ex g being Element of (Polynom-Ring F_Rat) st a = (hom_Ext_eval (x,F_Rat)) . g ; :: thesis: verum