let n, i, j be Element of NAT ; ( 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
; 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 ( ( 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
;
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 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 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 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
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
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 ;
( 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
;
k1 <= n
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;
verum
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;
verum end; case A29:
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 ) )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;
verum end; case A36:
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 ) )then A37:
i - j >= j - j
by XREAL_1:9;
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 H1(
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 = H1(
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
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 ;
( 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
;
( fs2 . (i1 + 1) = (fs2 /. i1) + 1 or fs2 . i1 = (fs2 /. (i1 + 1)) + 1 )
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;
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 ;
( 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
;
k1 <= n
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;
verum
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;
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 ) )
; verum