theorem :: NEWTON03:36

for a, n being Nat
for p being prime Nat st a divides p |^ n holds
ex k being Nat st a = p |^ k