for n, m being non zero Nat holds pfexp (n * m) = (pfexp n) + (pfexp m)