theorem Th16: :: ALGNUM_1:12

for A, B being Ring
for x being Element of A
for p being Polynomial of A st A is Subring of B holds
Ext_eval (p,(In (x,B))) = In ((eval (p,x)),B)