theorem ppolydiv: :: FIELD_14:49

for F being Field
for B1 being non zero bag of the carrier of F
for p being Ppoly of F,B1
for q being non constant monic Polynomial of F holds
( q divides p iff ex B2 being non zero bag of the carrier of F st
( q is Ppoly of F,B2 & B2 divides B1 ) )