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),(FAdj (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),(FAdj (F,{a}))
let a be Element of E; :: thesis: hom_Ext_eval (a,F) is Function of (Polynom-Ring F),(FAdj (F,{a}))
RAdj (F,{a}) is Subring of FAdj (F,{a}) by FIELD_6:39;
then A: the carrier of (RAdj (F,{a})) c= the carrier of (FAdj (F,{a})) by C0SP1:def 3;
hom_Ext_eval (a,F) is Function of (Polynom-Ring F),(RAdj (F,{a})) by u10;
hence hom_Ext_eval (a,F) is Function of (Polynom-Ring F),(FAdj (F,{a})) by A, FUNCT_2:7; :: thesis: verum