for R being Ring
for S being RingExtension of R
for a being Element of S
for p being Polynomial of R holds Ext_eval ((- p),a) = - (Ext_eval (p,a))