let n be Nat; :: thesis: for perm being Element of Permutations n ex P being Permutation of (Permutations n) st
for p being Element of Permutations n holds P . p = p * perm
let perm be Element of Permutations n; :: thesis: ex P being Permutation of (Permutations n) st
for p being Element of Permutations n holds P . p = p * perm
set P = Permutations n;
defpred S₁[ set , set ] means for p being Element of Permutations n st $1 = p holds
$2 = p * perm;
A1: for x being set st x in Permutations n holds
ex y being set st
( y in Permutations n & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in Permutations n implies ex y being set st
( y in Permutations n & S₁[x,y] ) )
assume x in Permutations n ; :: thesis: ex y being set st
( y in Permutations n & S₁[x,y] )
then reconsider p = x as Element of Permutations n ;
reconsider pp = p * perm as Element of Permutations n by MATRIX_9:39;
take pp ; :: thesis: ( pp in Permutations n & S₁[x,pp] )
thus ( pp in Permutations n & S₁[x,pp] ) ; :: thesis: verum

end;

consider G being Function of (Permutations n),(Permutations n) such that
A2: for x being set st x in Permutations n holds
S₁[x,G . x] from FUNCT_2:sch 1(A1);
for x1, x2 being set st x1 in Permutations n & x2 in Permutations n & G . x1 = G . x2 holds
x1 = x2

proof

let x1, x2 be set ; :: thesis: ( x1 in Permutations n & x2 in Permutations n & G . x1 = G . x2 implies x1 = x2 )
assume A3: ( x1 in Permutations n & x2 in Permutations n & G . x1 = G . x2 ) ; :: thesis: x1 = x2
reconsider p1 = x1, p2 = x2 as Element of Permutations n by A3;
( perm is Permutation of (Seg n) & p1 is Permutation of (Seg n) & p2 is Permutation of (Seg n) ) by MATRIX_2:def 11;
then A4: ( rng perm = Seg n & dom p1 = Seg n & dom p2 = Seg n & G . p1 = p1 * perm & G . p2 = p2 * perm ) by A2, FUNCT_2:67, FUNCT_2:def 3;
then p1 = p1 * (id (rng perm)) by RELAT_1:78
.= p1 * (perm * (perm " )) by FUNCT_1:61
.= (p2 * perm) * (perm " ) by A3, A4, RELAT_1:55
.= p2 * (perm * (perm " )) by RELAT_1:55
.= p2 * (id (rng perm)) by FUNCT_1:61
.= p2 by A4, RELAT_1:78 ;
hence x1 = x2 ; :: thesis: verum

end;

then A5: ( G is one-to-one & Permutations n is finite set & card (Permutations n) = card (Permutations n) ) by FUNCT_2:25, MATRIX_2:30;
then G is onto by STIRL2_1:70;
then reconsider G = G as Permutation of (Permutations n) by A5;
take G ; :: thesis: for p being Element of Permutations n holds G . p = p * perm
thus for p being Element of Permutations n holds G . p = p * perm by A2; :: thesis: verum