theorem Th4: :: NAT_3:4

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