let a, b be Real; :: thesis:
let jauge be positive-yielding Function of [.a,b.],REAL; :: thesis:
assume A1: a <= b ; :: thesis:
defpred S₁[ 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.] & S₁[x] ) ) from XBOOLE_0:sch 1();
for x being object st x in C holds
x is real

let x be object ; :: thesis:
assume x in C ; :: thesis:
then x in [.a,b.] by A2;
hence x is real ; :: thesis:

end;

then reconsider C = C as real-membered set by MEMBERED:def 3;

A3: now :: thesis:

thus a in [.a,b.] by A1, XXREAL_1:1; :: thesis:

now :: thesis:

set x = <*a*>;
set t = <*a*>;
take x = <*a*>; :: thesis:
take t = <*a*>; :: thesis:
( len x = 1 & len t = 1 ) by FINSEQ_1:39;
hence ( x . 1 = a & x . (len x) = a & t . 1 = a ) ; :: thesis:
thus dom x = dom t ; :: thesis:
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:

proof

let i be Nat; :: thesis:
assume ( i - 1 in dom t & i in dom t ) ; :: thesis:
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:

end;

thus for i being Nat st i in dom t holds
( t . i <= x . i & x . i <= (t . i) + (jauge . (t . i)) ) :: thesis:

proof

let i be Nat; :: thesis:
assume i in dom t ; :: thesis:
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:
t . i = a by A4;
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:

end;

hence S₁[a] ; :: thesis:

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:

per cases by XXREAL_1:1;

suppose c < a ; :: thesis:

hence contradiction by A3, A2, XXREAL_2:4; :: thesis:

end;

suppose b < c ; :: thesis:

hence contradiction by A6, XXREAL_2:def 3; :: thesis:

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 & S₁[c] )

proof

per cases ;

suppose d = c ; :: thesis:

hence ( c in C & S₁[c] ) by A10, A12, A13, A13bis, A14, A15, A16; :: thesis:

end;

suppose A18: d <> c ; :: thesis:

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 ;

now :: thesis:

thus c in [.a,b.] by A7; :: thesis:

now :: thesis:

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:
take T2 = T2; :: thesis:
rng D0 <> {} ;
then 1 in dom D0 by FINSEQ_3:32;
hence D2 . 1 = a by A12, FINSEQ_1:def 7; :: thesis:
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 ;
hence D2 . (len D2) = c ; :: thesis:
rng T0 <> {} ;
then 1 in dom T0 by FINSEQ_3:32;
hence T2 . 1 = a by A13bis, FINSEQ_1:def 7; :: thesis:
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:
A24: Seg (len D2) = dom T2 by A23, FINSEQ_1:def 3;

hereby :: thesis:

let i be Nat; :: thesis:
assume that
A25: i - 1 in dom T2 and
A26: i in dom T2 ; :: thesis:
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:
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:

end;

per cases by A26, FINSEQ_1:25;

suppose A40: i in dom T0 ; :: thesis:

then A41: T2 . i = T0 . i by FINSEQ_1:def 7;

per cases by A25, FINSEQ_1:25, A28;

suppose A42: i - 1 in dom T0 ; :: thesis:

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:

end;

suppose i = (len T0) + 2 ; :: thesis:

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:

end;

suppose ex n0 being Nat st
( n0 in dom <*c*> & i = (len T0) + n0 ) ; :: thesis:

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 ;
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:

end;

hereby :: thesis:

let i be Nat; :: thesis:
assume i in dom T2 ; :: thesis:

per cases by FINSEQ_1:25;

suppose A48: i in dom T0 ; :: thesis:

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:

end;

suppose ex n0 being Nat st
( n0 in dom <*c*> & i = (len T0) + n0 ) ; :: thesis:

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 ;
dom jauge = [.a,b.] by FUNCT_2:def 1;
then T2 . i in dom jauge by A7, A55;
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, A57; :: thesis:

end;

hence S₁[c] ; :: thesis:

end;

hence ( c in C & S₁[c] ) by A2; :: thesis:

end;

c = b

proof

assume A58: c <> b ; :: thesis:
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 & S₁[ min ((c + ((jauge . c) / 2)),b)] )

proof

set D1 = D0 ^ <*(min ((c + ((jauge . c) / 2)),b))*>;
set T1 = T0 ^ <*c*>;

per cases ;

suppose d = min ((c + ((jauge . c) / 2)),b) ; :: thesis:

hence ( min ((c + ((jauge . c) / 2)),b) in C & S₁[ min ((c + ((jauge . c) / 2)),b)] ) by A10, A2; :: thesis:

end;

suppose A61: d <> min ((c + ((jauge . c) / 2)),b) ; :: thesis:

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:
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:

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 ;

now :: thesis:

thus A67: min ((c + ((jauge . c) / 2)),b) in [.a,b.] :: thesis:

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:

end;

now :: thesis:

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:
take T2 = T2; :: thesis:
rng D0 <> {} ;
then 1 in dom D0 by FINSEQ_3:32;
hence D2 . 1 = a by A12, FINSEQ_1:def 7; :: thesis:
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) ;
hence D2 . (len D2) = min ((c + ((jauge . c) / 2)),b) ; :: thesis:
rng T0 <> {} ;
then 1 in dom T0 by FINSEQ_3:32;
hence T2 . 1 = a by A13bis, FINSEQ_1:def 7; :: thesis:
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:
A73: Seg (len D2) = dom T2 by A72, FINSEQ_1:def 3;

hereby :: thesis:

let i be Nat; :: thesis:
assume that
A74: i - 1 in dom T2 and
A75: i in dom T2 ; :: thesis:
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:
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:

end;

per cases by A75, FINSEQ_1:25;

suppose A79: i in dom T0 ; :: thesis:

then A80: T2 . i = T0 . i by FINSEQ_1:def 7;

per cases by A74, FINSEQ_1:25, A76;

suppose A81: i - 1 in dom T0 ; :: thesis:

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:

end;

suppose A82: i = (len T0) + 2 ; :: thesis:

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:

end;

suppose ex n0 being Nat st
( n0 in dom <*c*> & i = (len T0) + n0 ) ; :: thesis:

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 ;
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:

end;

hereby :: thesis:

let i be Nat; :: thesis:
assume i in dom T2 ; :: thesis:

per cases by FINSEQ_1:25;

suppose A89: i in dom T0 ; :: thesis:

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:

end;

suppose ex n0 being Nat st
( n0 in dom <*c*> & i = (len T0) + n0 ) ; :: thesis:

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 ;
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) ;
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:

end;

hence ( min ((c + ((jauge . c) / 2)),b) in [.a,b.] & S₁[ min ((c + ((jauge . c) / 2)),b)] ) by A67; :: thesis:

end;

hence ( min ((c + ((jauge . c) / 2)),b) in C & S₁[ min ((c + ((jauge . c) / 2)),b)] ) by A2; :: thesis:

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:

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: