let n be Nat; :: thesis: for F being Field
for E being FieldExtension of F
for x being Function of n,E holds 1. E in rng (hom_Ext_eval (x,F))
let F be Field; :: thesis: for E being FieldExtension of F
for x being Function of n,E holds 1. E in rng (hom_Ext_eval (x,F))
let E be FieldExtension of F; :: thesis: for x being Function of n,E holds 1. E in rng (hom_Ext_eval (x,F))
let x be Function of n,E; :: thesis: 1. E in rng (hom_Ext_eval (x,F))
set f = hom_Ext_eval (x,F);
A: (hom_Ext_eval (x,F)) . (1_ (Polynom-Ring (n,F))) = 1_ E by GROUP_1:def 13
.= 1. E ;
dom (hom_Ext_eval (x,F)) = the carrier of (Polynom-Ring (n,F)) by FUNCT_2:def 1;
hence 1. E in rng (hom_Ext_eval (x,F)) by A, FUNCT_1:def 3; :: thesis: verum