let n, q be Nat; ( q in Seg (n + 1) implies ex p being Permutation of (Seg (n + 1)) st
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 ) ) )
defpred S1[ Nat, set ] means ( ( $1 < q implies $2 = $1 ) & ( $1 = q implies $2 = n + 1 ) & ( $1 > q implies $2 = $1 - 1 ) );
assume A1:
q in Seg (n + 1)
; ex p being Permutation of (Seg (n + 1)) st
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 ) )
A2:
for i being Nat st i in Seg (n + 1) holds
ex p being Element of NAT st S1[i,p]
consider p being FinSequence of NAT such that
A6:
dom p = Seg (n + 1)
and
A7:
for i being Nat st i in Seg (n + 1) holds
S1[i,p /. i]
from RECDEF_1:sch 17(A2);
A8:
for i being Element of NAT st i in Seg (n + 1) holds
( i = q iff p /. i = n + 1 )
proof
let i be
Element of
NAT ;
( i in Seg (n + 1) implies ( i = q iff p /. i = n + 1 ) )
assume A9:
i in Seg (n + 1)
;
( i = q iff p /. i = n + 1 )
hence
(
i = q implies
p /. i = n + 1 )
by A7;
( p /. i = n + 1 implies i = q )
thus
(
p /. i = n + 1 implies
i = q )
verum
end;
A11:
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 ) )
proof
let i be
Element of
NAT ;
( i in Seg (n + 1) implies ( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) ) )
assume A12:
i in Seg (n + 1)
;
( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) )
then
p /. i = p . i
by A6, PARTFUN1:def 6;
hence
( (
i < q implies
p . i = i ) & (
i = q implies
p . i = n + 1 ) & (
i > q implies
p . i = i - 1 ) )
by A7, A12;
verum
end;
for i being object holds
( i in rng p iff i in Seg (n + 1) )
proof
let i be
object ;
( i in rng p iff i in Seg (n + 1) )
thus
(
i in rng p implies
i in Seg (n + 1) )
( i in Seg (n + 1) implies i in rng p )proof
assume
i in rng p
;
i in Seg (n + 1)
then consider j being
object such that A13:
j in Seg (n + 1)
and A14:
p . j = i
by A6, FUNCT_1:def 3;
reconsider j =
j as
Element of
NAT by A13;
per cases
( j < q or j = q or j > q )
by XXREAL_0:1;
suppose A15:
j > q
;
i in Seg (n + 1)then A16:
i = j - 1
by A11, A13, A14;
A17:
1
<= q
by A1, FINSEQ_1:1;
then reconsider i =
i as
Element of
NAT by A15, A16, INT_1:5, XXREAL_0:2;
j <= n + 1
by A13, FINSEQ_1:1;
then
i <= n
by A16, XREAL_1:20;
then A18:
i <= n + 1
by NAT_1:12;
1
< i + 1
by A15, A16, A17, XXREAL_0:2;
then
1
<= i
by NAT_1:13;
hence
i in Seg (n + 1)
by A18, FINSEQ_1:1;
verum end; end;
end;
thus
(
i in Seg (n + 1) implies
i in rng p )
verum
end;
then A24:
rng p = Seg (n + 1)
by TARSKI:2;
then A25:
p is Function of (Seg (n + 1)),(Seg (n + 1))
by A6, FUNCT_2:1;
A26:
for i being Element of NAT st i in Seg (n + 1) & p /. i <> n + 1 holds
( i < q iff p /. i < q )
for i1, i2 being object st i1 in Seg (n + 1) & i2 in Seg (n + 1) & p . i1 = p . i2 holds
i1 = i2
proof
let i1,
i2 be
object ;
( i1 in Seg (n + 1) & i2 in Seg (n + 1) & p . i1 = p . i2 implies i1 = i2 )
assume that A31:
i1 in Seg (n + 1)
and A32:
i2 in Seg (n + 1)
and A33:
p . i1 = p . i2
;
i1 = i2
reconsider i1 =
i1 as
Element of
NAT by A31;
A34:
p /. i1 = p . i1
by A6, A31, PARTFUN1:def 6;
reconsider i2 =
i2 as
Element of
NAT by A32;
A35:
p /. i2 = p . i2
by A6, A32, PARTFUN1:def 6;
per cases
( p /. i1 = n + 1 or ( p /. i1 <> n + 1 & p /. i1 < q ) or ( p /. i1 <> n + 1 & p /. i1 >= q ) )
;
suppose A37:
(
p /. i1 <> n + 1 &
p /. i1 < q )
;
i1 = i2then
i1 < q
by A26, A31;
then A38:
p /. i1 = i1
by A7, A31;
i2 < q
by A26, A32, A33, A34, A35, A37;
hence
i1 = i2
by A7, A32, A33, A34, A35, A38;
verum end; suppose A39:
(
p /. i1 <> n + 1 &
p /. i1 >= q )
;
i1 = i2then A40:
i1 <> q
by A8, A31;
i1 >= q
by A26, A31, A39;
then
i1 > q
by A40, XXREAL_0:1;
then A41:
p /. i1 = i1 - 1
by A7, A31;
A42:
i2 <> q
by A8, A32, A33, A34, A35, A39;
i2 >= q
by A26, A32, A33, A34, A35, A39;
then
i2 > q
by A42, XXREAL_0:1;
then
p /. i2 = i2 - 1
by A7, A32;
hence
i1 = i2
by A6, A32, A33, A34, A41, PARTFUN1:def 6, XCMPLX_1:19;
verum end; end;
end;
then
p is one-to-one
by A6, FUNCT_1:def 4;
then reconsider p = p as Permutation of (Seg (n + 1)) by A24, A25, FUNCT_2:57;
take
p
; 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 ) )
thus
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 ) )
by A11; verum