theorem Th39: :: NUMBER19:39

for R being Ring
for x being Element of R
for p being Polynomial of R holds Ext_eval (p,x) = eval (p,x)