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