let x, a be Element of F_Complex; ( 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)
; 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
; ( 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)
a = (hom_Ext_eval (x,F_Rat)) . g
thus
a = (hom_Ext_eval (x,F_Rat)) . g
by A3; verum