theorem ID: :: FIELD_16:16

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