theorem multi1: :: FIELD_14:40
for F being Field
for p, q being Polynomial of F
for n, k being Element of NAT st q `^ n divides p & k <= n holds
q `^ k divides p