let a, b be Real; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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
proof
let x be object ; :: thesis: ( x in C implies x is real )
assume x in C ; :: thesis: x is real
then x in [.a,b.] by A2;
hence x is real ; :: thesis: verum
end;
then reconsider C = C as real-membered set by MEMBERED:def 3;
A3: now :: thesis: ( a in [.a,b.] & S1[a] )
thus a in [.a,b.] by A1, XXREAL_1:1; :: thesis: S1[a]
now :: thesis: ex x, t being FinSequence of REAL st
( x . 1 = a & x . (len x) = a & 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)) ) ) )
set x = <*a*>;
set t = <*a*>;
take x = <*a*>; :: thesis: ex t being FinSequence of REAL st
( x . 1 = a & x . (len x) = a & 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)) ) ) )
take t = <*a*>; :: thesis: ( x . 1 = a & x . (len x) = a & 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)) ) ) )
( len x = 1 & len t = 1 ) by FINSEQ_1:39;
hence ( x . 1 = a & x . (len x) = a & t . 1 = a ) by FINSEQ_1:def 8; :: thesis: ( 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)) ) ) )
thus dom x = dom t ; :: thesis: ( ( 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)) ) ) )
thus 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 ) :: thesis: for i being Nat st i in dom t holds
( t . i <= x . i & x . i <= (t . i) + (jauge . (t . i)) )
proof
let i be Nat; :: thesis: ( i - 1 in dom t & i in dom t implies ( (t . i) - (jauge . (t . i)) <= x . (i - 1) & x . (i - 1) <= t . i ) )
assume ( i - 1 in dom t & i in dom t ) ; :: thesis: ( (t . i) - (jauge . (t . i)) <= x . (i - 1) & x . (i - 1) <= t . i )
then ( i - 1 in {1} & i in {1} ) by FINSEQ_1:2, FINSEQ_1:def 8;
then ( i - 1 = 1 & i = 1 ) by TARSKI:def 1;
hence ( (t . i) - (jauge . (t . i)) <= x . (i - 1) & x . (i - 1) <= t . i ) ; :: thesis: verum
end;
thus for i being Nat st i in dom t holds
( t . i <= x . i & x . i <= (t . i) + (jauge . (t . i)) ) :: thesis: verum
proof
let i be Nat; :: thesis: ( i in dom t implies ( t . i <= x . i & x . i <= (t . i) + (jauge . (t . i)) ) )
assume i in dom t ; :: thesis: ( t . i <= x . i & x . i <= (t . i) + (jauge . (t . i)) )
then i in {1} by FINSEQ_1:2, FINSEQ_1:def 8;
then A4: i = 1 by TARSKI:def 1;
thus t . i <= x . i ; :: thesis: x . i <= (t . i) + (jauge . (t . i))
t . i = a by A4, FINSEQ_1:def 8;
then t . i in [.a,b.] by A1, XXREAL_1:1;
then t . i in dom jauge by FUNCT_2:def 1;
then jauge . (t . i) in rng jauge by FUNCT_1:3;
then (x . i) + 0 < (t . i) + (jauge . (t . i)) by XREAL_1:8, PARTFUN3:def 1;
hence x . i <= (t . i) + (jauge . (t . i)) ; :: thesis: verum
end;
end;
hence S1[a] ; :: thesis: verum
end;
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.]
proof
assume not c in [.a,b.] ; :: thesis: contradiction
per cases then ( c < a or b < c ) by XXREAL_1:1;
end;
end;
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 d = c ; :: thesis: ( c in C & S1[c] )
hence ( c in C & S1[c] ) by A10, A12, A13, A13bis, A14, A15, A16; :: thesis: verum
end;
suppose A18: d <> c ; :: thesis: ( 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 :: thesis: ( c in [.a,b.] & S1[c] )
thus c in [.a,b.] by A7; :: thesis: S1[c]
now :: thesis: 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; :: thesis: 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; :: thesis: ( 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; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: ( 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 ; :: thesis: ( ( 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 :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( (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 )
proof
given n1 being Nat such that A29: n1 in dom <*c*> and
A30: i - 1 = (len T0) + n1 ; :: thesis: i = (len T0) + 2
n1 in Seg 1 by A29, FINSEQ_1:def 8;
then n1 = 1 by TARSKI:def 1, FINSEQ_1:2;
hence i = (len T0) + 2 by A30; :: thesis: verum
end;
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 A40: i in dom T0 ; :: thesis: ( (T2 . b1) - (jauge . (T2 . b1)) <= D2 . (b1 - 1) & D2 . (b1 - 1) <= T2 . b1 )
then A41: T2 . i = T0 . i by FINSEQ_1:def 7;
per cases ( i - 1 in dom T0 or i = (len T0) + 2 ) by A25, FINSEQ_1:25, A28;
suppose A42: i - 1 in dom T0 ; :: thesis: ( (T2 . b1) - (jauge . (T2 . b1)) <= D2 . (b1 - 1) & D2 . (b1 - 1) <= T2 . b1 )
then ( (T0 . i) - (jauge . (T0 . i)) <= D0 . (i - 1) & D0 . (i - 1) <= T0 . i ) by A40, A15;
hence ( (T2 . i) - (jauge . (T2 . i)) <= D2 . (i - 1) & D2 . (i - 1) <= T2 . i ) by A41, A42, A14, FINSEQ_1:def 7; :: thesis: verum
end;
suppose i = (len T0) + 2 ; :: thesis: ( (T2 . b1) - (jauge . (T2 . b1)) <= D2 . (b1 - 1) & D2 . (b1 - 1) <= T2 . b1 )
then (len T0) + 2 <= len T2 by A26, FINSEQ_3:25;
then (len T0) + 2 <= len D2 by A24, FINSEQ_1:def 3;
then (len T0) + 2 <= (len T0) + 1 by A21, A22, FINSEQ_1:6;
then ((len T0) + 2) - (len T0) <= ((len T0) + 1) - (len T0) by XREAL_1:13;
hence ( (T2 . i) - (jauge . (T2 . i)) <= D2 . (i - 1) & D2 . (i - 1) <= T2 . i ) ; :: thesis: verum
end;
end;
end;
suppose ex n0 being Nat st
( n0 in dom <*c*> & i = (len T0) + n0 ) ; :: thesis: ( (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; :: thesis: verum
end;
end;
end;
hereby :: thesis: verum
let i be Nat; :: thesis: ( i in dom T2 implies ( T2 . b1 <= D2 . b1 & D2 . b1 <= (T2 . b1) + (jauge . (T2 . b1)) ) )
assume i in dom T2 ; :: thesis: ( 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 A48: i in dom T0 ; :: thesis: ( T2 . b1 <= D2 . b1 & D2 . b1 <= (T2 . b1) + (jauge . (T2 . b1)) )
then A49: T2 . i = T0 . i by FINSEQ_1:def 7;
D2 . i = D0 . i by A48, A14, FINSEQ_1:def 7;
hence ( T2 . i <= D2 . i & D2 . i <= (T2 . i) + (jauge . (T2 . i)) ) by A16, A49, A48; :: thesis: verum
end;
suppose ex n0 being Nat st
( n0 in dom <*c*> & i = (len T0) + n0 ) ; :: thesis: ( 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; :: thesis: verum
end;
end;
end;
end;
hence S1[c] ; :: thesis: verum
end;
hence ( c in C & S1[c] ) by A2; :: thesis: verum
end;
end;
end;
c = b
proof
assume A58: c <> b ; :: thesis: 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 d = min ((c + ((jauge . c) / 2)),b) ; :: thesis: ( min ((c + ((jauge . c) / 2)),b) in C & S1[ min ((c + ((jauge . c) / 2)),b)] )
hence ( min ((c + ((jauge . c) / 2)),b) in C & S1[ min ((c + ((jauge . c) / 2)),b)] ) by A10, A2; :: thesis: verum
end;
suppose A61: d <> min ((c + ((jauge . c) / 2)),b) ; :: thesis: ( 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
proof
assume A65: b <= d ; :: thesis: contradiction
d in [.a,b.] by A10, A2;
then ( a <= d & d <= b ) by XXREAL_1:1;
then min ((c + ((jauge . c) / 2)),b) = min (d,(c + ((jauge . c) / 2))) by A65, XXREAL_0:1;
hence contradiction by A63, XXREAL_0:def 9, A61; :: thesis: verum
end;
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 :: thesis: ( 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.] :: thesis: ( 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; :: thesis: verum
end;
now :: thesis: 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; :: thesis: 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; :: thesis: ( 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; :: thesis: ( 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) ; :: thesis: ( 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; :: thesis: ( 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 ; :: thesis: ( ( 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 :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( (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 )
proof
given n1 being Nat such that A77: n1 in dom <*c*> and
A78: i - 1 = (len T0) + n1 ; :: thesis: i = (len T0) + 2
n1 in Seg 1 by A77, FINSEQ_1:def 8;
then i - 1 = (len T0) + 1 by A78, TARSKI:def 1, FINSEQ_1:2;
hence i = (len T0) + 2 ; :: thesis: verum
end;
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 A79: i in dom T0 ; :: thesis: ( (T2 . b1) - (jauge . (T2 . b1)) <= D2 . (b1 - 1) & D2 . (b1 - 1) <= T2 . b1 )
then A80: T2 . i = T0 . i by FINSEQ_1:def 7;
per cases ( i - 1 in dom T0 or i = (len T0) + 2 ) by A74, FINSEQ_1:25, A76;
suppose A81: i - 1 in dom T0 ; :: thesis: ( (T2 . b1) - (jauge . (T2 . b1)) <= D2 . (b1 - 1) & D2 . (b1 - 1) <= T2 . b1 )
then ( (T0 . i) - (jauge . (T0 . i)) <= D0 . (i - 1) & D0 . (i - 1) <= T0 . i ) by A79, A15;
hence ( (T2 . i) - (jauge . (T2 . i)) <= D2 . (i - 1) & D2 . (i - 1) <= T2 . i ) by A80, A81, A14, FINSEQ_1:def 7; :: thesis: verum
end;
suppose A82: i = (len T0) + 2 ; :: thesis: ( (T2 . b1) - (jauge . (T2 . b1)) <= D2 . (b1 - 1) & D2 . (b1 - 1) <= T2 . b1 )
i <= len T2 by A75, FINSEQ_3:25;
then (len T0) + 2 <= len D2 by A82, A73, FINSEQ_1:def 3;
then (len T0) + 2 <= (len T0) + 1 by A70, A71, FINSEQ_1:6;
then ((len T0) + 2) - (len T0) <= ((len T0) + 1) - (len T0) by XREAL_1:13;
hence ( (T2 . i) - (jauge . (T2 . i)) <= D2 . (i - 1) & D2 . (i - 1) <= T2 . i ) ; :: thesis: verum
end;
end;
end;
suppose ex n0 being Nat st
( n0 in dom <*c*> & i = (len T0) + n0 ) ; :: thesis: ( (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; :: thesis: verum
end;
end;
end;
hereby :: thesis: verum
let i be Nat; :: thesis: ( i in dom T2 implies ( T2 . b1 <= D2 . b1 & D2 . b1 <= (T2 . b1) + (jauge . (T2 . b1)) ) )
assume i in dom T2 ; :: thesis: ( 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 A89: i in dom T0 ; :: thesis: ( T2 . b1 <= D2 . b1 & D2 . b1 <= (T2 . b1) + (jauge . (T2 . b1)) )
then A90: T2 . i = T0 . i by FINSEQ_1:def 7;
D2 . i = D0 . i by A89, A14, FINSEQ_1:def 7;
hence ( T2 . i <= D2 . i & D2 . i <= (T2 . i) + (jauge . (T2 . i)) ) by A16, A90, A89; :: thesis: verum
end;
suppose ex n0 being Nat st
( n0 in dom <*c*> & i = (len T0) + n0 ) ; :: thesis: ( 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; :: thesis: verum
end;
end;
end;
end;
hence ( min ((c + ((jauge . c) / 2)),b) in [.a,b.] & S1[ min ((c + ((jauge . c) / 2)),b)] ) by A67; :: thesis: verum
end;
hence ( min ((c + ((jauge . c) / 2)),b) in C & S1[ min ((c + ((jauge . c) / 2)),b)] ) by A2; :: thesis: 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; :: thesis: 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; :: thesis: verum