let n be Nat; :: thesis: for F being Field
for E being FieldExtension of F
for x being Function of n,E
for a being Element of (Image_hom_Ext_eval (x,F)) ex y being Element of the carrier of (Polynom-Ring (n,F)) st (hom_Ext_eval (x,F)) . y = a
let F be Field; :: thesis: for E being FieldExtension of F
for x being Function of n,E
for a being Element of (Image_hom_Ext_eval (x,F)) ex y being Element of the carrier of (Polynom-Ring (n,F)) st (hom_Ext_eval (x,F)) . y = a
let E be FieldExtension of F; :: thesis: for x being Function of n,E
for a being Element of (Image_hom_Ext_eval (x,F)) ex y being Element of the carrier of (Polynom-Ring (n,F)) st (hom_Ext_eval (x,F)) . y = a
let x be Function of n,E; :: thesis: for a being Element of (Image_hom_Ext_eval (x,F)) ex y being Element of the carrier of (Polynom-Ring (n,F)) st (hom_Ext_eval (x,F)) . y = a
let a be Element of (Image_hom_Ext_eval (x,F)); :: thesis: ex y being Element of the carrier of (Polynom-Ring (n,F)) st (hom_Ext_eval (x,F)) . y = a
set f = hom_Ext_eval (x,F);
the carrier of (Image_hom_Ext_eval (x,F)) = rng (hom_Ext_eval (x,F)) by defIm;
then ex y being object st
( y in dom (hom_Ext_eval (x,F)) & (hom_Ext_eval (x,F)) . y = a ) by FUNCT_1:def 3;
hence ex y being Element of the carrier of (Polynom-Ring (n,F)) st (hom_Ext_eval (x,F)) . y = a ; :: thesis: verum