let n, i, j be Element of NAT ; :: thesis:
assume that
A1: i <= n and
A2: j <= n ; :: thesis:

case A3: i < j ; :: thesis:

then i - j < j - j by XREAL_1:9;
then A4: i -' j = 0 by XREAL_0:def 2;
j - i > 0 by A3, XREAL_1:50;
then A5: (j - i) + 1 > 0 + 1 by XREAL_1:6;
then (j + 1) - i >= 0 ;
then A6: (j + 1) -' i = (j - i) + 1 by XREAL_0:def 2;
then A7: (i + ((j + 1) -' i)) -' 1 = (i + ((j + 1) -' i)) - 1 by XREAL_0:def 2;
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
A8: len p = (j + 1) -' i and
A9: for k being Nat st k in dom p holds
p . k = (i + k) -' 1 ;
j - i >= i - i by A3, XREAL_1:9;
then A10: len p = ((i -' j) + (j -' i)) + 1 by A8, A6, A4, XREAL_0:def 2;
A11: (j + 1) -' i = (j + 1) - i by A5, XREAL_0:def 2;
then 1 in dom p by A5, A8, FINSEQ_3:25;
then p . 1 = (i + 1) -' 1 by A9;
then A12: p . 1 = i by NAT_D:34;
rng p c= NAT

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng p ; :: thesis:
then consider y being object such that
A13: y in dom p and
A14: p . y = x by FUNCT_1:def 3;
y in Seg (len p) by A13, FINSEQ_1:def 3;
then y in { k where k is Nat : ( 1 <= k & k <= len p ) } by FINSEQ_1:def 1;
then consider k being Nat such that
A15: k = y and
1 <= k and
k <= len p ;
p . k = (i + k) -' 1 by A9, A13, A15;
hence x in NAT by A14, A15; :: thesis:

end;

then reconsider fs2 = p as FinSequence of NAT by FINSEQ_1:def 4;
A16: 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 that
A17: 1 <= i1 and
A18: i1 < len fs2 ; :: thesis:
A19: 1 <= 1 + i1 by NAT_1:11;
i1 + 1 <= len fs2 by A18, NAT_1:13;
then i1 + 1 in dom p by A19, FINSEQ_3:25;
then A20: fs2 . (i1 + 1) = (i + (i1 + 1)) -' 1 by A9;
1 + (i + i1) >= 1 by NAT_1:11;
then (1 + (i + i1)) - 1 >= 1 - 1 by XREAL_1:9;
then A21: (1 + (i + i1)) -' 1 = i + i1 by XREAL_0:def 2;
i + i1 >= 1 + 0 by A17, XREAL_1:7;
then (i + i1) - 1 >= 1 - 1 by XREAL_1:9;
then A22: 1 + ((i + i1) -' 1) = 1 + ((i + i1) - 1) by XREAL_0:def 2
.= i + i1 ;
( i1 in dom fs2 & fs2 /. i1 = fs2 . i1 ) by A17, A18, FINSEQ_3:25, FINSEQ_4:15;
hence ( fs2 . (i1 + 1) = (fs2 /. i1) + 1 or fs2 . i1 = (fs2 /. (i1 + 1)) + 1 ) by A9, A20, A22, A21; :: thesis:

end;

A23: 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 that
A24: 1 <= k and
A25: k <= len p and
A26: k1 = p . k ; :: thesis:
k in dom p by A24, A25, FINSEQ_3:25;
then A27: k1 = (k + i) -' 1 by A9, A26;
(k + i) - 1 = k + (i - 1) ;
then 1 + (i - 1) <= (k + i) - 1 by A24, XREAL_1:6;
then A28: k1 = (k + i) - 1 by A27, XREAL_0:def 2;
k + i <= ((j + 1) -' i) + i by A8, A25, XREAL_1:6;
then k + i <= ((j + 1) - i) + i by A5, XREAL_0:def 2;
then k1 <= (j + 1) - 1 by A28, XREAL_1:9;
hence k1 <= n by A2, XXREAL_0:2; :: thesis:

end;

len p in dom p by A5, A8, A11, FINSEQ_3:25;
then p . (len p) = j by A8, A9, A11, A7;
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 A23, A12, A10, A16; :: thesis:

end;

case A29: i = j ; :: thesis:

then i - j = 0 ;
then A30: i -' j = 0 by XREAL_0:def 2;
consider f being Function such that
A31: dom f = Seg 1 and
A32: rng f = {i} by FUNCT_1:5;
( rng f c= NAT & f is FinSequence-like ) by A31, A32, FINSEQ_1:def 2, ZFMISC_1:31;
then reconsider fs1 = f as FinSequence of NAT by FINSEQ_1:def 4;
A33: 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 A31, FINSEQ_1:def 3;
1 in dom f by A31, FINSEQ_1:1;
then fs1 . 1 in rng f by FUNCT_1:def 3;
then A34: fs1 . 1 = i by A32, TARSKI:def 1;
A35: len fs1 = 1 by A31, FINSEQ_1:def 3;
then for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds
k1 <= n by A1, A34, XXREAL_0:1;
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 A29, A34, A35, A30, A33; :: thesis:

end;

case A36: j < i ; :: thesis:

then A37: i - j >= j - j by XREAL_1:9;

A38: now :: thesis:

per cases by A37;

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;

j - i < i - i by A36, XREAL_1:9;
then j -' i = 0 by XREAL_0:def 2;
then A39: ((i -' j) + (j -' i)) + 1 = ((i - j) + 1) + (j -' i) by A37, XREAL_0:def 2
.= (i + 1) - j by A38 ;
deffunc H₁( Nat) -> Element of NAT = (i + 1) -' $1;
A40: (i + 1) - 1 >= 0 ;
i - j > 0 by A36, XREAL_1:50;
then A41: (i - j) + 1 > 0 + 1 by XREAL_1:6;
then A42: (i + 1) - ((i + 1) -' j) = (i + 1) - ((i + 1) - j) by XREAL_0:def 2
.= j ;
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
A43: len p = (i + 1) -' j and
A44: for k being Nat st k in dom p holds
p . k = (i + 1) -' k ;
A45: (i + 1) -' j = (i + 1) - j by A41, XREAL_0:def 2;
then 1 in dom p by A41, A43, FINSEQ_3:25;
then p . 1 = (i + 1) -' 1 by A44;
then A46: p . 1 = i by A40, XREAL_0:def 2;
rng p c= NAT

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng p ; :: thesis:
then consider y being object such that
A47: y in dom p and
A48: p . y = x by FUNCT_1:def 3;
y in Seg (len p) by A47, FINSEQ_1:def 3;
then y in { k where k is Nat : ( 1 <= k & k <= len p ) } by FINSEQ_1:def 1;
then consider k being Nat such that
A49: k = y and
A50: ( 1 <= k & k <= len p ) ;
k in dom p by A50, FINSEQ_3:25;
then p . k = (i + 1) -' k by A44;
hence x in NAT by A48, A49; :: thesis:

end;

then reconsider fs2 = p as FinSequence of NAT by FINSEQ_1:def 4;
(i - j) + 1 >= 0 + 1 by A37, XREAL_1:6;
then A51: (i + 1) - j >= 0 ;
A52: 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 that
A53: 1 <= i1 and
A54: i1 < len fs2 ; :: thesis:
A55: i1 + 1 <= len fs2 by A54, NAT_1:13;
then i1 + 1 <= (i - j) + 1 by A43, A51, XREAL_0:def 2;
then i1 <= i - j by XREAL_1:6;
then i1 + j <= i by XREAL_1:19;
then j <= i - i1 by XREAL_1:19;
then A56: 1 + ((i + 1) -' (i1 + 1)) = 1 + ((i + 1) - (i1 + 1)) by XREAL_0:def 2
.= (i + 1) - i1 ;
A57: 1 <= i1 + 1 by A53, NAT_1:13;
then i1 + 1 in dom fs2 by A55, FINSEQ_3:25;
then fs2 . (i1 + 1) = (i + 1) -' (i1 + 1) by A44;
then A58: (fs2 /. (i1 + 1)) + 1 = 1 + ((i + 1) -' (i1 + 1)) by A57, A55, FINSEQ_4:15;
i1 in dom fs2 by A53, A54, FINSEQ_3:25;
then fs2 . i1 = (i + 1) -' i1 by A44;
hence ( fs2 . (i1 + 1) = (fs2 /. i1) + 1 or fs2 . i1 = (fs2 /. (i1 + 1)) + 1 ) by A58, A56, XREAL_0:def 2; :: thesis:

end;

A59: 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 that
A60: 1 <= k and
A61: k <= len p and
A62: k1 = p . k ; :: thesis:
k <= (i + 1) - j by A43, A60, A61, XREAL_0:def 2;
then k + j <= ((i + 1) - j) + j by XREAL_1:6;
then A63: (k + j) - k <= (i + 1) - k by XREAL_1:9;
- k <= - 1 by A60, XREAL_1:24;
then A64: (- k) + (i + 1) <= (- 1) + (i + 1) by XREAL_1:6;
k in dom p by A60, A61, FINSEQ_3:25;
then k1 = (i + 1) -' k by A44, A62;
then k1 = (i + 1) - k by A63, XREAL_0:def 2;
hence k1 <= n by A1, A64, XXREAL_0:2; :: thesis:

end;

len p in dom p by A41, A43, A45, FINSEQ_3:25;
then p . (len p) = (i + 1) -' ((i + 1) -' j) by A43, A44
.= j by A42, XREAL_0:def 2 ;
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 A43, A59, A45, A46, A39, A52; :: 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 ) ) ; :: thesis: