let n, i, j be Element of NAT ; :: thesis: ( i <= n & j <= n implies 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 ) ) )

assume that
A1: i <= n and
A2: j <= n ; :: thesis: 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 ) )

now :: thesis: ( ( i < j & 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 ) ) ) or ( i = j & 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 ) ) ) or ( j < i & 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 ) ) ) )
per cases ( i < j or i = j or j < i ) by XXREAL_0:1;
case A3: i < j ; :: thesis: 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 ) )

then i - j < j - j by XREAL_1:9;
then A4: i -' j = 0 by XREAL_0:def 2;
j - i > 0 by ;
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 H1( 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 = H1(k) ) ) from 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 ;
then A10: len p = ((i -' j) + (j -' i)) + 1 by ;
A11: (j + 1) -' i = (j + 1) - i by ;
then 1 in dom p by ;
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: ( not x in rng p or x in NAT )
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 ;
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 ; :: thesis: verum
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: ( 1 <= i1 & i1 < len fs2 & not fs2 . (i1 + 1) = (fs2 /. i1) + 1 implies fs2 . i1 = (fs2 /. (i1 + 1)) + 1 )
assume that
A17: 1 <= i1 and
A18: i1 < len fs2 ; :: thesis: ( fs2 . (i1 + 1) = (fs2 /. i1) + 1 or fs2 . i1 = (fs2 /. (i1 + 1)) + 1 )
A19: 1 <= 1 + i1 by NAT_1:11;
i1 + 1 <= len fs2 by ;
then i1 + 1 in dom p by ;
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 ;
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 ;
hence ( fs2 . (i1 + 1) = (fs2 /. i1) + 1 or fs2 . i1 = (fs2 /. (i1 + 1)) + 1 ) by A9, A20, A22, A21; :: thesis: verum
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: ( 1 <= k & k <= len p & k1 = p . k implies k1 <= n )
assume that
A24: 1 <= k and
A25: k <= len p and
A26: k1 = p . k ; :: thesis: k1 <= n
k in dom p by ;
then A27: k1 = (k + i) -' 1 by ;
(k + i) - 1 = k + (i - 1) ;
then 1 + (i - 1) <= (k + i) - 1 by ;
then A28: k1 = (k + i) - 1 by ;
k + i <= ((j + 1) -' i) + i by ;
then k + i <= ((j + 1) - i) + i by ;
then k1 <= (j + 1) - 1 by ;
hence k1 <= n by ; :: thesis: verum
end;
len p in dom p by ;
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: verum
end;
case A29: i = j ; :: thesis: 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 ) )

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 ;
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 ;
1 in dom f by ;
then fs1 . 1 in rng f by FUNCT_1:def 3;
then A34: fs1 . 1 = i by ;
A35: len fs1 = 1 by ;
then for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds
k1 <= n by ;
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: verum
end;
case A36: j < i ; :: thesis: 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 ) )

then A37: i - j >= j - j by XREAL_1:9;
A38: now :: thesis: ( ( i - j = 0 & j -' i = 0 ) or ( i - j > 0 & j -' i = 0 ) )
per cases ( i - j = 0 or i - j > 0 ) by A37;
case i - j > 0 ; :: thesis: j -' i = 0
then - (- (i - j)) > 0 ;
then j - i < 0 ;
hence j -' i = 0 by XREAL_0:def 2; :: thesis: verum
end;
end;
end;
j - i < i - i by ;
then j -' i = 0 by XREAL_0:def 2;
then A39: ((i -' j) + (j -' i)) + 1 = ((i - j) + 1) + (j -' i) by
.= (i + 1) - j by A38 ;
deffunc H1( Nat) -> Element of NAT = (i + 1) -' \$1;
A40: (i + 1) - 1 >= 0 ;
i - j > 0 by ;
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 = H1(k) ) ) from 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 ;
then 1 in dom p by ;
then p . 1 = (i + 1) -' 1 by A44;
then A46: p . 1 = i by ;
rng p c= NAT
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng p or x in NAT )
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 ;
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 ;
then p . k = (i + 1) -' k by A44;
hence x in NAT by ; :: thesis: verum
end;
then reconsider fs2 = p as FinSequence of NAT by FINSEQ_1:def 4;
(i - j) + 1 >= 0 + 1 by ;
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: ( 1 <= i1 & i1 < len fs2 & not fs2 . (i1 + 1) = (fs2 /. i1) + 1 implies fs2 . i1 = (fs2 /. (i1 + 1)) + 1 )
assume that
A53: 1 <= i1 and
A54: i1 < len fs2 ; :: thesis: ( fs2 . (i1 + 1) = (fs2 /. i1) + 1 or fs2 . i1 = (fs2 /. (i1 + 1)) + 1 )
A55: i1 + 1 <= len fs2 by ;
then i1 + 1 <= (i - j) + 1 by ;
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 ;
then i1 + 1 in dom fs2 by ;
then fs2 . (i1 + 1) = (i + 1) -' (i1 + 1) by A44;
then A58: (fs2 /. (i1 + 1)) + 1 = 1 + ((i + 1) -' (i1 + 1)) by ;
i1 in dom fs2 by ;
then fs2 . i1 = (i + 1) -' i1 by A44;
hence ( fs2 . (i1 + 1) = (fs2 /. i1) + 1 or fs2 . i1 = (fs2 /. (i1 + 1)) + 1 ) by ; :: thesis: verum
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: ( 1 <= k & k <= len p & k1 = p . k implies k1 <= n )
assume that
A60: 1 <= k and
A61: k <= len p and
A62: k1 = p . k ; :: thesis: k1 <= n
k <= (i + 1) - j by ;
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 ;
then A64: (- k) + (i + 1) <= (- 1) + (i + 1) by XREAL_1:6;
k in dom p by ;
then k1 = (i + 1) -' k by ;
then k1 = (i + 1) - k by ;
hence k1 <= n by ; :: thesis: verum
end;
len p in dom p by ;
then p . (len p) = (i + 1) -' ((i + 1) -' j) by
.= j by ;
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: verum
end;
end;
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: verum