theorem r59Bag: :: FIELD_14:51

for F being Field
for p being Ppoly of F
for q being monic Polynomial of F
for a being Element of F holds
( q divides (rpoly (1,a)) *' p iff ( q divides p or ex r being Polynomial of F st
( r divides p & q = (rpoly (1,a)) *' r ) ) )