theorem lift8: :: FIELD_12:41

for F1, F2 being Field
for p being Polynomial of F1
for q being Polynomial of F2
for a being Element of F1
for b being Element of F2 st F1 == F2 & p = q & a = b holds
eval (p,a) = eval (q,b)