let n, q be Nat; :: thesis:
let s, p be Permutation of (Seg (n + 1)); :: thesis:
let s' be FinSequence of Seg (n + 1); :: thesis:
assume that
A1: s' = 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:
A5: ( dom s = Seg (n + 1) & rng s = Seg (n + 1) ) by FUNCT_2:def 1, FUNCT_2:def 3;
then A6: len s' = n + 1 by A1, FINSEQ_1:def 3;
A7: ( dom p = Seg (n + 1) & rng p = Seg (n + 1) ) by FUNCT_2:def 1, FUNCT_2:def 3;
A8: 0 + n <= 1 + n by XREAL_1:8;
reconsider r = p * (s' | n) as FinSequence of Seg (n + 1) by FINSEQ_2:36;
len (s' | n) = n by A6, A8, FINSEQ_1:80;
then len r = n by FINSEQ_2:37;
then A9: dom r = Seg n by FINSEQ_1:def 3;
A10: Seg n c= Seg (n + 1) by A8, FINSEQ_1:7;
q in Seg (n + 1) by A2, A5, FINSEQ_1:6, FUNCT_1:12;
then A11: ( 1 <= q & q <= n + 1 ) by FINSEQ_1:3;
for i being set holds
( i in rng r iff i in Seg n )

proof

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

proof

assume i in rng r ; :: thesis:
then consider j being set such that
A12: j in Seg n and
A13: r . j = i by A9, FUNCT_1:def 5;
reconsider j = j as Element of NAT by A12;
A14: j <= n by A12, FINSEQ_1:3;
then A15: (s' | n) . j = s . j by A1, FINSEQ_3:121;
then A16: i = p . (s . j) by A9, A12, A13, FUNCT_1:22;
A17: j < n + 1 by A14, NAT_1:13;
A18: ( j in dom s & n + 1 in dom s ) by A5, A10, A12, FINSEQ_1:6;
A19: ( s . j in Seg (n + 1) & s . j in dom p ) by A5, A7, A10, A12, FUNCT_1:12;
then reconsider q1 = s . j as Element of NAT ;
A20: p . (s . j) in rng p by A19, FUNCT_1:12;
then reconsider i = i as Element of NAT by A7, A9, A12, A13, A15, FUNCT_1:22;
A21: q1 <> q by A2, A17, A18, FUNCT_1:def 8;

per cases by A21, XXREAL_0:1;

suppose q1 < q ; :: thesis:

then i < q by A3, A16, A19;
then i < n + 1 by A11, XXREAL_0:2;
then ( 1 <= i & i <= n ) by A7, A16, A20, FINSEQ_1:3, NAT_1:13;
hence i in Seg n by FINSEQ_1:3; :: thesis:

end;

suppose q1 > q ; :: thesis:

then A22: i = q1 - 1 by A3, A16, A19;
q1 <= n + 1 by A19, FINSEQ_1:3;
then ( 1 <= i & i <= n ) by A7, A16, A20, A22, FINSEQ_1:3, XREAL_1:22;
hence i in Seg n by FINSEQ_1:3; :: thesis:

end;

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

per cases ;

suppose A24: i < q ; :: thesis:

then A25: p . i = i by A3, A10, A23;
consider j being set such that
A26: j in dom s and
A27: i = s . j by A5, A10, A23, FUNCT_1:def 5;
j in Seg (n + 1) by A26;
then reconsider j = j as Element of NAT ;
j <= n + 1 by A26, FINSEQ_1:3;
then j < n + 1 by A2, A24, A27, XXREAL_0:1;
then A28: ( 1 <= j & j <= n ) by A26, FINSEQ_1:3, NAT_1:13;
then A29: (s' | n) . j = s . j by A1, FINSEQ_3:121;
A30: j in dom r by A9, A28, FINSEQ_1:3;
then r . j = i by A25, A27, A29, FUNCT_1:22;
hence i in rng r by A30, FUNCT_1:12; :: thesis:

end;

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

then A32: i + 1 > q by NAT_1:13;
i <= n by A23, FINSEQ_1:3;
then ( 1 <= i + 1 & i + 1 <= n + 1 ) by NAT_1:12, XREAL_1:8;
then A33: i + 1 in Seg (n + 1) by FINSEQ_1:3;
then consider j being set such that
A34: j in dom s and
A35: i + 1 = s . j by A5, FUNCT_1:def 5;
A36: p . (i + 1) = (i + 1) - 1 by A3, A32, A33
.= i ;
j in Seg (n + 1) by A34;
then reconsider j = j as Element of NAT ;
A37: j <> n + 1 by A2, A31, A35, NAT_1:13;
j <= n + 1 by A34, FINSEQ_1:3;
then j < n + 1 by A37, XXREAL_0:1;
then A38: ( 1 <= j & j <= n ) by A34, FINSEQ_1:3, NAT_1:13;
then A39: j in Seg n by FINSEQ_1:3;
(s' | n) . j = s . j by A1, A38, FINSEQ_3:121;
then r . j = p . (s . j) by A9, A39, FUNCT_1:22;
hence i in rng r by A9, A35, A36, A39, FUNCT_1:12; :: thesis:
thus verum ; :: thesis:

end;

then A40: rng r = Seg n by TARSKI:2;
s' | n = s' | (Seg n) by FINSEQ_1:def 15;
then s' | n is one-to-one by A1, FUNCT_1:84;
then X: r is one-to-one ;
p * (s' | n) is Function of (Seg n),(Seg n) by A9, A40, FUNCT_2:3;
hence p * (s' | n) is Permutation of (Seg n) by A40, X, FUNCT_2:83; :: thesis: