theorem :: FIELD_16:18

for F being Field
for E being FieldExtension of F
for a being b₁ -algebraic Element of E holds card { f where f is b₁ -fixing Automorphism of (FAdj (F,{a})) : verum } c= card (Roots ((FAdj (F,{a})),(MinPoly (a,F))))