for i, n, p being Nat st p is prime & i divides p |^ n & not i = 1 holds
ex k being Element of NAT st i = p * k