theorem lift7: :: FIELD_12:42

for F1, F2 being Field
for E1 being FieldExtension of F1
for E2 being FieldExtension of F2
for p being Polynomial of F1
for q being Polynomial of F2
for a being Element of E1
for b being Element of E2 st F1 == F2 & E1 == E2 & p = q & a = b holds
Ext_eval (p,a) = Ext_eval (q,b)