let n be Nat; :: thesis:
let perm be Element of Permutations n; :: thesis:
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] )

let x be object ; :: thesis:
assume x in Permutations n ; :: thesis:
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:
thus ( pp in Permutations n & S₁[x,pp] ) ; :: thesis:

end;

let x1, x2 be object ; :: thesis:
assume that
A4: x1 in Permutations n and
A5: x2 in Permutations n and
A6: G . x1 = G . x2 ; :: thesis:
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:

end;