let i, j, m, n be Nat; :: thesis: ( i < j & m |^ j divides n implies m |^ (i + 1) divides n )
assume that
A1: i < j and
A2: m |^ j divides n ; :: thesis: m |^ (i + 1) divides n
reconsider i = i, j = j, m = m as Element of NAT by ORDINAL1:def 12;
i + 1 <= j by A1, NAT_1:13;
then m |^ (i + 1) divides m |^ j by NEWTON:89;
hence m |^ (i + 1) divides n by A2, NAT_D:4; :: thesis: verum