for m, n being non zero Nat st pfexp m = pfexp n holds
m = n