let a, b be Real; for jauge being positive-yielding Function of [.a,b.],REAL st a <= b holds
ex x being non empty increasing FinSequence of REAL ex t being non empty FinSequence of REAL st
( x . 1 = a & x . (len x) = b & t . 1 = a & dom x = dom t & ( for i being Nat st i - 1 in dom t & i in dom t holds
( (t . i) - (jauge . (t . i)) <= x . (i - 1) & x . (i - 1) <= t . i ) ) & ( for i being Nat st i in dom t holds
( t . i <= x . i & x . i <= (t . i) + (jauge . (t . i)) ) ) )
let jauge be positive-yielding Function of [.a,b.],REAL; ( a <= b implies ex x being non empty increasing FinSequence of REAL ex t being non empty FinSequence of REAL st
( x . 1 = a & x . (len x) = b & t . 1 = a & dom x = dom t & ( for i being Nat st i - 1 in dom t & i in dom t holds
( (t . i) - (jauge . (t . i)) <= x . (i - 1) & x . (i - 1) <= t . i ) ) & ( for i being Nat st i in dom t holds
( t . i <= x . i & x . i <= (t . i) + (jauge . (t . i)) ) ) ) )
assume A1:
a <= b
; ex x being non empty increasing FinSequence of REAL ex t being non empty FinSequence of REAL st
( x . 1 = a & x . (len x) = b & t . 1 = a & dom x = dom t & ( for i being Nat st i - 1 in dom t & i in dom t holds
( (t . i) - (jauge . (t . i)) <= x . (i - 1) & x . (i - 1) <= t . i ) ) & ( for i being Nat st i in dom t holds
( t . i <= x . i & x . i <= (t . i) + (jauge . (t . i)) ) ) )
defpred S1[ object ] means ex x being non empty increasing FinSequence of REAL ex t being non empty FinSequence of REAL st
( x . 1 = a & x . (len x) = $1 & t . 1 = a & dom x = dom t & ( for i being Nat st i - 1 in dom t & i in dom t holds
( (t . i) - (jauge . (t . i)) <= x . (i - 1) & x . (i - 1) <= t . i ) ) & ( for i being Nat st i in dom t holds
( t . i <= x . i & x . i <= (t . i) + (jauge . (t . i)) ) ) );
consider C being set such that
A2:
for x being object holds
( x in C iff ( x in [.a,b.] & S1[x] ) )
from XBOOLE_0:sch 1();
for x being object st x in C holds
x is real
then reconsider C = C as real-membered set by MEMBERED:def 3;
A5:
b is UpperBound of [.a,b.]
by XXREAL_2:21;
C c= [.a,b.]
by A2;
then A6:
b is UpperBound of C
by A5, XXREAL_2:6;
then
( not C is empty & C is bounded_above & C is real-membered )
by A3, A2, XXREAL_2:def 10;
then reconsider c = sup C as Real ;
A7:
c in [.a,b.]
then
c in dom jauge
by FUNCT_2:def 1;
then A8:
jauge . c in rng jauge
by FUNCT_1:3;
then A9:
c - (jauge . c) < c
by XREAL_1:44, PARTFUN3:def 1;
C c= REAL
by MEMBERED:3;
then
C c= ExtREAL
by NUMBERS:31;
then
C is non empty Subset of ExtREAL
by A3, A2;
then consider d being Element of ExtREAL such that
A10:
d in C
and
A11:
c - (jauge . c) < d
by A9, XXREAL_2:94;
consider D0 being non empty increasing FinSequence of REAL , T0 being non empty FinSequence of REAL such that
A12:
D0 . 1 = a
and
A13:
D0 . (len D0) = d
and
A13bis:
T0 . 1 = a
and
A14:
dom D0 = dom T0
and
A15:
for i being Nat st i - 1 in dom T0 & i in dom T0 holds
( (T0 . i) - (jauge . (T0 . i)) <= D0 . (i - 1) & D0 . (i - 1) <= T0 . i )
and
A16:
for i being Nat st i in dom T0 holds
( T0 . i <= D0 . i & D0 . i <= (T0 . i) + (jauge . (T0 . i)) )
by A10, A2;
set D1 = D0 ^ <*c*>;
set T1 = T0 ^ <*c*>;
A17:
( c in C & S1[c] )
proof
per cases
( d = c or d <> c )
;
suppose A18:
d <> c
;
( c in C & S1[c] )A19:
d <= sup C
by A10, XXREAL_2:4;
then
D0 . (len D0) < c
by A13, A18, XXREAL_0:1;
then A20:
D0 . (len D0) < <*c*> . 1
by FINSEQ_1:def 8;
now ( c in [.a,b.] & S1[c] )thus
c in [.a,b.]
by A7;
S1[c]now ex D2 being non empty increasing FinSequence of REAL ex T2 being non empty FinSequence of REAL st
( D2 . 1 = a & D2 . (len D2) = c & T2 . 1 = a & dom D2 = dom T2 & ( for i being Nat st i - 1 in dom T2 & i in dom T2 holds
( (T2 . i) - (jauge . (T2 . i)) <= D2 . (i - 1) & D2 . (i - 1) <= T2 . i ) ) & ( for i being Nat st i in dom T2 holds
( T2 . i <= D2 . i & D2 . i <= (T2 . i) + (jauge . (T2 . i)) ) ) )reconsider D2 =
D0 ^ <*c*> as non
empty increasing FinSequence of
REAL by A20, Th1;
reconsider T2 =
T0 ^ <*c*> as non
empty FinSequence of
REAL ;
take D2 =
D2;
ex T2 being non empty FinSequence of REAL st
( D2 . 1 = a & D2 . (len D2) = c & T2 . 1 = a & dom D2 = dom T2 & ( for i being Nat st i - 1 in dom T2 & i in dom T2 holds
( (T2 . i) - (jauge . (T2 . i)) <= D2 . (i - 1) & D2 . (i - 1) <= T2 . i ) ) & ( for i being Nat st i in dom T2 holds
( T2 . i <= D2 . i & D2 . i <= (T2 . i) + (jauge . (T2 . i)) ) ) )take T2 =
T2;
( D2 . 1 = a & D2 . (len D2) = c & T2 . 1 = a & dom D2 = dom T2 & ( for i being Nat st i - 1 in dom T2 & i in dom T2 holds
( (T2 . i) - (jauge . (T2 . i)) <= D2 . (i - 1) & D2 . (i - 1) <= T2 . i ) ) & ( for i being Nat st i in dom T2 holds
( T2 . i <= D2 . i & D2 . i <= (T2 . i) + (jauge . (T2 . i)) ) ) )
rng D0 <> {}
;
then
1
in dom D0
by FINSEQ_3:32;
hence
D2 . 1
= a
by A12, FINSEQ_1:def 7;
( D2 . (len D2) = c & T2 . 1 = a & dom D2 = dom T2 & ( for i being Nat st i - 1 in dom T2 & i in dom T2 holds
( (T2 . i) - (jauge . (T2 . i)) <= D2 . (i - 1) & D2 . (i - 1) <= T2 . i ) ) & ( for i being Nat st i in dom T2 holds
( T2 . i <= D2 . i & D2 . i <= (T2 . i) + (jauge . (T2 . i)) ) ) )A21:
len D2 =
(len D0) + (len <*c*>)
by FINSEQ_1:22
.=
(len D0) + 1
by FINSEQ_1:39
;
1
in Seg 1
by FINSEQ_1:1;
then
1
in dom <*c*>
by FINSEQ_1:def 8;
then D2 . (len D2) =
<*c*> . 1
by A21, FINSEQ_1:def 7
.=
c
by FINSEQ_1:def 8
;
hence
D2 . (len D2) = c
;
( T2 . 1 = a & dom D2 = dom T2 & ( for i being Nat st i - 1 in dom T2 & i in dom T2 holds
( (T2 . i) - (jauge . (T2 . i)) <= D2 . (i - 1) & D2 . (i - 1) <= T2 . i ) ) & ( for i being Nat st i in dom T2 holds
( T2 . i <= D2 . i & D2 . i <= (T2 . i) + (jauge . (T2 . i)) ) ) )
rng T0 <> {}
;
then
1
in dom T0
by FINSEQ_3:32;
hence
T2 . 1
= a
by A13bis, FINSEQ_1:def 7;
( dom D2 = dom T2 & ( for i being Nat st i - 1 in dom T2 & i in dom T2 holds
( (T2 . i) - (jauge . (T2 . i)) <= D2 . (i - 1) & D2 . (i - 1) <= T2 . i ) ) & ( for i being Nat st i in dom T2 holds
( T2 . i <= D2 . i & D2 . i <= (T2 . i) + (jauge . (T2 . i)) ) ) )A22:
Seg (len D0) =
dom T0
by A14, FINSEQ_1:def 3
.=
Seg (len T0)
by FINSEQ_1:def 3
;
A23:
dom D2 =
Seg ((len D0) + (len <*c*>))
by FINSEQ_1:def 7
.=
Seg ((len T0) + (len <*c*>))
by A22, FINSEQ_1:6
.=
dom (T0 ^ <*c*>)
by FINSEQ_1:def 7
;
hence
dom D2 = dom T2
;
( ( for i being Nat st i - 1 in dom T2 & i in dom T2 holds
( (T2 . i) - (jauge . (T2 . i)) <= D2 . (i - 1) & D2 . (i - 1) <= T2 . i ) ) & ( for i being Nat st i in dom T2 holds
( T2 . i <= D2 . i & D2 . i <= (T2 . i) + (jauge . (T2 . i)) ) ) )A24:
Seg (len D2) = dom T2
by A23, FINSEQ_1:def 3;
hereby for i being Nat st i in dom T2 holds
( T2 . i <= D2 . i & D2 . i <= (T2 . i) + (jauge . (T2 . i)) )
let i be
Nat;
( i - 1 in dom T2 & i in dom T2 implies ( (T2 . b1) - (jauge . (T2 . b1)) <= D2 . (b1 - 1) & D2 . (b1 - 1) <= T2 . b1 ) )assume that A25:
i - 1
in dom T2
and A26:
i in dom T2
;
( (T2 . b1) - (jauge . (T2 . b1)) <= D2 . (b1 - 1) & D2 . (b1 - 1) <= T2 . b1 )A27:
(
i - 1
in dom T0 or ex
n1 being
Nat st
(
n1 in dom <*c*> &
i - 1
= (len T0) + n1 ) )
by A25, FINSEQ_1:25;
A28:
( ex
n1 being
Nat st
(
n1 in dom <*c*> &
i - 1
= (len T0) + n1 ) implies
i = (len T0) + 2 )
per cases
( i in dom T0 or ex n0 being Nat st
( n0 in dom <*c*> & i = (len T0) + n0 ) )
by A26, FINSEQ_1:25;
suppose
ex
n0 being
Nat st
(
n0 in dom <*c*> &
i = (len T0) + n0 )
;
( (T2 . b1) - (jauge . (T2 . b1)) <= D2 . (b1 - 1) & D2 . (b1 - 1) <= T2 . b1 )then consider n0 being
Nat such that A43:
n0 in dom <*c*>
and A44:
i = (len T0) + n0
;
A45:
n0 in Seg 1
by A43, FINSEQ_1:def 8;
then A46:
n0 = 1
by TARSKI:def 1, FINSEQ_1:2;
1
in Seg 1
by FINSEQ_1:1;
then
1
in dom <*c*>
by FINSEQ_1:def 8;
then
T2 . i = <*c*> . 1
by A46, A44, FINSEQ_1:def 7;
then A47:
T2 . i = c
by FINSEQ_1:def 8;
D0 . (i - 1) = d
by A13, A46, A44, A22, FINSEQ_1:6;
hence
(
(T2 . i) - (jauge . (T2 . i)) <= D2 . (i - 1) &
D2 . (i - 1) <= T2 . i )
by A11, A19, A47, A45, A44, A27, A28, A14, FINSEQ_1:def 7, TARSKI:def 1, FINSEQ_1:2;
verum end; end;
end; hereby verum
let i be
Nat;
( i in dom T2 implies ( T2 . b1 <= D2 . b1 & D2 . b1 <= (T2 . b1) + (jauge . (T2 . b1)) ) )assume
i in dom T2
;
( T2 . b1 <= D2 . b1 & D2 . b1 <= (T2 . b1) + (jauge . (T2 . b1)) )per cases then
( i in dom T0 or ex n0 being Nat st
( n0 in dom <*c*> & i = (len T0) + n0 ) )
by FINSEQ_1:25;
suppose
ex
n0 being
Nat st
(
n0 in dom <*c*> &
i = (len T0) + n0 )
;
( T2 . b1 <= D2 . b1 & D2 . b1 <= (T2 . b1) + (jauge . (T2 . b1)) )then consider n0 being
Nat such that A50:
n0 in dom <*c*>
and A51:
i = (len T0) + n0
;
A52:
1
in Seg 1
by FINSEQ_1:1;
then A53:
1
in dom <*c*>
by FINSEQ_1:def 8;
A54:
n0 in Seg 1
by A50, FINSEQ_1:def 8;
then
n0 = 1
by FINSEQ_1:2, TARSKI:def 1;
then A55:
T2 . i = <*c*> . 1
by A53, A51, FINSEQ_1:def 7;
len T0 = len D0
by A22, FINSEQ_1:6;
then A56:
i = (len D0) + 1
by A54, FINSEQ_1:2, TARSKI:def 1, A51;
1
in dom <*c*>
by A52, FINSEQ_1:def 8;
then A57:
D2 . i =
<*c*> . 1
by A56, FINSEQ_1:def 7
.=
c
by FINSEQ_1:def 8
;
dom jauge = [.a,b.]
by FUNCT_2:def 1;
then
T2 . i in dom jauge
by A7, A55, FINSEQ_1:def 8;
then
jauge . (T2 . i) in rng jauge
by FUNCT_1:3;
then
(T2 . i) + 0 < (T2 . i) + (jauge . (T2 . i))
by PARTFUN3:def 1, XREAL_1:8;
hence
(
T2 . i <= D2 . i &
D2 . i <= (T2 . i) + (jauge . (T2 . i)) )
by A55, FINSEQ_1:def 8, A57;
verum end; end;
end; end; hence
S1[
c]
;
verum end; hence
(
c in C &
S1[
c] )
by A2;
verum end; end;
end;
c = b
proof
assume A58:
c <> b
;
contradiction
A59:
(
a <= c &
c <= b )
by A7, XXREAL_1:1;
set c2 =
min (
(c + ((jauge . c) / 2)),
b);
A60:
(
min (
(c + ((jauge . c) / 2)),
b)
in C &
S1[
min (
(c + ((jauge . c) / 2)),
b)] )
proof
set D1 =
D0 ^ <*(min ((c + ((jauge . c) / 2)),b))*>;
set T1 =
T0 ^ <*c*>;
per cases
( d = min ((c + ((jauge . c) / 2)),b) or d <> min ((c + ((jauge . c) / 2)),b) )
;
suppose A61:
d <> min (
(c + ((jauge . c) / 2)),
b)
;
( min ((c + ((jauge . c) / 2)),b) in C & S1[ min ((c + ((jauge . c) / 2)),b)] )A62:
0 < jauge . c
by A8, PARTFUN3:def 1;
reconsider d =
d as
Real by A10;
A63:
d + 0 < c + ((jauge . c) / 2)
by A10, XXREAL_2:4, A62, XREAL_1:8;
A64:
d < b
d + 0 < c + ((jauge . c) / 2)
by A10, XXREAL_2:4, A62, XREAL_1:8;
then
D0 . (len D0) < min (
(c + ((jauge . c) / 2)),
b)
by A13, A64, XXREAL_0:21;
then A66:
D0 . (len D0) < <*(min ((c + ((jauge . c) / 2)),b))*> . 1
by FINSEQ_1:def 8;
now ( min ((c + ((jauge . c) / 2)),b) in [.a,b.] & min ((c + ((jauge . c) / 2)),b) in [.a,b.] & S1[ min ((c + ((jauge . c) / 2)),b)] )thus A67:
min (
(c + ((jauge . c) / 2)),
b)
in [.a,b.]
( min ((c + ((jauge . c) / 2)),b) in [.a,b.] & S1[ min ((c + ((jauge . c) / 2)),b)] )proof
A68:
min (
(c + ((jauge . c) / 2)),
b)
<= b
by XXREAL_0:17;
c in [.a,b.]
by A17, A2;
then A69:
(
a <= c &
c <= b )
by XXREAL_1:1;
0 < jauge . c
by A8, PARTFUN3:def 1;
then
a + 0 < c + ((jauge . c) / 2)
by A69, XREAL_1:8;
then
a <= min (
(c + ((jauge . c) / 2)),
b)
by A1, XXREAL_0:20;
hence
min (
(c + ((jauge . c) / 2)),
b)
in [.a,b.]
by A68, XXREAL_1:1;
verum
end; now ex D2 being non empty increasing FinSequence of REAL ex T2 being non empty FinSequence of REAL st
( D2 . 1 = a & D2 . (len D2) = min ((c + ((jauge . c) / 2)),b) & T2 . 1 = a & dom D2 = dom T2 & ( for i being Nat st i - 1 in dom T2 & i in dom T2 holds
( (T2 . i) - (jauge . (T2 . i)) <= D2 . (i - 1) & D2 . (i - 1) <= T2 . i ) ) & ( for i being Nat st i in dom T2 holds
( T2 . i <= D2 . i & D2 . i <= (T2 . i) + (jauge . (T2 . i)) ) ) )reconsider D2 =
D0 ^ <*(min ((c + ((jauge . c) / 2)),b))*> as non
empty increasing FinSequence of
REAL by A66, Th1;
reconsider T2 =
T0 ^ <*c*> as non
empty FinSequence of
REAL ;
take D2 =
D2;
ex T2 being non empty FinSequence of REAL st
( D2 . 1 = a & D2 . (len D2) = min ((c + ((jauge . c) / 2)),b) & T2 . 1 = a & dom D2 = dom T2 & ( for i being Nat st i - 1 in dom T2 & i in dom T2 holds
( (T2 . i) - (jauge . (T2 . i)) <= D2 . (i - 1) & D2 . (i - 1) <= T2 . i ) ) & ( for i being Nat st i in dom T2 holds
( T2 . i <= D2 . i & D2 . i <= (T2 . i) + (jauge . (T2 . i)) ) ) )take T2 =
T2;
( D2 . 1 = a & D2 . (len D2) = min ((c + ((jauge . c) / 2)),b) & T2 . 1 = a & dom D2 = dom T2 & ( for i being Nat st i - 1 in dom T2 & i in dom T2 holds
( (T2 . i) - (jauge . (T2 . i)) <= D2 . (i - 1) & D2 . (i - 1) <= T2 . i ) ) & ( for i being Nat st i in dom T2 holds
( T2 . i <= D2 . i & D2 . i <= (T2 . i) + (jauge . (T2 . i)) ) ) )
rng D0 <> {}
;
then
1
in dom D0
by FINSEQ_3:32;
hence
D2 . 1
= a
by A12, FINSEQ_1:def 7;
( D2 . (len D2) = min ((c + ((jauge . c) / 2)),b) & T2 . 1 = a & dom D2 = dom T2 & ( for i being Nat st i - 1 in dom T2 & i in dom T2 holds
( (T2 . i) - (jauge . (T2 . i)) <= D2 . (i - 1) & D2 . (i - 1) <= T2 . i ) ) & ( for i being Nat st i in dom T2 holds
( T2 . i <= D2 . i & D2 . i <= (T2 . i) + (jauge . (T2 . i)) ) ) )A70:
len D2 =
(len D0) + (len <*(min ((c + ((jauge . c) / 2)),b))*>)
by FINSEQ_1:22
.=
(len D0) + 1
by FINSEQ_1:39
;
1
in Seg 1
by FINSEQ_1:1;
then
1
in dom <*(min ((c + ((jauge . c) / 2)),b))*>
by FINSEQ_1:def 8;
then D2 . (len D2) =
<*(min ((c + ((jauge . c) / 2)),b))*> . 1
by A70, FINSEQ_1:def 7
.=
min (
(c + ((jauge . c) / 2)),
b)
by FINSEQ_1:def 8
;
hence
D2 . (len D2) = min (
(c + ((jauge . c) / 2)),
b)
;
( T2 . 1 = a & dom D2 = dom T2 & ( for i being Nat st i - 1 in dom T2 & i in dom T2 holds
( (T2 . i) - (jauge . (T2 . i)) <= D2 . (i - 1) & D2 . (i - 1) <= T2 . i ) ) & ( for i being Nat st i in dom T2 holds
( T2 . i <= D2 . i & D2 . i <= (T2 . i) + (jauge . (T2 . i)) ) ) )
rng T0 <> {}
;
then
1
in dom T0
by FINSEQ_3:32;
hence
T2 . 1
= a
by A13bis, FINSEQ_1:def 7;
( dom D2 = dom T2 & ( for i being Nat st i - 1 in dom T2 & i in dom T2 holds
( (T2 . i) - (jauge . (T2 . i)) <= D2 . (i - 1) & D2 . (i - 1) <= T2 . i ) ) & ( for i being Nat st i in dom T2 holds
( T2 . i <= D2 . i & D2 . i <= (T2 . i) + (jauge . (T2 . i)) ) ) )A71:
Seg (len D0) =
dom T0
by A14, FINSEQ_1:def 3
.=
Seg (len T0)
by FINSEQ_1:def 3
;
A72:
dom D2 =
Seg (len (D0 ^ <*(min ((c + ((jauge . c) / 2)),b))*>))
by FINSEQ_1:def 3
.=
Seg ((len D0) + 1)
by FINSEQ_2:16
.=
Seg ((len T0) + 1)
by A71, FINSEQ_1:6
.=
Seg (len (T0 ^ <*c*>))
by FINSEQ_2:16
.=
dom (T0 ^ <*c*>)
by FINSEQ_1:def 3
;
hence
dom D2 = dom T2
;
( ( for i being Nat st i - 1 in dom T2 & i in dom T2 holds
( (T2 . i) - (jauge . (T2 . i)) <= D2 . (i - 1) & D2 . (i - 1) <= T2 . i ) ) & ( for i being Nat st i in dom T2 holds
( T2 . i <= D2 . i & D2 . i <= (T2 . i) + (jauge . (T2 . i)) ) ) )A73:
Seg (len D2) = dom T2
by A72, FINSEQ_1:def 3;
hereby for i being Nat st i in dom T2 holds
( T2 . i <= D2 . i & D2 . i <= (T2 . i) + (jauge . (T2 . i)) )
let i be
Nat;
( i - 1 in dom T2 & i in dom T2 implies ( (T2 . b1) - (jauge . (T2 . b1)) <= D2 . (b1 - 1) & D2 . (b1 - 1) <= T2 . b1 ) )assume that A74:
i - 1
in dom T2
and A75:
i in dom T2
;
( (T2 . b1) - (jauge . (T2 . b1)) <= D2 . (b1 - 1) & D2 . (b1 - 1) <= T2 . b1 )A76:
( ex
n1 being
Nat st
(
n1 in dom <*c*> &
i - 1
= (len T0) + n1 ) implies
i = (len T0) + 2 )
per cases
( i in dom T0 or ex n0 being Nat st
( n0 in dom <*c*> & i = (len T0) + n0 ) )
by A75, FINSEQ_1:25;
suppose
ex
n0 being
Nat st
(
n0 in dom <*c*> &
i = (len T0) + n0 )
;
( (T2 . b1) - (jauge . (T2 . b1)) <= D2 . (b1 - 1) & D2 . (b1 - 1) <= T2 . b1 )then consider n0 being
Nat such that A83:
n0 in dom <*c*>
and A84:
i = (len T0) + n0
;
A85:
n0 in Seg 1
by A83, FINSEQ_1:def 8;
then A86:
n0 = 1
by TARSKI:def 1, FINSEQ_1:2;
A87:
i - 1
in dom T0
by A74, A76, FINSEQ_1:25, A84, A85, TARSKI:def 1, FINSEQ_1:2;
1
in Seg 1
by FINSEQ_1:1;
then
1
in dom <*c*>
by FINSEQ_1:def 8;
then
T2 . i = <*c*> . 1
by A86, A84, FINSEQ_1:def 7;
then A88:
T2 . i = c
by FINSEQ_1:def 8;
D0 . (i - 1) = d
by A13, A86, A84, A71, FINSEQ_1:6;
then
(
c - (jauge . c) <= D0 . (i - 1) &
D0 . (i - 1) <= c )
by A10, XXREAL_2:4, A11;
hence
(
(T2 . i) - (jauge . (T2 . i)) <= D2 . (i - 1) &
D2 . (i - 1) <= T2 . i )
by A88, A87, A14, FINSEQ_1:def 7;
verum end; end;
end; hereby verum
let i be
Nat;
( i in dom T2 implies ( T2 . b1 <= D2 . b1 & D2 . b1 <= (T2 . b1) + (jauge . (T2 . b1)) ) )assume
i in dom T2
;
( T2 . b1 <= D2 . b1 & D2 . b1 <= (T2 . b1) + (jauge . (T2 . b1)) )per cases then
( i in dom T0 or ex n0 being Nat st
( n0 in dom <*c*> & i = (len T0) + n0 ) )
by FINSEQ_1:25;
suppose
ex
n0 being
Nat st
(
n0 in dom <*c*> &
i = (len T0) + n0 )
;
( T2 . b1 <= D2 . b1 & D2 . b1 <= (T2 . b1) + (jauge . (T2 . b1)) )then consider n0 being
Nat such that A91:
n0 in dom <*c*>
and A92:
i = (len T0) + n0
;
1
in Seg 1
by FINSEQ_1:1;
then A93:
1
in dom <*c*>
by FINSEQ_1:def 8;
A94:
n0 in Seg 1
by A91, FINSEQ_1:def 8;
then
n0 = 1
by FINSEQ_1:2, TARSKI:def 1;
then
T2 . i = <*c*> . 1
by A93, A92, FINSEQ_1:def 7;
then A95:
T2 . i = c
by FINSEQ_1:def 8;
len T0 = len D0
by A71, FINSEQ_1:6;
then A96:
i = (len D0) + 1
by A94, A92, FINSEQ_1:2, TARSKI:def 1;
1
in Seg 1
by FINSEQ_1:1;
then
1
in dom <*(min ((c + ((jauge . c) / 2)),b))*>
by FINSEQ_1:def 8;
then A97:
D2 . i =
<*(min ((c + ((jauge . c) / 2)),b))*> . 1
by A96, FINSEQ_1:def 7
.=
min (
(c + ((jauge . c) / 2)),
b)
by FINSEQ_1:def 8
;
A98:
c <= b
by A7, XXREAL_1:1;
A99:
0 < jauge . c
by A8, PARTFUN3:def 1;
then A100:
c + 0 <= c + ((jauge . c) / 2)
by XREAL_1:8;
A101:
(c + ((jauge . c) / 2)) + 0 < (c + ((jauge . c) / 2)) + ((jauge . c) / 2)
by A99, XREAL_1:8;
min (
(c + ((jauge . c) / 2)),
b)
<= c + ((jauge . c) / 2)
by XXREAL_0:17;
hence
(
T2 . i <= D2 . i &
D2 . i <= (T2 . i) + (jauge . (T2 . i)) )
by A101, XXREAL_0:2, A95, A97, A100, A98, XXREAL_0:20;
verum end; end;
end; end; hence
(
min (
(c + ((jauge . c) / 2)),
b)
in [.a,b.] &
S1[
min (
(c + ((jauge . c) / 2)),
b)] )
by A67;
verum end; hence
(
min (
(c + ((jauge . c) / 2)),
b)
in C &
S1[
min (
(c + ((jauge . c) / 2)),
b)] )
by A2;
verum end; end;
end;
0 < jauge . c
by A8, PARTFUN3:def 1;
then A102:
c + 0 < c + ((jauge . c) / 2)
by XREAL_1:8;
c < b
by A59, A58, XXREAL_0:1;
then
c < min (
(c + ((jauge . c) / 2)),
b)
by A102, XXREAL_0:def 9;
hence
contradiction
by A60, XXREAL_2:4;
verum
end;
hence
ex x being non empty increasing FinSequence of REAL ex t being non empty FinSequence of REAL st
( x . 1 = a & x . (len x) = b & t . 1 = a & dom x = dom t & ( for i being Nat st i - 1 in dom t & i in dom t holds
( (t . i) - (jauge . (t . i)) <= x . (i - 1) & x . (i - 1) <= t . i ) ) & ( for i being Nat st i in dom t holds
( t . i <= x . i & x . i <= (t . i) + (jauge . (t . i)) ) ) )
by A17; verum