theorem lift6a: :: FIELD_12:39

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