let n, q be Nat; :: thesis: ( q in Seg (n + 1) implies ex p being Permutation of (Seg (n + 1)) st

for i being Element of NAT st i in Seg (n + 1) holds

( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) ) )

defpred S_{1}[ Nat, set ] means ( ( $1 < q implies $2 = $1 ) & ( $1 = q implies $2 = n + 1 ) & ( $1 > q implies $2 = $1 - 1 ) );

assume A1: q in Seg (n + 1) ; :: thesis: ex p being Permutation of (Seg (n + 1)) st

for i being Element of NAT st i in Seg (n + 1) holds

( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) )

A2: for i being Nat st i in Seg (n + 1) holds

ex p being Element of NAT st S_{1}[i,p]

A6: dom p = Seg (n + 1) and

A7: for i being Nat st i in Seg (n + 1) holds

S_{1}[i,p /. i]
from RECDEF_1:sch 17(A2);

A8: for i being Element of NAT st i in Seg (n + 1) holds

( i = q iff p /. i = n + 1 )

( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) )

( i in rng p iff i in Seg (n + 1) )

then A25: p is Function of (Seg (n + 1)),(Seg (n + 1)) by A6, FUNCT_2:1;

A26: for i being Element of NAT st i in Seg (n + 1) & p /. i <> n + 1 holds

( i < q iff p /. i < q )

i1 = i2

then reconsider p = p as Permutation of (Seg (n + 1)) by A24, A25, FUNCT_2:57;

take p ; :: thesis: for i being Element of NAT st i in Seg (n + 1) holds

( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) )

thus for i being Element of NAT st i in Seg (n + 1) holds

( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) ) by A11; :: thesis: verum

for i being Element of NAT st i in Seg (n + 1) holds

( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) ) )

defpred S

assume A1: q in Seg (n + 1) ; :: thesis: ex p being Permutation of (Seg (n + 1)) st

for i being Element of NAT st i in Seg (n + 1) holds

( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) )

A2: for i being Nat st i in Seg (n + 1) holds

ex p being Element of NAT st S

proof

consider p being FinSequence of NAT such that
let i be Nat; :: thesis: ( i in Seg (n + 1) implies ex p being Element of NAT st S_{1}[i,p] )

assume i in Seg (n + 1) ; :: thesis: ex p being Element of NAT st S_{1}[i,p]

end;assume i in Seg (n + 1) ; :: thesis: ex p being Element of NAT st S

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

end;

suppose A3:
i < q
; :: thesis: ex p being Element of NAT st S_{1}[i,p]

take
i
; :: thesis: ( i is Element of NAT & S_{1}[i,i] )

i in NAT by ORDINAL1:def 12;

hence ( i is Element of NAT & S_{1}[i,i] )
by A3; :: thesis: verum

end;i in NAT by ORDINAL1:def 12;

hence ( i is Element of NAT & S

suppose A5:
i > q
; :: thesis: ex p being Element of NAT st S_{1}[i,p]

1 <= q
by A1, FINSEQ_1:1;

then reconsider p = i - 1 as Element of NAT by A5, INT_1:5, XXREAL_0:2;

take p ; :: thesis: S_{1}[i,p]

thus S_{1}[i,p]
by A5; :: thesis: verum

end;then reconsider p = i - 1 as Element of NAT by A5, INT_1:5, XXREAL_0:2;

take p ; :: thesis: S

thus S

A6: dom p = Seg (n + 1) and

A7: for i being Nat st i in Seg (n + 1) holds

S

A8: for i being Element of NAT st i in Seg (n + 1) holds

( i = q iff p /. i = n + 1 )

proof

A11:
for i being Element of NAT st i in Seg (n + 1) holds
let i be Element of NAT ; :: thesis: ( i in Seg (n + 1) implies ( i = q iff p /. i = n + 1 ) )

assume A9: i in Seg (n + 1) ; :: thesis: ( i = q iff p /. i = n + 1 )

hence ( i = q implies p /. i = n + 1 ) by A7; :: thesis: ( p /. i = n + 1 implies i = q )

thus ( p /. i = n + 1 implies i = q ) :: thesis: verum

end;assume A9: i in Seg (n + 1) ; :: thesis: ( i = q iff p /. i = n + 1 )

hence ( i = q implies p /. i = n + 1 ) by A7; :: thesis: ( p /. i = n + 1 implies i = q )

thus ( p /. i = n + 1 implies i = q ) :: thesis: verum

( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) )

proof

for i being object holds
let i be Element of NAT ; :: thesis: ( i in Seg (n + 1) implies ( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) ) )

assume A12: i in Seg (n + 1) ; :: thesis: ( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) )

then p /. i = p . i by A6, PARTFUN1:def 6;

hence ( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) ) by A7, A12; :: thesis: verum

end;assume A12: i in Seg (n + 1) ; :: thesis: ( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) )

then p /. i = p . i by A6, PARTFUN1:def 6;

hence ( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) ) by A7, A12; :: thesis: verum

( i in rng p iff i in Seg (n + 1) )

proof

then A24:
rng p = Seg (n + 1)
by TARSKI:2;
let i be object ; :: thesis: ( i in rng p iff i in Seg (n + 1) )

thus ( i in rng p implies i in Seg (n + 1) ) :: thesis: ( i in Seg (n + 1) implies i in rng p )

end;thus ( i in rng p implies i in Seg (n + 1) ) :: thesis: ( i in Seg (n + 1) implies i in rng p )

proof

thus
( i in Seg (n + 1) implies i in rng p )
:: thesis: verum
assume
i in rng p
; :: thesis: i in Seg (n + 1)

then consider j being object such that

A13: j in Seg (n + 1) and

A14: p . j = i by A6, FUNCT_1:def 3;

reconsider j = j as Element of NAT by A13;

end;then consider j being object such that

A13: j in Seg (n + 1) and

A14: p . j = i by A6, FUNCT_1:def 3;

reconsider j = j as Element of NAT by A13;

per cases
( j < q or j = q or j > q )
by XXREAL_0:1;

end;

suppose A15:
j > q
; :: thesis: i in Seg (n + 1)

then A16:
i = j - 1
by A11, A13, A14;

A17: 1 <= q by A1, FINSEQ_1:1;

then reconsider i = i as Element of NAT by A15, A16, INT_1:5, XXREAL_0:2;

j <= n + 1 by A13, FINSEQ_1:1;

then i <= n by A16, XREAL_1:20;

then A18: i <= n + 1 by NAT_1:12;

1 < i + 1 by A15, A16, A17, XXREAL_0:2;

then 1 <= i by NAT_1:13;

hence i in Seg (n + 1) by A18, FINSEQ_1:1; :: thesis: verum

end;A17: 1 <= q by A1, FINSEQ_1:1;

then reconsider i = i as Element of NAT by A15, A16, INT_1:5, XXREAL_0:2;

j <= n + 1 by A13, FINSEQ_1:1;

then i <= n by A16, XREAL_1:20;

then A18: i <= n + 1 by NAT_1:12;

1 < i + 1 by A15, A16, A17, XXREAL_0:2;

then 1 <= i by NAT_1:13;

hence i in Seg (n + 1) by A18, FINSEQ_1:1; :: thesis: verum

proof

assume A19:
i in Seg (n + 1)
; :: thesis: i in rng p

then reconsider i = i as Element of NAT ;

i <= n + 1 by A19, FINSEQ_1:1;

then A20: ( i = n + 1 or i < n + 1 ) by XXREAL_0:1;

end;then reconsider i = i as Element of NAT ;

i <= n + 1 by A19, FINSEQ_1:1;

then A20: ( i = n + 1 or i < n + 1 ) by XXREAL_0:1;

per cases
( i < q or ( q <= i & i <= n ) or i = n + 1 )
by A20, NAT_1:13;

end;

suppose A21:
( q <= i & i <= n )
; :: thesis: i in rng p

A22:
1 <= i + 1
by NAT_1:12;

i + 1 <= n + 1 by A21, XREAL_1:6;

then A23: i + 1 in Seg (n + 1) by A22, FINSEQ_1:1;

q < i + 1 by A21, NAT_1:13;

then p . (i + 1) = (i + 1) - 1 by A11, A23

.= i ;

hence i in rng p by A6, A23, FUNCT_1:3; :: thesis: verum

end;i + 1 <= n + 1 by A21, XREAL_1:6;

then A23: i + 1 in Seg (n + 1) by A22, FINSEQ_1:1;

q < i + 1 by A21, NAT_1:13;

then p . (i + 1) = (i + 1) - 1 by A11, A23

.= i ;

hence i in rng p by A6, A23, FUNCT_1:3; :: thesis: verum

then A25: p is Function of (Seg (n + 1)),(Seg (n + 1)) by A6, FUNCT_2:1;

A26: for i being Element of NAT st i in Seg (n + 1) & p /. i <> n + 1 holds

( i < q iff p /. i < q )

proof

for i1, i2 being object st i1 in Seg (n + 1) & i2 in Seg (n + 1) & p . i1 = p . i2 holds
let i be Element of NAT ; :: thesis: ( i in Seg (n + 1) & p /. i <> n + 1 implies ( i < q iff p /. i < q ) )

assume that

A27: i in Seg (n + 1) and

A28: p /. i <> n + 1 ; :: thesis: ( i < q iff p /. i < q )

thus ( i < q implies p /. i < q ) by A7, A27; :: thesis: ( p /. i < q implies i < q )

thus ( p /. i < q implies i < q ) :: thesis: verum

end;assume that

A27: i in Seg (n + 1) and

A28: p /. i <> n + 1 ; :: thesis: ( i < q iff p /. i < q )

thus ( i < q implies p /. i < q ) by A7, A27; :: thesis: ( p /. i < q implies i < q )

thus ( p /. i < q implies i < q ) :: thesis: verum

i1 = i2

proof

then
p is one-to-one
by A6, FUNCT_1:def 4;
let i1, i2 be object ; :: thesis: ( i1 in Seg (n + 1) & i2 in Seg (n + 1) & p . i1 = p . i2 implies i1 = i2 )

assume that

A31: i1 in Seg (n + 1) and

A32: i2 in Seg (n + 1) and

A33: p . i1 = p . i2 ; :: thesis: i1 = i2

reconsider i1 = i1 as Element of NAT by A31;

A34: p /. i1 = p . i1 by A6, A31, PARTFUN1:def 6;

reconsider i2 = i2 as Element of NAT by A32;

A35: p /. i2 = p . i2 by A6, A32, PARTFUN1:def 6;

end;assume that

A31: i1 in Seg (n + 1) and

A32: i2 in Seg (n + 1) and

A33: p . i1 = p . i2 ; :: thesis: i1 = i2

reconsider i1 = i1 as Element of NAT by A31;

A34: p /. i1 = p . i1 by A6, A31, PARTFUN1:def 6;

reconsider i2 = i2 as Element of NAT by A32;

A35: p /. i2 = p . i2 by A6, A32, PARTFUN1:def 6;

per cases
( p /. i1 = n + 1 or ( p /. i1 <> n + 1 & p /. i1 < q ) or ( p /. i1 <> n + 1 & p /. i1 >= q ) )
;

end;

suppose A37:
( p /. i1 <> n + 1 & p /. i1 < q )
; :: thesis: i1 = i2

then
i1 < q
by A26, A31;

then A38: p /. i1 = i1 by A7, A31;

i2 < q by A26, A32, A33, A34, A35, A37;

hence i1 = i2 by A7, A32, A33, A34, A35, A38; :: thesis: verum

end;then A38: p /. i1 = i1 by A7, A31;

i2 < q by A26, A32, A33, A34, A35, A37;

hence i1 = i2 by A7, A32, A33, A34, A35, A38; :: thesis: verum

suppose A39:
( p /. i1 <> n + 1 & p /. i1 >= q )
; :: thesis: i1 = i2

then A40:
i1 <> q
by A8, A31;

i1 >= q by A26, A31, A39;

then i1 > q by A40, XXREAL_0:1;

then A41: p /. i1 = i1 - 1 by A7, A31;

A42: i2 <> q by A8, A32, A33, A34, A35, A39;

i2 >= q by A26, A32, A33, A34, A35, A39;

then i2 > q by A42, XXREAL_0:1;

then p /. i2 = i2 - 1 by A7, A32;

hence i1 = i2 by A6, A32, A33, A34, A41, PARTFUN1:def 6, XCMPLX_1:19; :: thesis: verum

end;i1 >= q by A26, A31, A39;

then i1 > q by A40, XXREAL_0:1;

then A41: p /. i1 = i1 - 1 by A7, A31;

A42: i2 <> q by A8, A32, A33, A34, A35, A39;

i2 >= q by A26, A32, A33, A34, A35, A39;

then i2 > q by A42, XXREAL_0:1;

then p /. i2 = i2 - 1 by A7, A32;

hence i1 = i2 by A6, A32, A33, A34, A41, PARTFUN1:def 6, XCMPLX_1:19; :: thesis: verum

then reconsider p = p as Permutation of (Seg (n + 1)) by A24, A25, FUNCT_2:57;

take p ; :: thesis: for i being Element of NAT st i in Seg (n + 1) holds

( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) )

thus for i being Element of NAT st i in Seg (n + 1) holds

( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) ) by A11; :: thesis: verum