let F be Ring; :: thesis: for S being RingExtension of F
for a being Element of S holds Ann_Poly (a,F) = ker (hom_Ext_eval (a,F))
let E be RingExtension of F; :: thesis: for a being Element of E holds Ann_Poly (a,F) = ker (hom_Ext_eval (a,F))
let a be Element of E; :: thesis: Ann_Poly (a,F) = ker (hom_Ext_eval (a,F))
set g = hom_Ext_eval (a,F);

A: now :: thesis: for o being object st o in Ann_Poly (a,F) holds
o in ker (hom_Ext_eval (a,F))

let o be object ; :: thesis: ( o in Ann_Poly (a,F) implies o in ker (hom_Ext_eval (a,F)) )
assume o in Ann_Poly (a,F) ; :: thesis: o in ker (hom_Ext_eval (a,F))
then consider p being Polynomial of F such that
A1: ( o = p & Ext_eval (p,a) = 0. E ) ;
A2: (hom_Ext_eval (a,F)) . p = 0. E by A1, ALGNUM_1:def 11;
reconsider b = p as Element of (Polynom-Ring F) by POLYNOM3:def 10;
b in { x where x is Element of (Polynom-Ring F) : (hom_Ext_eval (a,F)) . x = 0. E } by A2;
hence o in ker (hom_Ext_eval (a,F)) by A1, VECTSP10:def 9; :: thesis: verum

end;

now :: thesis: for o being object st o in ker (hom_Ext_eval (a,F)) holds
o in Ann_Poly (a,F)

let o be object ; :: thesis: ( o in ker (hom_Ext_eval (a,F)) implies o in Ann_Poly (a,F) )
assume o in ker (hom_Ext_eval (a,F)) ; :: thesis: o in Ann_Poly (a,F)
then o in { x where x is Element of (Polynom-Ring F) : (hom_Ext_eval (a,F)) . x = 0. E } by VECTSP10:def 9;
then consider b being Element of (Polynom-Ring F) such that
A1: ( o = b & (hom_Ext_eval (a,F)) . b = 0. E ) ;
reconsider p = b as Polynomial of F by POLYNOM3:def 10;
Ext_eval (p,a) = 0. E by A1, ALGNUM_1:def 11;
hence o in Ann_Poly (a,F) by A1; :: thesis: verum

end;

hence Ann_Poly (a,F) = ker (hom_Ext_eval (a,F)) by A, TARSKI:2; :: thesis: verum