theorem :: NAT_3:41

for p being Prime holds (pfexp p) . p = 1