for i, j, m, n being Nat st i < j & m |^ j divides n holds
m |^ (i + 1) divides n