for R being domRing
for B being non zero bag of the carrier of R
for p being Ppoly of R,B
for a being Element of R holds
( (rpoly (1,a)) `^ (B . a) divides p & not (rpoly (1,a)) `^ ((B . a) + 1) divides p )