let n, q be Nat; 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)); 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); ( 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 ) )
; 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
let i be
object ;
( i in rng r iff i in Seg n )
thus
(
i in rng r implies
i in Seg n )
( i in Seg n implies i in rng r )proof
assume
i in rng r
;
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;
assume A26:
i in Seg n
;
i in rng r
then reconsider i =
i as
Element of
NAT ;
per cases
( i < q or i >= q )
;
suppose A27:
i < q
;
i in rng rthen 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;
verum end; suppose A33:
i >= q
;
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;
verum 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; verum