let n, i, j be Element of NAT ; :: thesis:
assume A1: ( i <= n & j <= n ) ; :: thesis:

per cases by XXREAL_0:1;

then j - i > 0 by XREAL_1:52;
then A3: (j - i) + 1 > 0 + 1 by XREAL_1:8;
deffunc H₁( Nat) -> Element of NAT = (i + $1) -' 1;
ex p being FinSequence st
( len p = (j + 1) -' i & ( for k being Nat st k in dom p holds
p . k = H₁(k) ) ) from FINSEQ_1:sch 2();
then consider p being FinSequence such that
A4: ( len p = (j + 1) -' i & ( for k being Nat st k in dom p holds
p . k = (i + k) -' 1 ) ) ;
A5: for k, k1 being Element of NAT st 1 <= k & k <= len p & k1 = p . k holds
k1 <= n

proof

let k, k1 be Element of NAT ; :: thesis:
assume A6: ( 1 <= k & k <= len p & k1 = p . k ) ; :: thesis:
then k in dom p by FINSEQ_3:27;
then A7: k1 = (k + i) -' 1 by A4, A6;
k + i <= ((j + 1) -' i) + i by A4, A6, XREAL_1:8;
then A8: k + i <= ((j + 1) - i) + i by A3, XREAL_0:def 2;
(k + i) - 1 = k + (i - 1) ;
then 1 + (i - 1) <= (k + i) - 1 by A6, XREAL_1:8;
then k1 = (k + i) - 1 by A7, XREAL_0:def 2;
then k1 <= (j + 1) - 1 by A8, XREAL_1:11;
hence k1 <= n by A1, XXREAL_0:2; :: thesis:

end;

A9: (j + 1) - i >= 0 by A3;
A10: (j + 1) -' i = (j + 1) - i by A3, XREAL_0:def 2;
A11: (j + 1) -' i = (j - i) + 1 by A9, XREAL_0:def 2;
1 in dom p by A3, A10, FINSEQ_3:27, A4;
then p . 1 = (i + 1) -' 1 by A4;
then A12: p . 1 = i by NAT_D:34;
A13: j - i >= i - i by A2, XREAL_1:11;
A14: (i + ((j + 1) -' i)) -' 1 = (i + ((j + 1) -' i)) - 1 by A11, XREAL_0:def 2;
len p in dom p by FINSEQ_3:27, A3, A10, A4;
then A15: p . (len p) = j by A4, A10, A14;
i - j < j - j by A2, XREAL_1:11;
then i -' j = 0 by XREAL_0:def 2;
then A16: len p = ((i -' j) + (j -' i)) + 1 by A4, A11, A13, XREAL_0:def 2;
rng p c= NAT

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng p ; :: thesis:
then consider y being set such that
A17: ( y in dom p & p . y = x ) by FUNCT_1:def 5;
y in Seg (len p) by A17, FINSEQ_1:def 3;
then y in { k where k is Element of NAT : ( 1 <= k & k <= len p ) } by FINSEQ_1:def 1;
then consider k being Element of NAT such that
A18: ( k = y & 1 <= k & k <= len p ) ;
p . k = (i + k) -' 1 by A4, A18, A17;
hence x in NAT by A17, A18; :: thesis:

end;

then reconsider fs2 = p as FinSequence of NAT by FINSEQ_1:def 4;
for i1 being Element of NAT st 1 <= i1 & i1 < len fs2 & not fs2 . (i1 + 1) = (fs2 /. i1) + 1 holds
fs2 . i1 = (fs2 /. (i1 + 1)) + 1

proof

let i1 be Element of NAT ; :: thesis:
assume A19: ( 1 <= i1 & i1 < len fs2 ) ; :: thesis:
then A20: i1 + 1 <= len fs2 by NAT_1:13;
1 <= 1 + i1 by NAT_1:11;
then i1 + 1 in dom p by A20, FINSEQ_3:27;
then A21: fs2 . (i1 + 1) = (i + (i1 + 1)) -' 1 by A4;
A22: i1 in dom fs2 by A19, FINSEQ_3:27;
A23: fs2 /. i1 = fs2 . i1 by A19, FINSEQ_4:24;
i + i1 >= 1 + 0 by A19, XREAL_1:9;
then (i + i1) - 1 >= 1 - 1 by XREAL_1:11;
then A24: 1 + ((i + i1) -' 1) = 1 + ((i + i1) - 1) by XREAL_0:def 2
.= i + i1 ;
1 + (i + i1) >= 1 by NAT_1:11;
then (1 + (i + i1)) - 1 >= 1 - 1 by XREAL_1:11;
then (1 + (i + i1)) -' 1 = i + i1 by XREAL_0:def 2;
hence ( fs2 . (i1 + 1) = (fs2 /. i1) + 1 or fs2 . i1 = (fs2 /. (i1 + 1)) + 1 ) by A4, A21, A22, A23, A24; :: thesis:

end;

hence ex fs1 being FinSequence of NAT st
( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds
k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds
fs1 . i1 = (fs1 /. (i1 + 1)) + 1 ) ) by A5, A12, A15, A16; :: thesis:

end;

case A25: i = j ; :: thesis:

consider f being Function such that
A26: ( dom f = Seg 1 & rng f = {i} ) by FUNCT_1:15;
A27: rng f c= NAT by A26, ZFMISC_1:37;
f is FinSequence-like by A26, FINSEQ_1:def 2;
then reconsider fs1 = f as FinSequence of NAT by A27, FINSEQ_1:def 4;
1 in dom f by A26, FINSEQ_1:3;
then fs1 . 1 in rng f by FUNCT_1:def 5;
then A28: fs1 . 1 = i by A26, TARSKI:def 1;
A29: len fs1 = 1 by A26, FINSEQ_1:def 3;
i - j = 0 by A25;
then A30: i -' j = 0 by XREAL_0:def 2;
A31: for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds
k1 <= n by A1, A28, A29, XXREAL_0:1;
for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds
fs1 . i1 = (fs1 /. (i1 + 1)) + 1 by A26, FINSEQ_1:def 3;
hence ex fs1 being FinSequence of NAT st
( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds
k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds
fs1 . i1 = (fs1 /. (i1 + 1)) + 1 ) ) by A25, A28, A29, A30, A31; :: thesis:

end;

case A32: j < i ; :: thesis:

then i - j > 0 by XREAL_1:52;
then A33: (i - j) + 1 > 0 + 1 by XREAL_1:8;
deffunc H₁( Nat) -> Element of NAT = (i + 1) -' $1;
ex p being FinSequence st
( len p = (i + 1) -' j & ( for k being Nat st k in dom p holds
p . k = H₁(k) ) ) from FINSEQ_1:sch 2();
then consider p being FinSequence such that
A34: ( len p = (i + 1) -' j & ( for k being Nat st k in dom p holds
p . k = (i + 1) -' k ) ) ;
A35: for k, k1 being Element of NAT st 1 <= k & k <= len p & k1 = p . k holds
k1 <= n

proof

let k, k1 be Element of NAT ; :: thesis:
assume A36: ( 1 <= k & k <= len p & k1 = p . k ) ; :: thesis:
then k in dom p by FINSEQ_3:27;
then A37: k1 = (i + 1) -' k by A34, A36;
- k <= - 1 by A36, XREAL_1:26;
then A38: (- k) + (i + 1) <= (- 1) + (i + 1) by XREAL_1:8;
k <= (i + 1) - j by A34, A36, XREAL_0:def 2;
then k + j <= ((i + 1) - j) + j by XREAL_1:8;
then (k + j) - k <= (i + 1) - k by XREAL_1:11;
then k1 = (i + 1) - k by A37, XREAL_0:def 2;
hence k1 <= n by A1, A38, XXREAL_0:2; :: thesis:

end;

A39: (i + 1) -' j = (i + 1) - j by A33, XREAL_0:def 2;
then 1 in dom p by A33, FINSEQ_3:27, A34;
then A40: p . 1 = (i + 1) -' 1 by A34;
(i + 1) - 1 >= 0 ;
then A41: p . 1 = i by A40, XREAL_0:def 2;
A42: i - j >= j - j by A32, XREAL_1:11;
then (i - j) + 1 >= 0 + 1 by XREAL_1:8;
then A43: (i + 1) - j >= 0 ;
A44: (i + 1) - ((i + 1) -' j) = (i + 1) - ((i + 1) - j) by A33, XREAL_0:def 2
.= j ;

A45: now

per cases by A42;

case i - j = 0 ; :: thesis:

hence j -' i = 0 by XREAL_0:def 2; :: thesis:

end;

case i - j > 0 ; :: thesis:

then - (- (i - j)) > 0 ;
then j - i < 0 ;
hence j -' i = 0 by XREAL_0:def 2; :: thesis:

end;

len p in dom p by FINSEQ_3:27, A33, A34, A39;
then A46: p . (len p) = (i + 1) -' ((i + 1) -' j) by A34
.= j by A44, XREAL_0:def 2 ;
j - i < i - i by A32, XREAL_1:11;
then j -' i = 0 by XREAL_0:def 2;
then A47: ((i -' j) + (j -' i)) + 1 = ((i - j) + 1) + (j -' i) by A42, XREAL_0:def 2
.= (i + 1) - j by A45 ;
rng p c= NAT

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng p ; :: thesis:
then consider y being set such that
A48: ( y in dom p & p . y = x ) by FUNCT_1:def 5;
y in Seg (len p) by A48, FINSEQ_1:def 3;
then y in { k where k is Element of NAT : ( 1 <= k & k <= len p ) } by FINSEQ_1:def 1;
then consider k being Element of NAT such that
A49: ( k = y & 1 <= k & k <= len p ) ;
k in dom p by A49, FINSEQ_3:27;
then p . k = (i + 1) -' k by A34;
hence x in NAT by A48, A49; :: thesis:

end;

proof

let i1 be Element of NAT ; :: thesis:
assume A50: ( 1 <= i1 & i1 < len fs2 ) ; :: thesis:
then i1 in dom fs2 by FINSEQ_3:27;
then A51: fs2 . i1 = (i + 1) -' i1 by A34;
A52: ( 1 <= i1 + 1 & i1 + 1 <= len fs2 ) by A50, NAT_1:13;
then i1 + 1 in dom fs2 by FINSEQ_3:27;
then fs2 . (i1 + 1) = (i + 1) -' (i1 + 1) by A34;
then A53: (fs2 /. (i1 + 1)) + 1 = 1 + ((i + 1) -' (i1 + 1)) by A52, FINSEQ_4:24;
i1 + 1 <= (i - j) + 1 by A34, A43, A52, XREAL_0:def 2;
then i1 <= i - j by XREAL_1:8;
then i1 + j <= i by XREAL_1:21;
then j <= i - i1 by XREAL_1:21;
then 1 + ((i + 1) -' (i1 + 1)) = 1 + ((i + 1) - (i1 + 1)) by XREAL_0:def 2
.= (i + 1) - i1 ;
hence ( fs2 . (i1 + 1) = (fs2 /. i1) + 1 or fs2 . i1 = (fs2 /. (i1 + 1)) + 1 ) by A51, A53, XREAL_0:def 2; :: thesis:

end;