theorem bag5: :: FIELD_14:21
for F being Field
for B1, B2 being non zero bag of the carrier of F
for p being Ppoly of F,B1
for q being Ppoly of F,B2 st B1 = B2 holds
p = q