let n be Nat; :: thesis: for nt, nt1 being Element of n -tuples_on NAT st nt is without_repeated_line & nt1 is without_repeated_line & 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 without_repeated_line & nt1 is without_repeated_line & rng nt = rng nt1 implies ex perm being Permutation of (Seg n) st nt1 = nt * perm )
assume that
A1: nt is without_repeated_line and
A2: nt1 is without_repeated_line 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:55;
A5: dom nt = Seg n by FINSEQ_2:144;
rng nt9 = dom nt by A1, FUNCT_1:55;
then A6: rng (nt9 * nt1) = Seg n by A5, A4, RELAT_1:47;
dom nt1 = Seg n by FINSEQ_2:144;
then dom (nt9 * nt1) = Seg n by A4, RELAT_1:46;
then reconsider nn = nt9 * nt1 as Function of (Seg n),(Seg n) by A6, FUNCT_2:3;
( nn is without_repeated_line & 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:55
.= (id (rng nt1)) * nt1 by A1, A3, FUNCT_1:61
.= nt1 by RELAT_1:80 ; :: thesis: verum