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
the carrier of (FAdj (F,{a})) = the carrier of (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
the carrier of (FAdj (F,{a})) = the carrier of (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
the carrier of (FAdj (F,{a})) = the carrier of (FAdj (F,{b}))
let a be F -algebraic Element of E; :: thesis: for b being F -algebraic Element of K st b = a holds
the carrier of (FAdj (F,{a})) = the carrier of (FAdj (F,{b}))
let b be F -algebraic Element of K; :: thesis: ( b = a implies the carrier of (FAdj (F,{a})) = the carrier of (FAdj (F,{b})) )
assume AS: b = a ; :: thesis: the carrier of (FAdj (F,{a})) = the carrier of (FAdj (F,{b}))
FAdj (F,{a}) = RAdj (F,{a}) by FIELD_6:56
.= RAdj (F,{b}) by AS, bb1
.= FAdj (F,{b}) by FIELD_6:56 ;
hence the carrier of (FAdj (F,{a})) = the carrier of (FAdj (F,{b})) ; :: thesis: verum