for F being Field
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}))