theorem Th19: :: NUMBER08:19

for p being Prime
for n being non zero Nat holds Euler_factorization (p |^ n) = p .--> ((p |^ n) - (p |^ (n - 1)))