let x, a be Element of F_Complex; :: thesis: ( a <> 0. F_Complex & a in the carrier of (FQ_Ring x) implies ex g being Element of (Polynom-Ring F_Rat) st
( not g in Ann_Poly (x,F_Rat) & a = (hom_Ext_eval (x,F_Rat)) . g ) )
set M = { p where p is Polynomial of F_Rat : Ext_eval (p,x) = 0. F_Complex } ;
assume that
A1: a <> 0. F_Complex and
A2: a in the carrier of (FQ_Ring x) ; :: thesis: ex g being Element of (Polynom-Ring F_Rat) st
( not g in Ann_Poly (x,F_Rat) & a = (hom_Ext_eval (x,F_Rat)) . g )
consider g being Element of (Polynom-Ring F_Rat) such that
A3: a = (hom_Ext_eval (x,F_Rat)) . g by A2, Lm62;
take g ; :: thesis: ( not g in Ann_Poly (x,F_Rat) & a = (hom_Ext_eval (x,F_Rat)) . g )
thus not g in Ann_Poly (x,F_Rat) :: thesis: a = (hom_Ext_eval (x,F_Rat)) . g
proof
assume g in Ann_Poly (x,F_Rat) ; :: thesis: contradiction
then consider g1 being Polynomial of F_Rat such that
A5: g1 = g and
A6: Ext_eval (g1,x) = 0. F_Complex ;
thus contradiction by A1, A6, A3, A5, Def9; :: thesis: verum
end;
thus a = (hom_Ext_eval (x,F_Rat)) . g by A3; :: thesis: verum