let n be Nat; :: thesis: for F being Field
for E being FieldExtension of F
for x being Function of n,E holds 0. 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 0. E in rng (hom_Ext_eval (x,F))
let E be FieldExtension of F; :: thesis: for x being Function of n,E holds 0. E in rng (hom_Ext_eval (x,F))
let x be Function of n,E; :: thesis: 0. E in rng (hom_Ext_eval (x,F))
set f = hom_Ext_eval (x,F);
A: (hom_Ext_eval (x,F)) . (0. (Polynom-Ring (n,F))) = 0. E by RING_2:6;
dom (hom_Ext_eval (x,F)) = the carrier of (Polynom-Ring (n,F)) by FUNCT_2:def 1;
hence 0. E in rng (hom_Ext_eval (x,F)) by A, FUNCT_1:def 3; :: thesis: verum