theorem lemNor1c: :: FIELD_13:15

for F being Field
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