let n, i, j be Nat; ( 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)
; 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 S1[ 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 ; ( 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 }
; 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 & S1[x,y] )
consider f being Function of X,(Permutations n) such that
A6:
for x being object st x in X holds
S1[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 ;
( 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
;
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 for x being object st x in Seg (n + 1) holds
p1 . x = p2 . xlet x be
object ;
( x in Seg (n + 1) implies p1 . b1 = p2 . b1 )assume A18:
x in Seg (n + 1)
;
p1 . b1 = p2 . b1consider 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
;
p1 . b1 = p2 . b1
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 ) )
;
p1 . b1 = p2 . b1then
( (
(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;
verum end; suppose
( (
p1 . k < j &
p2 . k >= j ) or (
p1 . k >= j &
p2 . k < j ) )
;
p1 . b1 = p2 . b1then
( (
(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;
verum end; end; end; suppose A24:
k > i
;
p1 . b1 = p2 . b1then 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 ) )
;
p1 . b1 = p2 . b1then
( (
(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;
verum end; suppose
( (
p1 . (k1 + 1) < j &
p2 . (k1 + 1) >= j ) or (
p1 . (k1 + 1) >= j &
p2 . (k1 + 1) < j ) )
;
p1 . b1 = p2 . b1then
( (
(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;
verum end; end; end; end; end;
hence
x1 = x2
by A10, A13, A17, A16, FUNCT_1:2;
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
; ( 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
; 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); ( p . i = j implies f . p = Rem (p,i) )
assume A31:
p . i = j
; f . p = Rem (p,i)
p in X
by A3, A31;
hence
f . p = Rem (p,i)
by A6, A31; verum