theorem lemppolspl3a: :: FIELD_8:10

for F being Field
for p being non constant monic Polynomial of F
for q being non zero Polynomial of F st p *' q is Ppoly of F holds
p is Ppoly of F