theorem ID2a: :: FIELD_16:13

for F being Field
for E being FieldExtension of F
for a being b₁ -algebraic Element of E
for f being b₁ -fixing Automorphism of (FAdj (F,{a})) holds f . a in Roots ((FAdj (F,{a})),(MinPoly (a,F)))