let n, i, j be Nat; :: thesis: ( i in Seg (n + 1) & j in Seg (n + 1) implies for P being set st P = { p1 where p1 is Element of Permutations (n + 1) : p1 . i = j } holds
ex Proj being Function of P,(Permutations n) st
( Proj is bijective & ( for q1 being Element of Permutations (n + 1) st q1 . i = j holds
Proj . q1 = Rem (q1,i) ) ) )
assume that
A1: i in Seg (n + 1) and
A2: j in Seg (n + 1) ; :: thesis: for P being set st P = { p1 where p1 is Element of Permutations (n + 1) : p1 . i = j } holds
ex Proj being Function of P,(Permutations n) st
( Proj is bijective & ( for q1 being Element of Permutations (n + 1) st q1 . i = j holds
Proj . q1 = Rem (q1,i) ) )
set n1 = n + 1;
reconsider N = n as Element of NAT by ORDINAL1:def 12;
set P1 = Permutations (N + 1);
defpred S₁[ object , object ] means for p being Element of Permutations (N + 1) st $1 = p & p . i = j holds
$2 = Rem (p,i);
let X be set ; :: thesis: ( X = { p1 where p1 is Element of Permutations (n + 1) : p1 . i = j } implies ex Proj being Function of X,(Permutations n) st
( Proj is bijective & ( for q1 being Element of Permutations (n + 1) st q1 . i = j holds
Proj . q1 = Rem (q1,i) ) ) )
assume A3: X = { p1 where p1 is Element of Permutations (n + 1) : p1 . i = j } ; :: thesis: ex Proj being Function of X,(Permutations n) st
( Proj is bijective & ( for q1 being Element of Permutations (n + 1) st q1 . i = j holds
Proj . q1 = Rem (q1,i) ) )
A4: for x being object st x in X holds
ex y being object st
( y in Permutations n & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in X implies ex y being object st
( y in Permutations n & S₁[x,y] ) )
assume x in X ; :: thesis: ex y being object st
( y in Permutations n & S₁[x,y] )
then consider p being Element of Permutations (N + 1) such that
A5: p = x and
p . i = j by A3;
take Rem (p,i) ; :: thesis: ( Rem (p,i) in Permutations n & S₁[x, Rem (p,i)] )
thus ( Rem (p,i) in Permutations n & S₁[x, Rem (p,i)] ) by A5; :: thesis: verum

end;

consider f being Function of X,(Permutations n) such that
A6: for x being object st x in X holds
S₁[x,f . x] from FUNCT_2:sch 1(A4);
for x1, x2 being object st x1 in X & x2 in X & f . x1 = f . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in X & x2 in X & f . x1 = f . x2 implies x1 = x2 )
assume that
A7: x1 in X and
A8: x2 in X and
A9: f . x1 = f . x2 ; :: thesis: x1 = x2
consider p1 being Element of Permutations (N + 1) such that
A10: p1 = x1 and
A11: p1 . i = j by A3, A7;
set R1 = Rem (p1,i);
A12: f . x1 = Rem (p1,i) by A6, A7, A10, A11;
consider p2 being Element of Permutations (N + 1) such that
A13: p2 = x2 and
A14: p2 . i = j by A3, A8;
set R2 = Rem (p2,i);
A15: f . x2 = Rem (p2,i) by A6, A8, A13, A14;
reconsider p19 = p1, p29 = p2 as Permutation of (Seg (n + 1)) by MATRIX_1:def 12;
A16: dom p29 = Seg (n + 1) by FUNCT_2:52;
A17: dom p19 = Seg (n + 1) by FUNCT_2:52;

now :: thesis: for x being object st x in Seg (n + 1) holds
p1 . x = p2 . x

let x be object ; :: thesis: ( x in Seg (n + 1) implies p1 . b₁ = p2 . b₁ )
assume A18: x in Seg (n + 1) ; :: thesis: p1 . b₁ = p2 . b₁
consider k being Nat such that
A19: x = k and
A20: 1 <= k and
A21: k <= n + 1 by A18;

per cases ( k < i or k = i or k > i ) by XXREAL_0:1;

suppose A22: k < i ; :: thesis: p1 . b₁ = p2 . b₁

i <= n + 1 by A1, FINSEQ_1:1;
then k < n + 1 by A22, XXREAL_0:2;
then k <= n by NAT_1:13;
then A23: k in Seg n by A20;

per cases ( ( p1 . k < j & p2 . k < j ) or ( p1 . k >= j & p2 . k >= j ) or ( p1 . k < j & p2 . k >= j ) or ( p1 . k >= j & p2 . k < j ) ) ;

suppose ( ( p1 . k < j & p2 . k < j ) or ( p1 . k >= j & p2 . k >= j ) ) ; :: thesis: p1 . b₁ = p2 . b₁

then ( ( (Rem (p1,i)) . k = p1 . k & (Rem (p2,i)) . k = p2 . k ) or ( (Rem (p1,i)) . k = (p1 . k) - 1 & (Rem (p2,i)) . k = (p2 . k) - 1 ) ) by A1, A11, A14, A22, A23, Def3;
hence p1 . x = p2 . x by A9, A12, A15, A19; :: thesis: verum

end;

suppose ( ( p1 . k < j & p2 . k >= j ) or ( p1 . k >= j & p2 . k < j ) ) ; :: thesis: p1 . b₁ = p2 . b₁

then ( ( (Rem (p1,i)) . k = p1 . k & (Rem (p2,i)) . k = (p2 . k) - 1 & p1 . k < j & p2 . k >= j ) or ( (Rem (p1,i)) . k = (p1 . k) - 1 & (Rem (p2,i)) . k = p2 . k & p1 . k >= j & p2 . k < j ) ) by A1, A11, A14, A22, A23, Def3;
then ( ( (p1 . k) + 1 = p2 . k & p1 . k < j & p2 . k >= j ) or ( p1 . k = (p2 . k) + 1 & p1 . k >= j & p2 . k < j ) ) by A9, A12, A15;
then ( ( p2 . k <= j & p2 . k >= j ) or ( p1 . k >= j & p1 . k <= j ) ) by NAT_1:13;
then ( p29 . k = p29 . i or p19 . k = p19 . i ) by A11, A14, XXREAL_0:1;
hence p1 . x = p2 . x by A1, A17, A16, A18, A19, A22, FUNCT_1:def 4; :: thesis: verum

end;

end;

end;

suppose k = i ; :: thesis: p1 . b₁ = p2 . b₁

hence p1 . x = p2 . x by A11, A14, A19; :: thesis: verum

end;

suppose A24: k > i ; :: thesis: p1 . b₁ = p2 . b₁

then reconsider k1 = k - 1 as Element of NAT by NAT_1:20;
k1 + 1 > i by A24;
then A25: k1 >= i by NAT_1:13;
k1 + 1 <= n + 1 by A21;
then k1 < n + 1 by NAT_1:13;
then A26: k1 <= n by NAT_1:13;
1 <= i by A1, FINSEQ_1:1;
then 1 < k1 + 1 by A24, XXREAL_0:2;
then 1 <= k1 by NAT_1:13;
then A27: k1 in Seg n by A26;

per cases ( ( p1 . (k1 + 1) < j & p2 . (k1 + 1) < j ) or ( p1 . (k1 + 1) >= j & p2 . (k1 + 1) >= j ) or ( p1 . (k1 + 1) < j & p2 . (k1 + 1) >= j ) or ( p1 . (k1 + 1) >= j & p2 . (k1 + 1) < j ) ) ;

suppose ( ( p1 . (k1 + 1) < j & p2 . (k1 + 1) < j ) or ( p1 . (k1 + 1) >= j & p2 . (k1 + 1) >= j ) ) ; :: thesis: p1 . b₁ = p2 . b₁

then ( ( (Rem (p1,i)) . k1 = p1 . k & (Rem (p2,i)) . k1 = p2 . k ) or ( (Rem (p1,i)) . k1 = (p1 . k) - 1 & (Rem (p2,i)) . k1 = (p2 . k) - 1 ) ) by A1, A11, A14, A27, A25, Def3;
hence p1 . x = p2 . x by A9, A12, A15, A19; :: thesis: verum

end;

suppose ( ( p1 . (k1 + 1) < j & p2 . (k1 + 1) >= j ) or ( p1 . (k1 + 1) >= j & p2 . (k1 + 1) < j ) ) ; :: thesis: p1 . b₁ = p2 . b₁

then ( ( (Rem (p1,i)) . k1 = p1 . k & (Rem (p2,i)) . k1 = (p2 . k) - 1 & p1 . k < j & p2 . k >= j ) or ( (Rem (p1,i)) . k1 = (p1 . k) - 1 & (Rem (p2,i)) . k1 = p2 . k & p1 . k >= j & p2 . k < j ) ) by A1, A11, A14, A27, A25, Def3;
then ( ( (p1 . k) + 1 = p2 . k & p1 . k < j & p2 . k >= j ) or ( p1 . k = (p2 . k) + 1 & p1 . k >= j & p2 . k < j ) ) by A9, A12, A15;
then ( ( p2 . k <= j & p2 . k >= j ) or ( p1 . k >= j & p1 . k <= j ) ) by NAT_1:13;
then ( p29 . k = p29 . i or p19 . k = p19 . i ) by A11, A14, XXREAL_0:1;
hence p1 . x = p2 . x by A1, A17, A16, A18, A19, A24, FUNCT_1:def 4; :: thesis: verum

end;

end;

end;

end;

end;

hence x1 = x2 by A10, A13, A17, A16, FUNCT_1:2; :: thesis: verum

end;

then A28: f is one-to-one by FUNCT_2:19;
set P = Permutations N;
card X = N ! by A1, A2, A3, Th7;
then reconsider P9 = Permutations N, X9 = X as finite set ;
take f ; :: thesis: ( f is bijective & ( for q1 being Element of Permutations (n + 1) st q1 . i = j holds
f . q1 = Rem (q1,i) ) )
A30: card P9 = n ! by Th6;
card X9 = n ! by A1, A2, A3, Th7;
then ( f is onto & f is one-to-one ) by A28, A30, FINSEQ_4:63;
hence f is bijective ; :: thesis: for q1 being Element of Permutations (n + 1) st q1 . i = j holds
f . q1 = Rem (q1,i)
let p be Element of Permutations (n + 1); :: thesis: ( p . i = j implies f . p = Rem (p,i) )
assume A31: p . i = j ; :: thesis: f . p = Rem (p,i)
p in X by A3, A31;
hence f . p = Rem (p,i) by A6, A31; :: thesis: verum