theorem lemma: :: REALALG3:23

for F being Field
for E being FieldExtension of F
for a being b₁ -algebraic Element of E
for b being Element of E holds
( b in the carrier of (FAdj (F,{a})) iff ex p being Polynomial of F st
( deg p < deg (MinPoly (a,F)) & b = Ext_eval (p,a) ) )