let F be Ring; :: thesis:
let E be RingExtension of F; :: thesis:
let a be Element of E; :: thesis:
set g = hom_Ext_eval (a,F);

let o be object ; :: thesis:
assume o in Ann_Poly (a,F) ; :: thesis:
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:

end;

let o be object ; :: thesis:
assume o in ker (hom_Ext_eval (a,F)) ; :: thesis:
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:

end;