theorem lift6: :: FIELD_12:40

for F1, F2 being Field
for p being non zero Polynomial of F1 st F1 == F2 holds
p is non zero Polynomial of F2