let n, q be Nat; :: thesis: for s, p being Permutation of (Seg (n + 1))
for s9 being FinSequence of Seg (n + 1) st s9 = s & q = s . (n + 1) & ( 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 ) ) ) holds
p * (s9 | n) is Permutation of (Seg n)

let s, p be Permutation of (Seg (n + 1)); :: thesis: for s9 being FinSequence of Seg (n + 1) st s9 = s & q = s . (n + 1) & ( 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 ) ) ) holds
p * (s9 | n) is Permutation of (Seg n)

let s9 be FinSequence of Seg (n + 1); :: thesis: ( s9 = s & q = s . (n + 1) & ( 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 ) ) ) implies p * (s9 | n) is Permutation of (Seg n) )

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: p * (s9 | n) is Permutation of (Seg n)
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 15;
then A7: s9 | n is one-to-one by ;
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 ;
then len (s9 | n) = n by ;
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 ;
then A12: q <= n + 1 by FINSEQ_1:1;
for i being object holds
( i in rng r iff i in Seg n )
proof
let i be object ; :: thesis: ( i in rng r iff i in Seg n )
thus ( i in rng r implies i in Seg n ) :: thesis: ( i in Seg n implies i in rng r )
proof
assume i in rng r ; :: thesis: i in Seg n
then consider j being object such that
A13: j in Seg n and
A14: r . j = i by ;
reconsider j = j as Element of NAT by A13;
A15: j <= n by ;
then A16: (s9 | n) . j = s . j by ;
then A17: i = p . (s . j) by ;
s . j in dom p by ;
then A18: p . (s . j) in rng p by FUNCT_1:3;
then reconsider i = i as Element of NAT by ;
A19: n + 1 in dom s by ;
A20: s . j in Seg (n + 1) by ;
then reconsider q1 = s . j as Element of NAT ;
j < n + 1 by ;
then A21: q1 <> q by ;
per cases ( q1 < q or q1 > q ) by ;
suppose q1 < q ; :: thesis: i in Seg n
then i < q by A3, A17, A20;
then i < n + 1 by ;
then A22: i <= n by NAT_1:13;
1 <= i by ;
hence i in Seg n by ; :: thesis: verum
end;
suppose A23: q1 > q ; :: thesis: i in Seg n
A24: q1 <= n + 1 by ;
i = q1 - 1 by A3, A17, A20, A23;
then A25: i <= n by ;
1 <= i by ;
hence i in Seg n by ; :: thesis: verum
end;
end;
end;
assume A26: i in Seg n ; :: thesis: i in rng r
then reconsider i = i as Element of NAT ;
per cases ( i < q or i >= q ) ;
suppose A27: i < q ; :: thesis: i in rng r
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 ;
j in Seg (n + 1) by A29;
then reconsider j = j as Element of NAT ;
j <= n + 1 by ;
then j < n + 1 by ;
then A31: j <= n by NAT_1:13;
1 <= j by ;
then A32: j in dom r by ;
(s9 | n) . j = s . j by ;
then r . j = i by ;
hence i in rng r by ; :: thesis: verum
end;
suppose A33: i >= q ; :: thesis: i in rng r
i <= n by ;
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 ;
then consider j being object such that
A36: j in dom s and
A37: i + 1 = s . j by ;
j in Seg (n + 1) by A36;
then reconsider j = j as Element of NAT ;
A38: j <= n + 1 by ;
j <> n + 1 by ;
then j < n + 1 by ;
then A39: j <= n by NAT_1:13;
1 <= j by ;
then A40: j in Seg n by ;
i + 1 > q by ;
then A41: p . (i + 1) = (i + 1) - 1 by
.= i ;
(s9 | n) . j = s . j by ;
then r . j = p . (s . j) by ;
hence i in rng r by ; :: thesis: verum
end;
end;
end;
then A42: rng r = Seg n by TARSKI:2;
then p * (s9 | n) is Function of (Seg n),(Seg n) by ;
hence p * (s9 | n) is Permutation of (Seg n) by ; :: thesis: verum