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