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 p1 st p2 = p1 & E is F2 -extending holds
E is SplittingField of p2
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 p1 st p2 = p1 & E is F2 -extending holds
E is SplittingField of p2
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 p1 st p2 = p1 & E is F2 -extending holds
E is SplittingField of p2
let p2 be non constant Element of the carrier of (Polynom-Ring F2); :: thesis: for E being SplittingField of p1 st p2 = p1 & E is F2 -extending holds
E is SplittingField of p2
let E be SplittingField of p1; :: thesis: ( p2 = p1 & E is F2 -extending implies E is SplittingField of p2 )
assume AS: ( p2 = p1 & E is F2 -extending ) ; :: thesis: E is SplittingField of p2
p1 splits_in E by defspl;
then consider a being non zero Element of E, q being Ppoly of E such that
A: p1 = a * q by FIELD_4:def 5;

now :: thesis: for K being FieldExtension of F2 st p2 splits_in K & K is Subfield of E holds
K == E

let K be FieldExtension of F2; :: thesis: ( p2 splits_in K & K is Subfield of E implies K == E )
assume C: ( p2 splits_in K & K is Subfield of E ) ; :: thesis: K == E
then consider a being non zero Element of K, q being Ppoly of K such that
D: p2 = a * q by FIELD_4:def 5;
p1 splits_in K by D, AS, FIELD_4:def 5;
hence K == E by C, defspl; :: thesis: verum

end;

hence E is SplittingField of p2 by A, AS, FIELD_4:def 5, defspl; :: thesis: verum