theorem Th40: :: NUMBER19:40

for R, S being Ring st S is Subring of R holds
for p being Polynomial of R
for x being Element of R
for q being Polynomial of S
for y being Element of S st p = q & x = y holds
eval (p,x) = eval (q,y)