let n be Nat; :: thesis: 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
let nt, nt1 be Element of n -tuples_on NAT; :: thesis: ( nt is one-to-one & nt1 is one-to-one & rng nt = rng nt1 implies ex perm being Permutation of (Seg n) st nt1 = nt * perm )
assume that
A1: nt is one-to-one and
A2: nt1 is one-to-one and
A3: rng nt = rng nt1 ; :: thesis: ex perm being Permutation of (Seg n) st nt1 = nt * perm
reconsider nt9 = nt " as Function ;
A4: dom nt9 = rng nt1 by A1, A3, FUNCT_1:33;
A5: dom nt = Seg n by FINSEQ_2:124;
rng nt9 = dom nt by A1, FUNCT_1:33;
then A6: rng (nt9 * nt1) = Seg n by A5, A4, RELAT_1:28;
dom nt1 = Seg n by FINSEQ_2:124;
then dom (nt9 * nt1) = Seg n by A4, RELAT_1:27;
then reconsider nn = nt9 * nt1 as Function of (Seg n),(Seg n) by A6, FUNCT_2:1;
( nn is one-to-one & nn is onto ) by A1, A2, A6, FUNCT_2:def 3;
then reconsider nn = nn as Permutation of (Seg n) ;
take nn ; :: thesis: nt1 = nt * nn
thus nt * nn = (nt * nt9) * nt1 by RELAT_1:36
.= (id (rng nt1)) * nt1 by A1, A3, FUNCT_1:39
.= nt1 by RELAT_1:54 ; :: thesis: verum