theorem lemrpoly: :: FIELD_14:17

for R being domRing
for a being Element of R
for m being non zero Nat holds (rpoly (1,a)) `^ m is Ppoly of R