theorem lemNor1cx: :: FIELD_13:12

for F1, F2 being Field
for p being Ppoly of F1 st F1 == F2 holds
p is Ppoly of F2