let F be Field; :: thesis: for E being FieldExtension of F
for a being Element of E holds rng (hom_Ext_eval (a,F)) = { (Ext_eval (p,a)) where p is Polynomial of F : verum }
let E be FieldExtension of F; :: thesis: for a being Element of E holds rng (hom_Ext_eval (a,F)) = { (Ext_eval (p,a)) where p is Polynomial of F : verum }
let a be Element of E; :: thesis: rng (hom_Ext_eval (a,F)) = { (Ext_eval (p,a)) where p is Polynomial of F : verum }
set g = hom_Ext_eval (a,F);
A: now :: thesis: for x being object st x in rng (hom_Ext_eval (a,F)) holds
x in { (Ext_eval (p,a)) where p is Polynomial of F : verum }
let x be object ; :: thesis: ( x in rng (hom_Ext_eval (a,F)) implies x in { (Ext_eval (p,a)) where p is Polynomial of F : verum } )
assume x in rng (hom_Ext_eval (a,F)) ; :: thesis: x in { (Ext_eval (p,a)) where p is Polynomial of F : verum }
then consider p being object such that
A1: ( p in dom (hom_Ext_eval (a,F)) & x = (hom_Ext_eval (a,F)) . p ) by FUNCT_1:def 3;
reconsider p = p as Element of the carrier of (Polynom-Ring F) by A1;
reconsider p = p as Polynomial of F ;
x = Ext_eval (p,a) by A1, ALGNUM_1:def 11;
hence x in { (Ext_eval (p,a)) where p is Polynomial of F : verum } ; :: thesis: verum
end;
now :: thesis: for x being object st x in { (Ext_eval (p,a)) where p is Polynomial of F : verum } holds
x in rng (hom_Ext_eval (a,F))
let x be object ; :: thesis: ( x in { (Ext_eval (p,a)) where p is Polynomial of F : verum } implies x in rng (hom_Ext_eval (a,F)) )
assume x in { (Ext_eval (p,a)) where p is Polynomial of F : verum } ; :: thesis: x in rng (hom_Ext_eval (a,F))
then consider p being Polynomial of F such that
A2: x = Ext_eval (p,a) ;
A3: (hom_Ext_eval (a,F)) . p = x by A2, ALGNUM_1:def 11;
A4: dom (hom_Ext_eval (a,F)) = the carrier of (Polynom-Ring F) by FUNCT_2:def 1;
p is Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
hence x in rng (hom_Ext_eval (a,F)) by A3, A4, FUNCT_1:3; :: thesis: verum
end;
hence rng (hom_Ext_eval (a,F)) = { (Ext_eval (p,a)) where p is Polynomial of F : verum } by A, TARSKI:2; :: thesis: verum