theorem lemppoly3: :: RING_5:52
for R being domRing
for p, q being Ppoly of R holds p *' q is Ppoly of R