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_{1}[ 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_{1}[x,y] )

A6: for x being object st x in X holds

S_{1}[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

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

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

$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

proof

consider f being Function of X,(Permutations n) such that
let x be object ; :: thesis: ( x in X implies ex y being object st

( y in Permutations n & S_{1}[x,y] ) )

assume x in X ; :: thesis: ex y being object st

( y in Permutations n & S_{1}[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_{1}[x, Rem (p,i)] )

thus ( Rem (p,i) in Permutations n & S_{1}[x, Rem (p,i)] )
by A5; :: thesis: verum

end;( y in Permutations n & S

assume x in X ; :: thesis: ex y being object st

( y in Permutations n & S

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

thus ( Rem (p,i) in Permutations n & S

A6: for x being object st x in X holds

S

for x1, x2 being object st x1 in X & x2 in X & f . x1 = f . x2 holds

x1 = x2

proof

then A28:
f is one-to-one
by FUNCT_2:19;
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;

end;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

hence
x1 = x2
by A10, A13, A17, A16, FUNCT_1:2; :: thesis: verump1 . x = p2 . x

let x be object ; :: thesis: ( x in Seg (n + 1) implies p1 . b_{1} = p2 . b_{1} )

assume A18: x in Seg (n + 1) ; :: thesis: p1 . b_{1} = p2 . b_{1}

consider k being Nat such that

A19: x = k and

A20: 1 <= k and

A21: k <= n + 1 by A18;

end;assume A18: x in Seg (n + 1) ; :: thesis: p1 . 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;

end;

suppose A22:
k < i
; :: thesis: p1 . b_{1} = p2 . b_{1}

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;

end;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 ) )
;

end;

suppose
( ( p1 . k < j & p2 . k < j ) or ( p1 . k >= j & p2 . k >= j ) )
; :: thesis: p1 . b_{1} = p2 . b_{1}

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;hence p1 . x = p2 . x by A9, A12, A15, A19; :: thesis: verum

suppose
( ( p1 . k < j & p2 . k >= j ) or ( p1 . k >= j & p2 . k < j ) )
; :: thesis: p1 . b_{1} = p2 . b_{1}

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;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

suppose A24:
k > i
; :: thesis: p1 . b_{1} = p2 . b_{1}

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;

end;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 ) )
;

end;

suppose
( ( p1 . (k1 + 1) < j & p2 . (k1 + 1) < j ) or ( p1 . (k1 + 1) >= j & p2 . (k1 + 1) >= j ) )
; :: thesis: p1 . b_{1} = p2 . b_{1}

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;hence p1 . x = p2 . x by A9, A12, A15, A19; :: thesis: verum

suppose
( ( p1 . (k1 + 1) < j & p2 . (k1 + 1) >= j ) or ( p1 . (k1 + 1) >= j & p2 . (k1 + 1) < j ) )
; :: thesis: p1 . b_{1} = p2 . b_{1}

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;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

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