let F be Field; :: thesis: for E being FieldExtension of F
for K being F -extending FieldExtension of F
for a being F -algebraic Element of E
for b being F -algebraic Element of K st b = a holds
FAdj (F,{a}) = FAdj (F,{b})
let E be FieldExtension of F; :: thesis: for K being F -extending FieldExtension of F
for a being F -algebraic Element of E
for b being F -algebraic Element of K st b = a holds
FAdj (F,{a}) = FAdj (F,{b})
let K be F -extending FieldExtension of F; :: thesis: for a being F -algebraic Element of E
for b being F -algebraic Element of K st b = a holds
FAdj (F,{a}) = FAdj (F,{b})
let a be F -algebraic Element of E; :: thesis: for b being F -algebraic Element of K st b = a holds
FAdj (F,{a}) = FAdj (F,{b})
let b be F -algebraic Element of K; :: thesis: ( b = a implies FAdj (F,{a}) = FAdj (F,{b}) )
assume AS: b = a ; :: thesis: FAdj (F,{a}) = FAdj (F,{b})
E is Subfield of K by FIELD_4:7;
then FAdj (F,{a}) is Subfield of K by EC_PF_1:5;
hence FAdj (F,{a}) = FAdj (F,{b}) by AS, bba, EC_PF_1:8; :: thesis: verum