theorem lemma7: :: FIELD_6:11

for F being Field
for p being Element of the carrier of (Polynom-Ring F)
for E being FieldExtension of F
for K being b₃ -extending FieldExtension of F
for a being Element of E
for b being Element of K st a = b holds
Ext_eval (p,a) = Ext_eval (p,b)