let F be Field; :: thesis: 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
let p, q be Polynomial of F; :: thesis: for n, k being Element of NAT st q `^ n divides p & k <= n holds
q `^ k divides p
let n, k be Element of NAT ; :: thesis: ( q `^ n divides p & k <= n implies q `^ k divides p )
assume A: ( q `^ n divides p & k <= n ) ; :: thesis: q `^ k divides p
then consider r being Polynomial of F such that
B: p = (q `^ n) *' r by RING_4:1;
consider j being Nat such that
C: n = k + j by A, NAT_1:10;
reconsider j = j as Element of NAT by ORDINAL1:def 12;
(q `^ n) *' r = ((q `^ k) *' (q `^ j)) *' r by C, multi0
.= (q `^ k) *' ((q `^ j) *' r) by POLYNOM3:33 ;
hence q `^ k divides p by B, RING_4:1; :: thesis: verum