for n, m being non zero Nat holds ppf (n |^ m) = (ppf n) |^ m