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 nt' = nt " as Function ;
A4: dom nt' = rng nt1 by A1, A3, FUNCT_1:55;
A5: dom nt = Seg n by FINSEQ_2:144;
rng nt' = dom nt by A1, FUNCT_1:55;
then A6: rng (nt' * nt1) = Seg n by A5, A4, RELAT_1:47;
dom nt1 = Seg n by FINSEQ_2:144;
then dom (nt' * nt1) = Seg n by A4, RELAT_1:46;
then reconsider nn = nt' * 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 * nt') * nt1 by RELAT_1:55
.= (id (rng nt1)) * nt1 by A1, A3, FUNCT_1:61
.= nt1 by RELAT_1:80 ; :: thesis: verum