let i, j, n be Nat; ( 1 <= i & i < j & j <= n implies ex P being Permutation of (Seg n) st
( P . 1 = i & P . 2 = j & ( for k being Nat st k in Seg n & k > 2 holds
( ( k <= i + 1 implies P . k = k - 2 ) & ( i + 1 < k & k <= j implies P . k = k - 1 ) & ( k > j implies P . k = k ) ) ) ) )
assume that
A1:
1 <= i
and
A2:
i < j
and
A3:
j <= n
; ex P being Permutation of (Seg n) st
( P . 1 = i & P . 2 = j & ( for k being Nat st k in Seg n & k > 2 holds
( ( k <= i + 1 implies P . k = k - 2 ) & ( i + 1 < k & k <= j implies P . k = k - 1 ) & ( k > j implies P . k = k ) ) ) )
i <= n
by A2, A3, XXREAL_0:2;
then A4:
i in Seg n
by A1;
1 <= j
by A1, A2, XXREAL_0:2;
then A5:
j in Seg n
by A3;
reconsider S = Seg n as non empty Subset of NAT by A1, A2, A3;
defpred S1[ Nat, Nat] means ( ( $1 = 1 implies $2 = i ) & ( $1 = 2 implies $2 = j ) & ( $1 > 2 implies ( ( $1 <= i + 1 implies $2 = $1 - 2 ) & ( i + 1 < $1 & $1 <= j implies $2 = $1 - 1 ) & ( $1 > j implies $2 = $1 ) ) ) );
A6:
i + 1 < j + 1
by A2, XREAL_1:8;
A7:
for k being Nat st k in Seg n holds
ex d being Element of S st S1[k,d]
consider f being FinSequence of S such that
A18:
( len f = n & ( for k being Nat st k in Seg n holds
S1[k,f /. k] ) )
from FINSEQ_4:sch 1(A7);
A19:
1 < j
by A1, A2, XXREAL_0:2;
then
1 <= n
by A3, XXREAL_0:2;
then A20:
1 in S
;
then A21:
S1[1,f /. 1]
by A18;
1 + 1 <= j
by A19, NAT_1:13;
then
2 <= n
by A3, XXREAL_0:2;
then A22:
2 in S
;
then A23:
S1[2,f /. 2]
by A18;
A24:
dom f = S
by A18, FINSEQ_1:def 3;
then A25:
f /. 1 = f . 1
by A20, PARTFUN1:def 6;
A26:
rng f c= S
by FINSEQ_1:def 4;
then reconsider F = f as Function of S,S by A24, FUNCT_2:2;
A27:
f /. 2 = f . 2
by A22, A24, PARTFUN1:def 6;
S c= rng f
proof
let x be
object ;
TARSKI:def 3 ( not x in S or x in rng f )
assume A28:
x in S
;
x in rng f
then reconsider k =
x as
Nat ;
set k1 =
k + 1;
set k2 =
(k + 1) + 1;
A29:
1
<= k
by A28, FINSEQ_1:1;
per cases
( k < i or k = i or ( k > i & k < j ) or k = j or k > j )
by XXREAL_0:1;
suppose A30:
k < i
;
x in rng fA31:
k + 2
> 0 + 2
by A29, XREAL_1:8;
A32:
k + 1
<= i
by A30, NAT_1:13;
then
k + 1
< j
by A2, XXREAL_0:2;
then
(k + 1) + 1
<= j
by NAT_1:13;
then
( 1
<= (k + 1) + 1 &
(k + 1) + 1
<= n )
by A3, NAT_1:11, XXREAL_0:2;
then A33:
(k + 1) + 1
in S
;
then
S1[
(k + 1) + 1,
f /. ((k + 1) + 1)]
by A18;
then
f . ((k + 1) + 1) = k
by A24, A31, A32, A33, PARTFUN1:def 6, XREAL_1:6;
hence
x in rng f
by A24, A33, FUNCT_1:def 3;
verum end; suppose A34:
(
k > i &
k < j )
;
x in rng fthen
k > 1
by A1, A29, XXREAL_0:1;
then A35:
k >= 1
+ 1
by NAT_1:13;
k + 1
<= j
by A34, NAT_1:13;
then
( 1
<= k + 1 &
k + 1
<= n )
by A3, NAT_1:11, XXREAL_0:2;
then A36:
k + 1
in S
;
then
S1[
k + 1,
f /. (k + 1)]
by A18;
then
f . (k + 1) = k
by A24, A34, A35, A36, NAT_1:13, PARTFUN1:def 6, XREAL_1:8;
hence
x in rng f
by A24, A36, FUNCT_1:def 3;
verum end; suppose A37:
k > j
;
x in rng f
j > 1
by A1, A2, XXREAL_0:2;
then A38:
j >= 1
+ 1
by NAT_1:13;
S1[
k,
f /. k]
by A18, A28;
then
f . k = k
by A24, A37, A38, PARTFUN1:def 6, XXREAL_0:2;
hence
x in rng f
by A24, A28, FUNCT_1:def 3;
verum end; end;
end;
then
rng F = S
by A26, XBOOLE_0:def 10;
then A39:
F is onto
by FUNCT_2:def 3;
card S = card S
;
then
F is one-to-one
by A39, FINSEQ_4:63;
then reconsider F = F as Permutation of (Seg n) by A39;
take
F
; ( F . 1 = i & F . 2 = j & ( for k being Nat st k in Seg n & k > 2 holds
( ( k <= i + 1 implies F . k = k - 2 ) & ( i + 1 < k & k <= j implies F . k = k - 1 ) & ( k > j implies F . k = k ) ) ) )
thus
( F . 1 = i & F . 2 = j )
by A20, A21, A22, A23, A24, PARTFUN1:def 6; for k being Nat st k in Seg n & k > 2 holds
( ( k <= i + 1 implies F . k = k - 2 ) & ( i + 1 < k & k <= j implies F . k = k - 1 ) & ( k > j implies F . k = k ) )
let k be Nat; ( k in Seg n & k > 2 implies ( ( k <= i + 1 implies F . k = k - 2 ) & ( i + 1 < k & k <= j implies F . k = k - 1 ) & ( k > j implies F . k = k ) ) )
assume that
A40:
k in Seg n
and
A41:
k > 2
; ( ( k <= i + 1 implies F . k = k - 2 ) & ( i + 1 < k & k <= j implies F . k = k - 1 ) & ( k > j implies F . k = k ) )
f /. k = f . k
by A24, A40, PARTFUN1:def 6;
hence
( ( k <= i + 1 implies F . k = k - 2 ) & ( i + 1 < k & k <= j implies F . k = k - 1 ) & ( k > j implies F . k = k ) )
by A18, A40, A41; verum