let n be Nat; :: thesis: for F, E being Field
for x being Function of n,E holds rng (hom_Ext_eval (x,F)) = { (Ext_eval (p,x)) where p is Polynomial of n,F : verum }
let F, E be Field; :: thesis: for x being Function of n,E holds rng (hom_Ext_eval (x,F)) = { (Ext_eval (p,x)) where p is Polynomial of n,F : verum }
let x be Function of n,E; :: thesis: rng (hom_Ext_eval (x,F)) = { (Ext_eval (p,x)) where p is Polynomial of n,F : verum }
set g = hom_Ext_eval (x,F);

A: now :: thesis: for o being object st o in rng (hom_Ext_eval (x,F)) holds
o in { (Ext_eval (p,x)) where p is Polynomial of n,F : verum }

let o be object ; :: thesis: ( o in rng (hom_Ext_eval (x,F)) implies o in { (Ext_eval (p,x)) where p is Polynomial of n,F : verum } )
assume o in rng (hom_Ext_eval (x,F)) ; :: thesis: o in { (Ext_eval (p,x)) where p is Polynomial of n,F : verum }
then consider p being object such that
A1: ( p in dom (hom_Ext_eval (x,F)) & o = (hom_Ext_eval (x,F)) . p ) by FUNCT_1:def 3;
reconsider p = p as Element of the carrier of (Polynom-Ring (n,F)) by A1;
reconsider p = p as Polynomial of n,F by POLYNOM1:def 11;
o = Ext_eval (p,x) by A1, dh;
hence o in { (Ext_eval (p,x)) where p is Polynomial of n,F : verum } ; :: thesis: verum

end;

now :: thesis: for o being object st o in { (Ext_eval (p,x)) where p is Polynomial of n,F : verum } holds
o in rng (hom_Ext_eval (x,F))

let o be object ; :: thesis: ( o in { (Ext_eval (p,x)) where p is Polynomial of n,F : verum } implies o in rng (hom_Ext_eval (x,F)) )
assume o in { (Ext_eval (p,x)) where p is Polynomial of n,F : verum } ; :: thesis: o in rng (hom_Ext_eval (x,F))
then consider p being Polynomial of n,F such that
A2: o = Ext_eval (p,x) ;
A3: (hom_Ext_eval (x,F)) . p = o by A2, dh;
A4: dom (hom_Ext_eval (x,F)) = the carrier of (Polynom-Ring (n,F)) by FUNCT_2:def 1;
p is Element of the carrier of (Polynom-Ring (n,F)) by POLYNOM1:def 11;
hence o in rng (hom_Ext_eval (x,F)) by A3, A4, FUNCT_1:3; :: thesis: verum

end;

hence rng (hom_Ext_eval (x,F)) = { (Ext_eval (p,x)) where p is Polynomial of n,F : verum } by A, TARSKI:2; :: thesis: verum