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 ;
then A4: i in Seg n by A1;
1 <= j by ;
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 ;
A7: for k being Nat st k in Seg n holds
ex d being Element of S st S1[k,d]
proof
let k be Nat; :: thesis: ( k in Seg n implies ex d being Element of S st S1[k,d] )
assume A8: k in Seg n ; :: thesis: ex d being Element of S st S1[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 ) ;
per cases then ( k = 1 or k = 2 or ( k > 2 & k <> 1 & k <> 2 ) ) by A10;
suppose ( k = 1 or k = 2 ) ; :: thesis: ex d being Element of S st S1[k,d]
hence ex d being Element of S st S1[k,d] by A4, A5; :: thesis: verum
end;
suppose A11: ( k > 2 & k <> 1 & k <> 2 ) ; :: thesis: ex d being Element of S st S1[k,d]
then reconsider k2 = k - 2 as Nat by NAT_1:21;
k2 > 2 - 2 by ;
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;
suppose A14: k <= i + 1 ; :: thesis: ex d being Element of S st S1[k,d]
then k < j + 1 by ;
then A15: k <= j by NAT_1:13;
k2 <= n by ;
then k2 in S by A12;
hence ex d being Element of S st S1[k,d] by ; :: thesis: verum
end;
suppose A16: ( k > i + 1 & k <= j ) ; :: thesis: ex d being Element of S st S1[k,d]
set k1 = k2 + 1;
k2 + 1 <= (k2 + 1) + 1 by NAT_1:11;
then A17: k2 + 1 <= n by ;
k2 + 1 >= 1 by NAT_1:11;
then k2 + 1 in S by A17;
hence ex d being Element of S st S1[k,d] by ; :: thesis: verum
end;
suppose ( k > i + 1 & k > j & k in S ) ; :: thesis: ex d being Element of S st S1[k,d]
hence ex d being Element of S st S1[k,d] by A11; :: thesis: verum
end;
end;
end;
end;
end;
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 A19: 1 < j by ;
then 1 <= n by ;
then A20: 1 in S ;
then A21: S1[1,f /. 1] by A18;
1 + 1 <= j by ;
then 2 <= n by ;
then A22: 2 in S ;
then A23: S1[2,f /. 2] by A18;
A24: dom f = S by ;
then A25: f /. 1 = f . 1 by ;
A26: rng f c= S by FINSEQ_1:def 4;
then reconsider F = f as Function of S,S by ;
A27: f /. 2 = f . 2 by ;
S c= rng f
proof
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 ;
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 ; :: thesis: x in rng f
A31: k + 2 > 0 + 2 by ;
A32: k + 1 <= i by ;
then k + 1 < j by ;
then (k + 1) + 1 <= j by NAT_1:13;
then ( 1 <= (k + 1) + 1 & (k + 1) + 1 <= n ) by ;
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 ;
hence x in rng f by ; :: thesis: verum
end;
suppose k = i ; :: thesis: x in rng f
hence x in rng f by ; :: thesis: verum
end;
suppose A34: ( k > i & k < j ) ; :: thesis: x in rng f
then k > 1 by ;
then A35: k >= 1 + 1 by NAT_1:13;
k + 1 <= j by ;
then ( 1 <= k + 1 & k + 1 <= n ) by ;
then A36: k + 1 in S ;
then S1[k + 1,f /. (k + 1)] by A18;
then f . (k + 1) = k by ;
hence x in rng f by ; :: thesis: verum
end;
suppose k = j ; :: thesis: x in rng f
hence x in rng f by ; :: thesis: verum
end;
suppose A37: k > j ; :: thesis: x in rng f
j > 1 by ;
then A38: j >= 1 + 1 by NAT_1:13;
S1[k,f /. k] by ;
then f . k = k by ;
hence x in rng f by ; :: thesis: verum
end;
end;
end;
then rng F = S by ;
then A39: F is onto by FUNCT_2:def 3;
card S = card S ;
then F is one-to-one by ;
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 ; :: 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 ;
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 ; :: thesis: verum