for R, T being Ring
for S being Subring of R
for f being Polynomial of S
for g being Polynomial of R st f = g holds
for a being Element of R holds Ext_eval (f,(In (a,T))) = Ext_eval (g,(In (a,T)))