let F be Field; :: thesis: for E1, E2 being FieldExtension of F
for p being Polynomial of F st E1 == E2 & p splits_in E1 holds
p splits_in E2
let E1, E2 be FieldExtension of F; :: thesis: for p being Polynomial of F st E1 == E2 & p splits_in E1 holds
p splits_in E2
let p be Polynomial of F; :: thesis: ( E1 == E2 & p splits_in E1 implies p splits_in E2 )
assume AS: E1 == E2 ; :: thesis: ( not p splits_in E1 or p splits_in E2 )
then A: doubleLoopStr(# the carrier of E1, the addF of E1, the multF of E1, the OneF of E1, the ZeroF of E1 #) = doubleLoopStr(# the carrier of E2, the addF of E2, the multF of E2, the OneF of E2, the ZeroF of E2 #) by FIELD_7:def 1;
assume p splits_in E1 ; :: thesis: p splits_in E2
then consider a being non zero Element of E1, q being Ppoly of E1 such that
C: p = a * q by FIELD_4:def 5;
reconsider q1 = q as Ppoly of E2 by AS, lemNor1cx;
reconsider a1 = a as Element of E2 by A;

now :: thesis: not a1 = 0. E2

assume a1 = 0. E2 ; :: thesis: contradiction
then a1 = 0. E1 by A;
hence contradiction ; :: thesis: verum

end;

then reconsider a1 = a as non zero Element of E2 by STRUCT_0:def 12;
p = a1 * q1 by AS, C, lemNor1cy;
hence p splits_in E2 by FIELD_4:def 5; :: thesis: verum