theorem lemNor3z: :: FIELD_13:20

for F1, F2 being Field
for p1 being Element of the carrier of (Polynom-Ring F1)
for p2 being Element of the carrier of (Polynom-Ring F2)
for E1 being FieldExtension of F1
for E2 being FieldExtension of F2 st E1 = E2 & p1 = p2 holds
Roots (E1,p1) = Roots (E2,p2)