for F being domRing
for p, q being Polynomial of F
for a being Element of F holds
( not rpoly (1,a) divides p *' q or rpoly (1,a) divides p or rpoly (1,a) divides q )