theorem Th19: :: ALGNUM_1:15

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