theorem :: DTCONSTR:12

for n being Nat holds n = PN-to-NAT . (NAT-to-PN . n)