theorem lemphi4: :: FIELD_6:44

for F being Field
for E being Polynom-Ring b₁ -homomorphic FieldExtension of F
for a being Element of E holds RAdj (F,{a}) = Image (hom_Ext_eval (a,F))