theorem Th31: :: RINGDER1:31

for R being domRing
for p, q being Polynomial of R st p = anpoly ((1. R),1) holds
for i being Element of NAT holds
( (p *' q) . (i + 1) = q . i & (p *' q) . 0 = 0. R )