theorem Th59: :: NAT_3:59

for p being Prime
for n being non zero Nat holds (ppf (p |^ n)) . p = p |^ n