theorem Th40: :: NAT_3:40

for a being Nat
for p being Prime holds (pfexp (p |^ a)) . p = a