theorem lemphi5: :: FIELD_6:45

for F being Field
for E being Polynom-Ring b₁ -homomorphic FieldExtension of F
for a being Element of E holds the carrier of (RAdj (F,{a})) = { (Ext_eval (p,a)) where p is Polynomial of F : verum }