let n, q be Nat; :: thesis:
let s, p be Permutation of (Seg (n + 1)); :: thesis:
let s9 be FinSequence of Seg (n + 1); :: thesis:
assume that
A1: s9 = s and
A2: q = s . (n + 1) and
A3: 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 ) ) ; :: thesis:
A4: dom p = Seg (n + 1) by FUNCT_2:def 1;
reconsider r = p * (s9 | n) as FinSequence of Seg (n + 1) by FINSEQ_2:32;
A5: 0 + n <= 1 + n by XREAL_1:6;
then A6: Seg n c= Seg (n + 1) by FINSEQ_1:5;
s9 | n = s9 | (Seg n) by FINSEQ_1:def 16;
then A7: s9 | n is one-to-one by A1, FUNCT_1:52;
A8: rng p = Seg (n + 1) by FUNCT_2:def 3;
A9: dom s = Seg (n + 1) by FUNCT_2:def 1;
then len s9 = n + 1 by A1, FINSEQ_1:def 3;
then len (s9 | n) = n by A5, FINSEQ_1:59;
then len r = n by FINSEQ_2:33;
then A10: dom r = Seg n by FINSEQ_1:def 3;
A11: rng s = Seg (n + 1) by FUNCT_2:def 3;
then q in Seg (n + 1) by A2, A9, FINSEQ_1:4, FUNCT_1:3;
then A12: q <= n + 1 by FINSEQ_1:1;
aaa: rng r c= Seg (n + 1) by RELAT_1:def 19;
for i being object holds
( i in rng r iff i in Seg n )

proof

let i be object ; :: thesis:
thus ( i in rng r implies i in Seg n ) :: thesis:

proof

assume bbb: i in rng r ; :: thesis:
then consider j being object such that
A13: j in Seg n and
A14: r . j = i by A10, FUNCT_1:def 3;
reconsider j = j as Element of NAT by A13;
A15: j <= n by A13, FINSEQ_1:1;
then A16: (s9 | n) . j = s . j by A1, FINSEQ_3:112;
then A17: i = p . (s . j) by A10, A13, A14, FUNCT_1:12;
s . j in dom p by A9, A11, A4, A6, A13, FUNCT_1:3;
then p . (s . j) in rng p by FUNCT_1:3;
then reconsider i = i as Element of NAT by A8, A10, A13, A14, A16, FUNCT_1:12;
A19: n + 1 in dom s by A9, FINSEQ_1:4;
A20: s . j in Seg (n + 1) by A9, A11, A6, A13, FUNCT_1:3;
then reconsider q1 = s . j as Element of NAT ;
j < n + 1 by A15, NAT_1:13;
then A21: q1 <> q by A2, A9, A6, A13, A19, FUNCT_1:def 4;

per cases by A21, XXREAL_0:1;

suppose q1 < q ; :: thesis:

then i < q by A3, A17, A20;
then i < n + 1 by A12, XXREAL_0:2;
then A22: i <= n by NAT_1:13;
1 <= i by bbb, aaa, FINSEQ_1:1;
hence i in Seg n by A22, FINSEQ_1:1; :: thesis:

end;

suppose A23: q1 > q ; :: thesis:

A24: q1 <= n + 1 by A20, FINSEQ_1:1;
i = q1 - 1 by A3, A17, A20, A23;
then A25: i <= n by A24, XREAL_1:20;
1 <= i by bbb, aaa, FINSEQ_1:1;
hence i in Seg n by A25, FINSEQ_1:1; :: thesis:

end;

end;

end;

assume A26: i in Seg n ; :: thesis:
then reconsider i = i as Element of NAT ;

per cases ;

suppose A27: i < q ; :: thesis:

then A28: p . i = i by A3, A6, A26;
consider j being object such that
A29: j in dom s and
A30: i = s . j by A11, A6, A26, FUNCT_1:def 3;
j in Seg (n + 1) by A29;
then reconsider j = j as Element of NAT ;
j <= n + 1 by A29, FINSEQ_1:1;
then j < n + 1 by A2, A27, A30, XXREAL_0:1;
then A31: j <= n by NAT_1:13;
1 <= j by A29, FINSEQ_1:1;
then A32: j in dom r by A10, A31, FINSEQ_1:1;
(s9 | n) . j = s . j by A1, A31, FINSEQ_3:112;
then r . j = i by A28, A30, A32, FUNCT_1:12;
hence i in rng r by A32, FUNCT_1:3; :: thesis:

end;

suppose A33: i >= q ; :: thesis:

i <= n by A26, FINSEQ_1:1;
then A34: i + 1 <= n + 1 by XREAL_1:6;
1 <= i + 1 by NAT_1:12;
then A35: i + 1 in Seg (n + 1) by A34, FINSEQ_1:1;
then consider j being object such that
A36: j in dom s and
A37: i + 1 = s . j by A11, FUNCT_1:def 3;
j in Seg (n + 1) by A36;
then reconsider j = j as Element of NAT ;
A38: j <= n + 1 by A36, FINSEQ_1:1;
j <> n + 1 by A2, A33, A37, NAT_1:13;
then j < n + 1 by A38, XXREAL_0:1;
then A39: j <= n by NAT_1:13;
1 <= j by A36, FINSEQ_1:1;
then A40: j in Seg n by A39, FINSEQ_1:1;
i + 1 > q by A33, NAT_1:13;
then A41: p . (i + 1) = (i + 1) - 1 by A3, A35
.= i ;
(s9 | n) . j = s . j by A1, A39, FINSEQ_3:112;
then r . j = p . (s . j) by A10, A40, FUNCT_1:12;
hence i in rng r by A10, A37, A41, A40, FUNCT_1:3; :: thesis:

end;

end;

end;

then A42: rng r = Seg n by TARSKI:2;
then p * (s9 | n) is Function of (Seg n),(Seg n) by A10, FUNCT_2:1;
hence p * (s9 | n) is Permutation of (Seg n) by A42, A7, FUNCT_2:57; :: thesis: