theorem lemppoly1: :: RING_5:51
for R being domRing
for a being Element of R holds rpoly (1,a) is Ppoly of R