theorem Th13: :: EUCLID_7:14

for h being FinSequence of NAT st h is one-to-one holds
ex h3 being Permutation of (dom h) ex h2 being FinSequence of NAT st
( h2 = h * h3 & h2 is increasing & dom h = dom h2 & rng h = rng h2 )