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 A1: ( i in Seg (n + 1) & 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 ) )
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 A2: 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 ) )
reconsider N = n as Element of NAT by ORDINAL1:def 13;
set P1 = Permutations (N + 1);
set P = Permutations N;
set n1 = n + 1;
defpred S₁[ set , set ] means for p being Element of Permutations (N + 1) st $1 = p & p . i = j holds
$2 = Rem p,i;
A3: for x being set st x in X holds
ex y being set st
( y in Permutations n & S₁[x,y] )

proof

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

end;

consider f being Function of X,(Permutations n) such that
A5: for x being set st x in X holds
S₁[x,f . x] from FUNCT_2:sch 1(A3);
take f ; :: thesis: ( f is bijective & ( for q1 being Element of Permutations (n + 1) st q1 . i = j holds
f . q1 = Rem q1,i ) )
A6: for x1, x2 being set st x1 in X & x2 in X & f . x1 = f . x2 holds
x1 = x2

proof

let x1, x2 be set ; :: thesis: ( x1 in X & x2 in X & f . x1 = f . x2 implies x1 = x2 )
assume A7: ( x1 in X & x2 in X & f . x1 = f . x2 ) ; :: thesis: x1 = x2
consider p1 being Element of Permutations (N + 1) such that
A8: ( p1 = x1 & p1 . i = j ) by A2, A7;
consider p2 being Element of Permutations (N + 1) such that
A9: ( p2 = x2 & p2 . i = j ) by A2, A7;
set R1 = Rem p1,i;
set R2 = Rem p2,i;
A10: ( f . x1 = Rem p1,i & f . x2 = Rem p2,i ) by A5, A7, A8, A9;
reconsider p1' = p1, p2' = p2 as Permutation of (Seg (n + 1)) by MATRIX_2:def 11;
A11: ( dom p1' = Seg (n + 1) & dom p2' = Seg (n + 1) ) by FUNCT_2:67;

now

let x be set ; :: thesis: ( x in Seg (n + 1) implies p1 . b₁ = p2 . b₁ )
assume A12: x in Seg (n + 1) ; :: thesis: p1 . b₁ = p2 . b₁
consider k being Element of NAT such that
A13: ( x = k & 1 <= k & k <= n + 1 ) by A12;

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

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

i <= n + 1 by A1, FINSEQ_1:3;
then k < n + 1 by A14, XXREAL_0:2;
then k <= n by NAT_1:13;
then A15: k in Seg n by A13;

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, A8, A9, A14, A15, Def3;
hence p1 . x = p2 . x by A7, A10, A13; :: 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, A8, A9, A14, A15, 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 A7, A10;
then ( ( p2 . k <= j & p2 . k >= j ) or ( p1 . k >= j & p1 . k <= j ) ) by NAT_1:13;
then ( p2' . k = p2' . i or p1' . k = p1' . i ) by A8, A9, XXREAL_0:1;
hence p1 . x = p2 . x by A1, A11, A12, A13, A14, FUNCT_1:def 8; :: thesis: verum

end;

end;

end;

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

hence p1 . x = p2 . x by A8, A9, A13; :: thesis: verum

end;

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

then reconsider k1 = k - 1 as Element of NAT by NAT_1:20;
( 1 <= i & k1 + 1 <= n + 1 ) by A1, A13, FINSEQ_1:3;
then ( 1 < k1 + 1 & k1 < n + 1 ) by A16, NAT_1:13, XXREAL_0:2;
then ( 1 <= k1 & k1 <= n & k1 + 1 > i ) by A16, NAT_1:13;
then A17: ( k1 in Seg n & k1 >= i ) by NAT_1:13;

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, A8, A9, A17, Def3;
hence p1 . x = p2 . x by A7, A10, A13; :: 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, A8, A9, A17, 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 A7, A10;
then ( ( p2 . k <= j & p2 . k >= j ) or ( p1 . k >= j & p1 . k <= j ) ) by NAT_1:13;
then ( p2' . k = p2' . i or p1' . k = p1' . i ) by A8, A9, XXREAL_0:1;
hence p1 . x = p2 . x by A1, A11, A12, A13, A16, FUNCT_1:def 8; :: thesis: verum

end;

end;

end;

end;

end;

hence x1 = x2 by A8, A9, A11, FUNCT_1:9; :: thesis: verum

end;

( card (Permutations N) = N ! & card X = N ! ) by A1, A2, Th6, Th7;
then reconsider P' = Permutations N, X' = X as finite set ;
( f is one-to-one & card P' = n ! & card X' = n ! ) by A1, A2, A6, Th6, Th7, FUNCT_2:25;
then ( f is onto & f is one-to-one ) by STIRL2_1:70;
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 A18: p . i = j ; :: thesis: f . p = Rem p,i
p in X by A2, A18;
hence f . p = Rem p,i by A5, A18; :: thesis: verum