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