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