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₁[ object , object ] means for p being Element of Permutations n st $1 = p holds
$2 = p * perm;
A1: card (Permutations n) = card (Permutations n) ;
A2: for x being object st x in Permutations n holds
ex y being object st
( y in Permutations n & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in Permutations n implies ex y being object st
( y in Permutations n & S₁[x,y] ) )
assume x in Permutations n ; :: thesis: ex y being object 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
A3: for x being object st x in Permutations n holds
S₁[x,G . x] from FUNCT_2:sch 1(A2);
for x1, x2 being object st x1 in Permutations n & x2 in Permutations n & G . x1 = G . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in Permutations n & x2 in Permutations n & G . x1 = G . x2 implies x1 = x2 )
assume that
A4: x1 in Permutations n and
A5: x2 in Permutations n and
A6: G . x1 = G . x2 ; :: thesis: x1 = x2
reconsider p1 = x1, p2 = x2 as Element of Permutations n by A4, A5;
p2 is Permutation of (Seg n) by MATRIX_1:def 12;
then A7: dom p2 = Seg n by FUNCT_2:52;
A8: G . p2 = p2 * perm by A3;
A9: G . p1 = p1 * perm by A3;
perm is Permutation of (Seg n) by MATRIX_1:def 12;
then A10: rng perm = Seg n by FUNCT_2:def 3;
p1 is Permutation of (Seg n) by MATRIX_1:def 12;
then dom p1 = Seg n by FUNCT_2:52;
then p1 = p1 * (id (rng perm)) by A10, RELAT_1:52
.= p1 * (perm * (perm ")) by FUNCT_1:39
.= (p2 * perm) * (perm ") by A6, A9, A8, RELAT_1:36
.= p2 * (perm * (perm ")) by RELAT_1:36
.= p2 * (id (rng perm)) by FUNCT_1:39
.= p2 by A10, A7, RELAT_1:52 ;
hence x1 = x2 ; :: thesis: verum

end;

then A11: G is one-to-one by FUNCT_2:19;
G is onto by A11, A1, FINSEQ_4:63;
then reconsider G = G as Permutation of (Permutations n) by A11;
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 A3; :: thesis: verum