let F be Field; :: thesis: for K being F -finite FieldExtension of F
for E being F -extending F -finite FieldExtension of F
for a being b₁ -algebraic Element of E st E == FAdj (F,{a}) holds
( E == FAdj (K,{a}) & K == FAdj (F,(Coeff (MinPoly (a,K)))) )
let K be F -finite FieldExtension of F; :: thesis: for E being F -extending F -finite FieldExtension of F
for a being K -algebraic Element of E st E == FAdj (F,{a}) holds
( E == FAdj (K,{a}) & K == FAdj (F,(Coeff (MinPoly (a,K)))) )
let E be F -extending F -finite FieldExtension of F; :: thesis: for a being K -algebraic Element of E st E == FAdj (F,{a}) holds
( E == FAdj (K,{a}) & K == FAdj (F,(Coeff (MinPoly (a,K)))) )
let a be K -algebraic Element of E; :: thesis: ( E == FAdj (F,{a}) implies ( E == FAdj (K,{a}) & K == FAdj (F,(Coeff (MinPoly (a,K)))) ) )
assume AS: E == FAdj (F,{a}) ; :: thesis: ( E == FAdj (K,{a}) & K == FAdj (F,(Coeff (MinPoly (a,K)))) )
F: FAdj (K,{a}) = FAdj (F,{a})

proof

E is FieldExtension of FAdj (K,{a}) by FIELD_4:7;
then H1: FAdj (F,{a}) is FieldExtension of FAdj (K,{a}) by AS, FIELD_13:11;
( {a} is Subset of (FAdj (K,{a})) & F is Subfield of FAdj (K,{a}) ) by FIELD_4:7, FIELD_6:35;
then FAdj (K,{a}) == FAdj (F,{a}) by H1, FIELD_6:37, FIELD_4:7;
hence FAdj (K,{a}) = FAdj (F,{a}) ; :: thesis: verum

end;

hence E == FAdj (K,{a}) by AS; :: thesis: K == FAdj (F,(Coeff (MinPoly (a,K))))
set K1 = FAdj (F,(Coeff (MinPoly (a,K))));
( FAdj (F,(Coeff (MinPoly (a,K)))) is Subfield of K & K is Subfield of E ) by FIELD_4:7;
then FAdj (F,(Coeff (MinPoly (a,K)))) is Subfield of E by EC_PF_1:5;
then reconsider E1 = E as F -extending FieldExtension of F by FIELD_4:7;
reconsider a1 = a as FAdj (F,(Coeff (MinPoly (a,K)))) -algebraic Element of E1 ;
A: FAdj (F,{a1}) = FAdj ((FAdj (F,(Coeff (MinPoly (a,K))))),{a1})

proof

E is FieldExtension of FAdj ((FAdj (F,(Coeff (MinPoly (a,K))))),{a1}) by FIELD_4:7;
then H1: FAdj (F,{a1}) is FieldExtension of FAdj ((FAdj (F,(Coeff (MinPoly (a,K))))),{a1}) by AS, FIELD_13:11;
( {a1} is Subset of (FAdj ((FAdj (F,(Coeff (MinPoly (a,K))))),{a1})) & F is Subfield of FAdj ((FAdj (F,(Coeff (MinPoly (a,K))))),{a1}) ) by FIELD_4:7, FIELD_6:35;
then FAdj ((FAdj (F,(Coeff (MinPoly (a,K))))),{a1}) == FAdj (F,{a1}) by H1, FIELD_6:37, FIELD_4:7;
hence FAdj (F,{a1}) = FAdj ((FAdj (F,(Coeff (MinPoly (a,K))))),{a1}) ; :: thesis: verum

end;

B: ( K is FAdj (F,(Coeff (MinPoly (a,K)))) -extending & Coeff (MinPoly (a,K)) is Subset of (FAdj (F,(Coeff (MinPoly (a,K))))) ) by FIELD_4:7, FIELD_6:35;
then reconsider p = MinPoly (a,K) as Polynomial of (FAdj (F,(Coeff (MinPoly (a,K))))) by FIELD_7:11;
reconsider p = p as Element of the carrier of (Polynom-Ring (FAdj (F,(Coeff (MinPoly (a,K)))))) by POLYNOM3:def 10;
LC p = LC (MinPoly (a,K)) by B, FIELD_8:5
.= 1. K by RATFUNC1:def 7
.= 1. (FAdj (F,(Coeff (MinPoly (a,K))))) by EC_PF_1:def 1 ;
then reconsider p = p as monic Element of the carrier of (Polynom-Ring (FAdj (F,(Coeff (MinPoly (a,K)))))) by RATFUNC1:def 7;
C: p is irreducible by B, hirr;
Ext_eval (p,a1) = Ext_eval ((MinPoly (a,K)),a1) by B, FIELD_7:15
.= 0. E1 by FIELD_6:52 ;
then D: MinPoly (a,K) = MinPoly (a1,(FAdj (F,(Coeff (MinPoly (a,K)))))) by C, FIELD_6:52;
E: deg (E,K) = deg ((FAdj (K,{a})),K) by F, AS, FIELD_7:5
.= deg (MinPoly (a,K)) by FIELD_6:67
.= deg (MinPoly (a1,(FAdj (F,(Coeff (MinPoly (a,K))))))) by B, D, FIELD_4:20
.= deg ((FAdj ((FAdj (F,(Coeff (MinPoly (a,K))))),{a1})),(FAdj (F,(Coeff (MinPoly (a,K)))))) by FIELD_6:67
.= deg (E1,(FAdj (F,(Coeff (MinPoly (a,K)))))) by A, AS, FIELD_7:5 ;
reconsider K1 = FAdj (F,(Coeff (MinPoly (a,K)))) as Field ;
reconsider K2 = K as FieldExtension of K1 by FIELD_4:7;
reconsider K2 = K2 as K1 -finite FieldExtension of K1 by FIELD_7:31;
reconsider E2 = E1 as K1 -extending FieldExtension of K1 ;
reconsider E2 = E2 as K1 -extending K2 -finite FieldExtension of K1 by FIELD_7:31;
deg (E2,K1) = (deg (E2,K1)) * (deg (K2,K1)) by E, FIELD_7:30;
hence K == FAdj (F,(Coeff (MinPoly (a,K)))) by FIELD_7:8, XCMPLX_1:7; :: thesis: verum