let i, j, n be Nat; :: thesis:
assume that
A1: 1 <= i and
A2: i < j and
A3: j <= n ; :: thesis:
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₁[ 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₁[k,d]

proof

let k be Nat; :: thesis:
assume A8: k in Seg n ; :: thesis:
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 by A10;

suppose ( k = 1 or k = 2 ) ; :: thesis:

hence ex d being Element of S st S₁[k,d] by A4, A5; :: thesis:

end;

suppose A11: ( k > 2 & k <> 1 & k <> 2 ) ; :: thesis:

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;

per cases by A8;

suppose A14: k <= i + 1 ; :: thesis:

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₁[k,d] by A11, A14, A15; :: thesis:

end;

suppose A16: ( k > i + 1 & k <= j ) ; :: thesis:

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₁[k,d] by A11, A16; :: thesis:

end;

suppose ( k > i + 1 & k > j & k in S ) ; :: thesis:

hence ex d being Element of S st S₁[k,d] by A11; :: thesis:

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
S₁[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,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₁[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 ; :: according to TARSKI:def 3 :: thesis:
assume A28: x in S ; :: thesis:
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 by XXREAL_0:1;

suppose A30: k < i ; :: thesis:

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₁[(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:

end;

suppose k = i ; :: thesis:

hence x in rng f by A20, A21, A24, A25, FUNCT_1:def 3; :: thesis:

end;

suppose A34: ( k > i & k < j ) ; :: thesis:

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₁[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:

end;

suppose k = j ; :: thesis:

hence x in rng f by A22, A23, A24, A27, FUNCT_1:def 3; :: thesis:

end;

suppose A37: k > j ; :: thesis:

j > 1 by A1, A2, XXREAL_0:2;
then A38: j >= 1 + 1 by NAT_1:13;
S₁[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:

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 ; :: thesis:
thus ( F . 1 = i & F . 2 = j ) by A20, A21, A22, A23, A24, PARTFUN1:def 6; :: thesis:
let k be Nat; :: thesis:
assume that
A40: k in Seg n and
A41: k > 2 ; :: thesis:
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: