theorem mmk: :: FIELD_10:9

for F being Field
for E being FieldExtension of F
for K being b₁ -extending FieldExtension of F
for a being b₁ -algebraic Element of E
for b being b₁ -algebraic Element of K st b = a holds
FAdj (F,{a}) = FAdj (F,{b})