let i, j, n be Nat; :: thesis: ( 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 ; :: thesis: 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 S_{1}[ 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 S_{1}[k,d]

A18: ( len f = n & ( for k being Nat st k in Seg n holds

S_{1}[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: S_{1}[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: S_{1}[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

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 ; :: thesis: ( 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( ( 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; :: thesis: verum

( 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 ; :: thesis: 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 S

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 S

proof

consider f being FinSequence of S such that
let k be Nat; :: thesis: ( k in Seg n implies ex d being Element of S st S_{1}[k,d] )

assume A8: k in Seg n ; :: thesis: ex d being Element of S st S_{1}[k,d]

then A9: k <= n by FINSEQ_1:1;

A10: k <> 0 by A8;

( k <= 2 implies not not k = 0 & ... & not k = 2 ) ;

end;assume A8: k in Seg n ; :: thesis: ex d being Element of S st S

then A9: k <= n by FINSEQ_1:1;

A10: k <> 0 by A8;

( k <= 2 implies not not k = 0 & ... & not k = 2 ) ;

per cases then
( k = 1 or k = 2 or ( k > 2 & k <> 1 & k <> 2 ) )
by A10;

end;

suppose A11:
( k > 2 & k <> 1 & k <> 2 )
; :: thesis: ex d being Element of S st S_{1}[k,d]

then reconsider k2 = k - 2 as Nat by NAT_1:21;

k2 > 2 - 2 by A11, XREAL_1:8;

then A12: k2 >= 1 by NAT_1:14;

A13: k2 <= k - 0 by XREAL_1:10;

end;k2 > 2 - 2 by A11, XREAL_1:8;

then A12: k2 >= 1 by NAT_1:14;

A13: k2 <= k - 0 by XREAL_1:10;

per cases
( k <= i + 1 or ( k > i + 1 & k <= j ) or ( k > i + 1 & k > j & k in S ) )
by A8;

end;

suppose A14:
k <= i + 1
; :: thesis: ex d being Element of S st S_{1}[k,d]

then
k < j + 1
by A6, XXREAL_0:2;

then A15: k <= j by NAT_1:13;

k2 <= n by A9, A13, XXREAL_0:2;

then k2 in S by A12;

hence ex d being Element of S st S_{1}[k,d]
by A11, A14, A15; :: thesis: verum

end;then A15: k <= j by NAT_1:13;

k2 <= n by A9, A13, XXREAL_0:2;

then k2 in S by A12;

hence ex d being Element of S st S

suppose A16:
( k > i + 1 & k <= j )
; :: thesis: ex d being Element of S st S_{1}[k,d]

set k1 = k2 + 1;

k2 + 1 <= (k2 + 1) + 1 by NAT_1:11;

then A17: k2 + 1 <= n by A9, XXREAL_0:2;

k2 + 1 >= 1 by NAT_1:11;

then k2 + 1 in S by A17;

hence ex d being Element of S st S_{1}[k,d]
by A11, A16; :: thesis: verum

end;k2 + 1 <= (k2 + 1) + 1 by NAT_1:11;

then A17: k2 + 1 <= n by A9, XXREAL_0:2;

k2 + 1 >= 1 by NAT_1:11;

then k2 + 1 in S by A17;

hence ex d being Element of S st S

A18: ( len f = n & ( for k being Nat st k in Seg n holds

S

A19: 1 < j by A1, A2, XXREAL_0:2;

then 1 <= n by A3, XXREAL_0:2;

then A20: 1 in S ;

then A21: S

1 + 1 <= j by A19, NAT_1:13;

then 2 <= n by A3, XXREAL_0:2;

then A22: 2 in S ;

then A23: S

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

then
rng F = S
by A26, XBOOLE_0:def 10;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in S or x in rng f )

assume A28: x in S ; :: thesis: 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;

end;assume A28: x in S ; :: thesis: 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;

end;

suppose A30:
k < i
; :: thesis: x in rng f

A31:
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 S_{1}[(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; :: thesis: verum

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

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

suppose A34:
( k > i & k < j )
; :: thesis: x in rng f

then
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 S_{1}[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; :: thesis: verum

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

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

suppose A37:
k > j
; :: thesis: x in rng f

j > 1
by A1, A2, XXREAL_0:2;

then A38: j >= 1 + 1 by NAT_1:13;

S_{1}[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; :: thesis: verum

end;then A38: j >= 1 + 1 by NAT_1:13;

S

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

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 ; :: thesis: ( 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( ( 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; :: thesis: verum