theorem WOW: :: MOEBIUS2:37

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