let F1 be Field; :: thesis: for p1 being non constant Element of the carrier of (Polynom-Ring F1)
for F2 being FieldExtension of F1
for p2 being non constant Element of the carrier of (Polynom-Ring F2)
for E being SplittingField of p2
for T being F1 -algebraic Subset of F2 st T c= Roots (E,p2) & F2 == FAdj (F1,T) & p1 = p2 holds
E is SplittingField of p1
let p1 be non constant Element of the carrier of (Polynom-Ring F1); :: thesis: for F2 being FieldExtension of F1
for p2 being non constant Element of the carrier of (Polynom-Ring F2)
for E being SplittingField of p2
for T being F1 -algebraic Subset of F2 st T c= Roots (E,p2) & F2 == FAdj (F1,T) & p1 = p2 holds
E is SplittingField of p1
let F2 be FieldExtension of F1; :: thesis: for p2 being non constant Element of the carrier of (Polynom-Ring F2)
for E being SplittingField of p2
for T being F1 -algebraic Subset of F2 st T c= Roots (E,p2) & F2 == FAdj (F1,T) & p1 = p2 holds
E is SplittingField of p1
let p2 be non constant Element of the carrier of (Polynom-Ring F2); :: thesis: for E being SplittingField of p2
for T being F1 -algebraic Subset of F2 st T c= Roots (E,p2) & F2 == FAdj (F1,T) & p1 = p2 holds
E is SplittingField of p1
let E be SplittingField of p2; :: thesis: for T being F1 -algebraic Subset of F2 st T c= Roots (E,p2) & F2 == FAdj (F1,T) & p1 = p2 holds
E is SplittingField of p1
let T be F1 -algebraic Subset of F2; :: thesis: ( T c= Roots (E,p2) & F2 == FAdj (F1,T) & p1 = p2 implies E is SplittingField of p1 )
assume AS: ( T c= Roots (E,p2) & F2 == FAdj (F1,T) ) ; :: thesis: ( not p1 = p2 or E is SplittingField of p1 )
reconsider E = E as F2 -extending FieldExtension of F1 ;
reconsider T = T as finite F1 -algebraic Subset of F2 by AS;
assume A: p2 = p1 ; :: thesis: E is SplittingField of p1
p2 splits_in E by FIELD_8:def 1;
then consider a being non zero Element of E, q being Ppoly of E such that
C: p2 = a * q by FIELD_4:def 5;
D: p1 splits_in E by A, C, FIELD_4:def 5;

E: now :: thesis: for K being Field st p1 splits_in K holds
p2 splits_in K

let K be Field; :: thesis: ( p1 splits_in K implies p2 splits_in K )
assume p1 splits_in K ; :: thesis: p2 splits_in K
then consider a being non zero Element of K, q being Ppoly of K such that
E: p1 = a * q by FIELD_4:def 5;
thus p2 splits_in K by A, E, FIELD_4:def 5; :: thesis: verum

end;

now :: thesis: for U being FieldExtension of F1 st p1 splits_in U & U is Subfield of E holds
E == U

let U be FieldExtension of F1; :: thesis: ( p1 splits_in U & U is Subfield of E implies E == U )
assume F1: ( p1 splits_in U & U is Subfield of E ) ; :: thesis: E == U
then E is FieldExtension of U by FIELD_4:7;
then F3: Roots (E,p1) c= the carrier of U by D, F1, FIELD_8:27;
F1 is Subfield of U by FIELD_4:7;
then F4: FAdj (F1,(Roots (E,p1))) is Subfield of U by F1, F3, FIELD_6:37;
reconsider T1 = T as Subset of E by AS, XBOOLE_1:1;
T c= Roots (E,p1) by AS, A, FIELD_8:7;
then F5: FAdj (F1,T1) is Subfield of FAdj (F1,(Roots (E,p1))) by FIELD_7:10;
FAdj (F1,T1) = FAdj (F1,T) by lemh1;
then FAdj (F1,T) is Subfield of U by F4, F5, EC_PF_1:5;
then U is FieldExtension of FAdj (F1,T) by FIELD_4:7;
then F6: U is FieldExtension of F2 by AS, FIELD_12:37;
p2 splits_in U by F1, E;
hence E == U by F1, F6, FIELD_8:def 1; :: thesis: verum

end;

hence E is SplittingField of p1 by A, C, FIELD_4:def 5, FIELD_8:def 1; :: thesis: verum