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 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;

for i being object holds

( i in rng r iff i in Seg n )

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: verum

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 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;

for i being object holds

( i in rng r iff i in Seg n )

proof

then A42:
rng r = Seg n
by TARSKI:2;
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 )

then reconsider i = i as Element of NAT ;

end;thus ( i in rng r implies i in Seg n ) :: thesis: ( i in Seg n implies i in rng r )

proof

assume A26:
i in Seg n
; :: thesis: i in rng r
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 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 A18: 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;

end;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 A18: 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
( q1 < q or q1 > q )
by A21, XXREAL_0:1;

end;

suppose
q1 < q
; :: thesis: i in Seg n

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 A17, A18, FINSEQ_1:1;

hence i in Seg n by A22, FINSEQ_1:1; :: thesis: verum

end;then i < n + 1 by A12, XXREAL_0:2;

then A22: i <= n by NAT_1:13;

1 <= i by A17, A18, FINSEQ_1:1;

hence i in Seg n by A22, FINSEQ_1:1; :: thesis: verum

suppose A23:
q1 > q
; :: thesis: i in Seg n

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 A17, A18, FINSEQ_1:1;

hence i in Seg n by A25, FINSEQ_1:1; :: thesis: verum

end;i = q1 - 1 by A3, A17, A20, A23;

then A25: i <= n by A24, XREAL_1:20;

1 <= i by A17, A18, FINSEQ_1:1;

hence i in Seg n by A25, FINSEQ_1:1; :: thesis: verum

then reconsider i = i as Element of NAT ;

per cases
( i < q or i >= q )
;

end;

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 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: verum

end;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: verum

suppose A33:
i >= q
; :: thesis: i in rng r

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: verum

end;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: verum

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: verum