theorem Th24: :: ALGNUM_1:20

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