for n being Nat
for nt, nt1 being Element of n -tuples_on NAT st nt is one-to-one & nt1 is one-to-one & rng nt = rng nt1 holds
ex perm being Permutation of (Seg n) st nt1 = nt * perm