for n being Nat
for R being domRing
for p being non zero Polynomial of R
for a being Element of R
for b being non zero Element of R holds
( (rpoly (1,a)) `^ n divides p iff (rpoly (1,a)) `^ n divides b * p )