theorem ZZ3z: :: FIELD_14:38
for F being Field
for p, q being Polynomial of F
for r being non zero Polynomial of F st r *' q divides r *' p holds
q divides p