let F be Field; :: thesis: for E being FieldExtension of F
for a being Element of E holds hom_Ext_eval (a,F) is Function of (Polynom-Ring F),(RAdj (F,{a}))
let E be FieldExtension of F; :: thesis: for a being Element of E holds hom_Ext_eval (a,F) is Function of (Polynom-Ring F),(RAdj (F,{a}))
let a be Element of E; :: thesis: hom_Ext_eval (a,F) is Function of (Polynom-Ring F),(RAdj (F,{a}))
reconsider E1 = E as Polynom-Ring F -homomorphic Field ;
reconsider f = hom_Ext_eval (a,F) as Homomorphism of (Polynom-Ring F),E1 ;
RAdj (F,{a}) = Image f by FIELD_6:44;
then rng f = the carrier of (RAdj (F,{a})) by RING_2:def 6;
hence hom_Ext_eval (a,F) is Function of (Polynom-Ring F),(RAdj (F,{a})) by FUNCT_2:6; :: thesis: verum