let n, q be Nat; :: thesis:
defpred S₁[ 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:
A2: for i being Nat st i in Seg (n + 1) holds
ex p being Element of NAT st S₁[i,p]

let i be Nat; :: thesis:
assume i in Seg (n + 1) ; :: thesis:

suppose A3: i < q ; :: thesis:

take i ; :: thesis:
i in NAT by ORDINAL1:def 12;
hence ( i is Element of NAT & S₁[i,i] ) by A3; :: thesis:

end;

suppose A4: i = q ; :: thesis:

take n + 1 ; :: thesis:
thus S₁[i,n + 1] by A4; :: thesis:

end;

suppose A5: i > q ; :: thesis:

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:
thus S₁[i,p] by A5; :: thesis:

end;

consider p being FinSequence of NAT such that
A6: dom p = Seg (n + 1) and
A7: for i being Nat st i in Seg (n + 1) holds
S₁[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 )

proof

let i be Element of NAT ; :: thesis:
assume A9: i in Seg (n + 1) ; :: thesis:
hence ( i = q implies p /. i = n + 1 ) by A7; :: thesis:
thus ( p /. i = n + 1 implies i = q ) :: thesis:

proof

assume A10: p /. i = n + 1 ; :: thesis:

per cases by XXREAL_0:1;

suppose i = q ; :: thesis:

hence i = q ; :: thesis:

end;

suppose i < q ; :: thesis:

then n + 1 < q by A7, A9, A10;
hence i = q by A1, FINSEQ_1:1; :: thesis:

end;

suppose i > q ; :: thesis:

then i - 1 = n + 1 by A7, A9, A10;
then i >= (n + 1) + 1 ;
then i > n + 1 by NAT_1:13;
hence i = q by A9, FINSEQ_1:1; :: thesis:

end;

A11: 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 ) )

proof

let i be Element of NAT ; :: thesis:
assume A12: i in Seg (n + 1) ; :: thesis:
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:

end;

for i being object holds
( i in rng p iff i in Seg (n + 1) )

proof

let i be object ; :: thesis:
thus ( i in rng p implies i in Seg (n + 1) ) :: thesis:

proof

assume i in rng p ; :: thesis:
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 by XXREAL_0:1;

suppose j < q ; :: thesis:

hence i in Seg (n + 1) by A11, A13, A14; :: thesis:

end;

suppose j = q ; :: thesis:

then i = n + 1 by A11, A13, A14;
hence i in Seg (n + 1) by FINSEQ_1:4; :: thesis:

end;

suppose A15: j > q ; :: thesis:

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:

end;

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

proof

assume A19: i in Seg (n + 1) ; :: thesis:
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 by A20, NAT_1:13;

suppose i < q ; :: thesis:

then p . i = i by A11, A19;
hence i in rng p by A6, A19, FUNCT_1:3; :: thesis:

end;

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

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:

end;

suppose i = n + 1 ; :: thesis:

then p . q = i by A1, A11;
hence i in rng p by A1, A6, FUNCT_1:3; :: thesis:

end;

then A24: rng p = Seg (n + 1) by TARSKI:2;
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

let i be Element of NAT ; :: thesis:
assume that
A27: i in Seg (n + 1) and
A28: p /. i <> n + 1 ; :: thesis:
thus ( i < q implies p /. i < q ) by A7, A27; :: thesis:
thus ( p /. i < q implies i < q ) :: thesis:

proof

assume A29: p /. i < q ; :: thesis:

per cases by XXREAL_0:1;

suppose i < q ; :: thesis:

hence i < q ; :: thesis:

end;

suppose i = q ; :: thesis:

hence i < q by A7, A27, A28; :: thesis:

end;

suppose A30: i > q ; :: thesis:

then p /. i = i - 1 by A7, A27;
then (i - 1) + 1 < q + 1 by A29, XREAL_1:8;
hence i < q by A30, NAT_1:13; :: thesis:

end;

for i1, i2 being object st i1 in Seg (n + 1) & i2 in Seg (n + 1) & p . i1 = p . i2 holds
i1 = i2

proof

let i1, i2 be object ; :: thesis:
assume that
A31: i1 in Seg (n + 1) and
A32: i2 in Seg (n + 1) and
A33: p . i1 = p . i2 ; :: thesis:
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 ;

suppose A36: p /. i1 = n + 1 ; :: thesis:

then i1 = q by A8, A31;
hence i1 = i2 by A8, A32, A33, A34, A35, A36; :: thesis:

end;

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

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:

end;

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

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:

end;

then p is one-to-one by A6, FUNCT_1:def 4;
then reconsider p = p as Permutation of (Seg (n + 1)) by A24, A25, FUNCT_2:57;
take p ; :: thesis:
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: