for pn being Element of TS PeanoNat holds pn = NAT-to-PN . (PN-to-NAT . pn)