let F be Field; :: thesis: for E1, E2 being FieldExtension of F
for p being non constant Element of the carrier of (Polynom-Ring F) st E1 == E2 & E1 is SplittingField of p holds
E2 is SplittingField of p
let E1, E2 be FieldExtension of F; :: thesis: for p being non constant Element of the carrier of (Polynom-Ring F) st E1 == E2 & E1 is SplittingField of p holds
E2 is SplittingField of p
let p be non constant Element of the carrier of (Polynom-Ring F); :: thesis: ( E1 == E2 & E1 is SplittingField of p implies E2 is SplittingField of p )
assume AS: E1 == E2 ; :: thesis: ( not E1 is SplittingField of p or E2 is SplittingField of p )
assume B: E1 is SplittingField of p ; :: thesis: E2 is SplittingField of p
then C: p splits_in E1 by FIELD_8:def 1;

now :: thesis: for E being FieldExtension of F st p splits_in E & E is Subfield of E2 holds
E == E2

let E be FieldExtension of F; :: thesis: ( p splits_in E & E is Subfield of E2 implies E == E2 )
assume D: ( p splits_in E & E is Subfield of E2 ) ; :: thesis: E == E2
then E2 is FieldExtension of E by FIELD_4:7;
then E1 is FieldExtension of E by AS, lemNor1cu;
then E is Subfield of E1 by FIELD_4:7;
then E == E1 by B, D, FIELD_8:def 1;
hence E == E2 by AS, helpb; :: thesis: verum

end;

hence E2 is SplittingField of p by AS, lemNor1c, C, FIELD_8:def 1; :: thesis: verum