cousin.miz



    begin

    theorem :: COUSIN:1

    

     Th1: for p,q be non empty increasing FinSequence of REAL st (p . ( len p)) < (q . 1) holds (p ^ q) is non empty increasing FinSequence of REAL

    proof

      let p,q be non empty increasing FinSequence of REAL ;

      assume

       A1: (p . ( len p)) < (q . 1);

      set pq = (p ^ q);

      now

        let e1,e2 be ExtReal;

        assume that

         A2: e1 in ( dom pq) and

         A3: e2 in ( dom pq) and

         A4: e1 < e2;

        per cases by A2, A3, FINSEQ_1: 25;

          suppose

           A5: e1 in ( dom p) & e2 in ( dom p);

          then

           A6: (pq . e1) = (p . e1) & (pq . e2) = (p . e2) by FINSEQ_1:def 7;

          e1 < e2 & p is increasing by A4;

          hence (pq . e1) < (pq . e2) by A5, A6;

        end;

          suppose

           A7: e1 in ( dom p) & ex n be Nat st n in ( dom q) & e2 = (( len p) + n);

          then

          consider n0 be Nat such that

           A8: n0 in ( dom q) and

           A9: e2 = (( len p) + n0);

          

           A10: (pq . e1) = (p . e1) & (pq . e2) = (q . n0) by A7, A9, FINSEQ_1:def 7;

          ( rng q) <> {} ;

          then

           A11: 1 in ( dom q) by FINSEQ_3: 32;

          1 <= n0 by A8, FINSEQ_3: 25;

          then 1 = n0 or 1 < n0 by XXREAL_0: 1;

          then

           A12: (q . 1) <= (q . n0) by A8, A11, VALUED_0:def 13;

          ( rng p) <> {} ;

          then 1 in ( dom p) by FINSEQ_3: 32;

          then 1 <= ( len p) by FINSEQ_3: 25;

          then

           A13: ( len p) in ( dom p) by FINSEQ_3: 25;

          e1 <= ( len p) by A7, FINSEQ_3: 25;

          then e1 < ( len p) or e1 = ( len p) by XXREAL_0: 1;

          then (p . e1) <= (p . ( len p)) by A13, A7, VALUED_0:def 13;

          then (p . e1) < (q . 1) by A1, XXREAL_0: 2;

          hence (pq . e1) < (pq . e2) by A10, A12, XXREAL_0: 2;

        end;

          suppose

           A14: (ex n be Nat st n in ( dom q) & e1 = (( len p) + n)) & e2 in ( dom p);

          then

          consider n0 be Nat such that n0 in ( dom q) and

           A15: e1 = (( len p) + n0);

          

           A16: ( len p) <= e1 by A15, NAT_1: 11;

          e2 in ( Seg ( len p)) by A14, FINSEQ_1:def 3;

          then e2 <= ( len p) by FINSEQ_1: 1;

          hence (pq . e1) < (pq . e2) by A4, A16, XXREAL_0: 2;

        end;

          suppose

           A17: (ex n be Nat st n in ( dom q) & e1 = (( len p) + n)) & (ex n be Nat st n in ( dom q) & e2 = (( len p) + n));

          then

          consider n1 be Nat such that

           A18: n1 in ( dom q) and

           A19: e1 = (( len p) + n1);

          consider n2 be Nat such that

           A20: n2 in ( dom q) and

           A21: e2 = (( len p) + n2) by A17;

          

           A22: ((( len p) + n1) - ( len p)) < ((( len p) + n2) - ( len p)) by A4, A19, A21, XREAL_1: 14;

          (q . n1) = (pq . e1) & (q . n2) = (pq . e2) by A18, A19, A20, A21, FINSEQ_1:def 7;

          hence (pq . e1) < (pq . e2) by A22, A18, A20, VALUED_0:def 13;

        end;

      end;

      then (p ^ q) is increasing;

      hence thesis;

    end;

    theorem :: COUSIN:2

    for a,b be Real st 1 < a & 0 < b < 1 holds ( log (a,b)) < 0

    proof

      let a,b be Real;

      assume that

       A1: 1 < a and

       A2: 0 < b < 1;

      ( log (a,1)) = 0 by A1, POWER: 51;

      hence thesis by A1, A2, POWER: 57;

    end;

    theorem :: COUSIN:3

    

     Th2: for a,b be Real st 1 < a & 1 < b holds 0 < ( log (a,b))

    proof

      let a,b be Real;

      assume that

       A1: 1 < a and

       A2: 1 < b;

      ( log (a,1)) = 0 by A1, POWER: 51;

      hence thesis by A1, A2, POWER: 57;

    end;

    theorem :: COUSIN:4

    

     Th5: for x be object holds ( product <* {x}*>) = { <*x*>}

    proof

      let x be object;

       the set of all <*y*> where y be Element of {x} = { <*x*>}

      proof

        set SA = the set of all <*y*> where y be Element of {x};

        

         A1: for t be object st t in SA holds t in { <*x*>}

        proof

          let t be object;

          assume t in the set of all <*y*> where y be Element of {x};

          then

          consider y0 be Element of {x} such that

           A2: t = <*y0*>;

          t = <*x*> by A2, TARSKI:def 1;

          hence thesis by TARSKI:def 1;

        end;

        for t be object st t in { <*x*>} holds t in SA

        proof

          let t be object;

          assume t in { <*x*>};

          then t = <*x*> & x is Element of {x} by TARSKI:def 1;

          hence thesis;

        end;

        then SA c= { <*x*>} & { <*x*>} c= SA by A1;

        hence thesis;

      end;

      hence thesis by SRINGS_4: 24;

    end;

    theorem :: COUSIN:5

    

     Th6: for x be Element of ( REAL 1) holds ex rx be Real st x = <*rx*>

    proof

      let x be Element of ( REAL 1);

      x is Element of ( TOP-REAL 1) by EUCLID: 22;

      then

      consider rx be Real such that

       A1: x = <*rx*> by JORDAN2B: 20;

      thus thesis by A1;

    end;

    theorem :: COUSIN:6

    

     Th7: for a be Real holds <*a*> is Point of ( Euclid 1)

    proof

      let a be Real;

      reconsider ra = <*a*> as FinSequence of REAL ;

      ( dom ra) = ( Seg 1) by FINSEQ_1:def 8;

      then ( len ra) = 1 by FINSEQ_1:def 3;

      hence thesis by TOPREAL3: 45;

    end;

    theorem :: COUSIN:7

    

     Th8: for a,b be Real st a <= b holds a <= ((a + b) / 2) <= b

    proof

      let a,b be Real;

      assume

       A1: a <= b;

      (2 * a) = (a + a);

      then (2 * a) <= (a + b) by A1, XREAL_1: 7;

      then ((2 * a) / 2) <= ((a + b) / 2) by XREAL_1: 72;

      hence a <= ((a + b) / 2);

      (a + b) <= (b + b) by A1, XREAL_1: 7;

      then ((a + b) / 2) <= ((2 * b) / 2) by XREAL_1: 72;

      hence thesis;

    end;

    theorem :: COUSIN:8

    for a,b,c be Real st a <= b & b < c holds a < ((b + c) / 2)

    proof

      let a,b,c be Real;

      assume that

       A1: a <= b and

       A2: b < c;

      

       A3: (a + b) < (b + c) by A1, A2, XREAL_1: 8;

      (a + a) <= (a + b) by A1, XREAL_1: 7;

      then (2 * a) < (b + c) by A3, XXREAL_0: 2;

      then ((2 * a) / 2) < ((b + c) / 2) by XREAL_1: 74;

      hence thesis;

    end;

    theorem :: COUSIN:9

    for a,b be Real st a < b holds ((a + b) / 2) < b

    proof

      let a,b be Real;

      assume a < b;

      then (a + b) < (b + b) by XREAL_1: 8;

      then ((a + b) / 2) < ((2 * b) / 2) by XREAL_1: 74;

      hence thesis;

    end;

    theorem :: COUSIN:10

    for a,b be Real st a <= b holds [.a, b.] is non empty compact Subset of REAL by XXREAL_1: 30;

    theorem :: COUSIN:11

    for f be FinSequence st 2 <= ( len f) holds ((f /^ 1) . ( len (f /^ 1))) = (f . ( len f))

    proof

      let f be FinSequence;

      assume

       A1: 2 <= ( len f);

      set g = (f /^ 1);

      

       A2: 1 <= ( len f) by A1, XXREAL_0: 2;

      

      then

       A3: (( len g) + 1) = ((( len f) - 1) + 1) by RFINSEQ:def 1

      .= ( len f);

      then (2 - 1) <= ((( len g) + 1) - 1) by A1, XREAL_1: 13;

      then ( len g) in ( Seg ( len g)) by FINSEQ_1: 3;

      then ( len g) in ( dom g) by FINSEQ_1:def 3;

      hence thesis by A3, A2, RFINSEQ:def 1;

    end;

    begin

    reserve n for Nat;

    reserve s1 for sequence of ( Euclid n),

s2 for sequence of ( REAL-NS n);

    theorem :: COUSIN:12

    

     Th9: for x,y be Element of ( Euclid n), g,h be Point of ( REAL-NS n) st x = g & y = h holds ( dist (x,y)) = ||.(g - h).||

    proof

      let x,y be Element of ( Euclid n), g,h be Point of ( REAL-NS n);

      assume

       A1: x = g & y = h;

      x in ( Euclid n) & y in ( Euclid n);

      then x in ( TOP-REAL n) & y in ( TOP-REAL n) by EUCLID: 67;

      then

      reconsider rx = x, ry = y as Element of ( REAL n) by EUCLID: 22;

      

       A2: ( Euclid n) = MetrStruct (# ( REAL n), ( Pitag_dist n) #) by EUCLID:def 7;

      reconsider g1 = g, h1 = h as Element of ( REAL n) by REAL_NS1:def 4;

      reconsider z1 = (g1 - h1) as Element of ( REAL n);

       ||.(g - h).|| = (the normF of ( REAL-NS n) . (g1 - h1)) by REAL_NS1: 5

      .= (( Euclid_norm n) . z1) by REAL_NS1:def 4

      .= |.z1.| by REAL_NS1:def 3;

      hence thesis by A1, A2, EUCLID:def 6;

    end;

    theorem :: COUSIN:13

    

     Th10: the carrier of ( REAL-NS n) = the carrier of ( Euclid n)

    proof

      

      thus the carrier of ( Euclid n) = the carrier of ( TOP-REAL n) by EUCLID: 67

      .= ( REAL n) by EUCLID: 22

      .= the carrier of ( REAL-NS n) by REAL_NS1:def 4;

    end;

    theorem :: COUSIN:14

    

     Th11: s1 = s2 implies (s1 is Cauchy iff s2 is Cauchy_sequence_by_Norm)

    proof

      assume

       A1: s1 = s2;

      thus s1 is Cauchy implies s2 is Cauchy_sequence_by_Norm

      proof

        assume

         A3: s1 is Cauchy;

        now

          let r be Real;

          assume r > 0 ;

          then

          consider p be Nat such that

           A4: for n,m be Nat st p <= n & p <= m holds ( dist ((s1 . n),(s1 . m))) < r by A3;

          take p;

          hereby

            let n0,m0 be Nat;

            assume

             A5: n0 >= p & m0 >= p;

            ( dist ((s1 . n0),(s1 . m0))) = ||.((s2 . n0) - (s2 . m0)).|| by A1, Th9;

            hence ||.((s2 . n0) - (s2 . m0)).|| < r by A5, A4;

          end;

        end;

        hence s2 is Cauchy_sequence_by_Norm by RSSPACE3: 8;

      end;

      assume

       A9: s2 is Cauchy_sequence_by_Norm;

      now

        let r be Real;

        assume r > 0 ;

        then

        consider k be Nat such that

         A10: for n,m be Nat st n >= k & m >= k holds ||.((s2 . n) - (s2 . m)).|| < r by A9, RSSPACE3: 8;

        hereby

          take k;

          hereby

            let n0,m0 be Nat;

            assume

             A11: k <= n0 & k <= m0;

             ||.((s2 . n0) - (s2 . m0)).|| = ( dist ((s1 . n0),(s1 . m0))) by A1, Th9;

            hence ( dist ((s1 . n0),(s1 . m0))) < r by A11, A10;

          end;

        end;

        hence ex p be Nat st for n,m be Nat st p <= n & p <= m holds ( dist ((s1 . n),(s1 . m))) < r;

      end;

      hence s1 is Cauchy;

    end;

    theorem :: COUSIN:15

    

     Th12: s1 = s2 implies (s1 is convergent iff s2 is convergent)

    proof

      assume

       A1: s1 = s2;

      hereby

        assume s1 is convergent;

        then

        consider x be Element of ( Euclid n) such that

         A2: for r be Real st r > 0 holds ex n0 be Nat st for m be Nat st n0 <= m holds ( dist ((s1 . m),x)) < r;

        x is Element of ( TOP-REAL n) by EUCLID: 67;

        then x is Element of ( REAL n) by EUCLID: 22;

        then

        reconsider g = x as Point of ( REAL-NS n) by REAL_NS1:def 4;

        now

          take g;

          hereby

            let r be Real;

            assume 0 < r;

            then

            consider n0 be Nat such that

             A3: for m be Nat st n0 <= m holds ( dist ((s1 . m),x)) < r by A2;

            hereby

              take n0;

              hereby

                let n1 be Nat;

                assume n0 <= n1;

                then ( dist ((s1 . n1),x)) < r & (s1 . n1) = (s2 . n1) by A1, A3;

                hence ||.((s2 . n1) - g).|| < r by Th9;

              end;

            end;

          end;

        end;

        hence s2 is convergent;

      end;

      assume s2 is convergent;

      then

      consider g be Point of ( REAL-NS n) such that

       A4: for r be Real st 0 < r holds ex m be Nat st for n0 be Nat st m <= n0 holds ||.((s2 . n0) - g).|| < r;

      g is Element of ( REAL n) by REAL_NS1:def 4;

      then g is Element of ( TOP-REAL n) by EUCLID: 22;

      then

      reconsider x = g as Element of ( Euclid n) by EUCLID: 67;

      now

        take x;

        hereby

          let r be Real;

          assume r > 0 ;

          then

          consider m0 be Nat such that

           A5: for n0 be Nat st m0 <= n0 holds ||.((s2 . n0) - g).|| < r by A4;

          hereby

            take m0;

            hereby

              let m be Nat;

              assume m0 <= m;

              then ||.((s2 . m) - g).|| < r & (s2 . m) = (s1 . m) by A1, A5;

              hence ( dist ((s1 . m),x)) < r by Th9;

            end;

          end;

        end;

      end;

      hence s1 is convergent;

    end;

    theorem :: COUSIN:16

    

     Th13: for S2 be sequence of ( Euclid n) st S2 is Cauchy holds S2 is convergent

    proof

      let S2 be sequence of ( Euclid n);

      assume

       A1: S2 is Cauchy;

      reconsider S2NS = S2 as sequence of ( REAL-NS n) by Th10;

      S2NS is Cauchy_sequence_by_Norm by A1, Th11;

      then S2NS is convergent by LOPBAN_1:def 15;

      hence S2 is convergent by Th12;

    end;

    theorem :: COUSIN:17

    ( Euclid n) is complete by Th13;

    begin

    theorem :: COUSIN:18

    

     Th14: ( distance_by_norm_of ( REAL-NS n)) = ( Pitag_dist n)

    proof

      the carrier of ( REAL-NS n) = ( REAL n) by REAL_NS1:def 4;

      then

      reconsider d1 = ( distance_by_norm_of ( REAL-NS n)) as Function of [:( REAL n), ( REAL n):], REAL ;

      now

        let x,y be set;

        assume

         A1: x in ( REAL n) & y in ( REAL n);

        then x is Element of ( TOP-REAL n) & y is Element of ( TOP-REAL n) by EUCLID: 22;

        then

        reconsider px = x, py = y as Element of ( Euclid n) by EUCLID: 67;

        reconsider g = x, h = y as Point of ( REAL-NS n) by A1, REAL_NS1:def 4;

        ( Euclid n) = MetrStruct (# ( REAL n), ( Pitag_dist n) #) by EUCLID:def 7;

        

        hence (( Pitag_dist n) . (x,y)) = ( dist (px,py))

        .= ||.(g - h).|| by Th9

        .= (d1 . (x,y)) by NORMSP_2:def 1;

      end;

      hence thesis by BINOP_1:def 21;

    end;

    theorem :: COUSIN:19

    

     Th15: ( MetricSpaceNorm ( REAL-NS n)) = ( Euclid n)

    proof

      set MS = ( MetricSpaceNorm ( REAL-NS n));

      

       A1: MS = MetrStruct (# the carrier of ( REAL-NS n), ( distance_by_norm_of ( REAL-NS n)) #) by NORMSP_2:def 2;

      then

       A2: the carrier of MS = ( REAL n) by REAL_NS1:def 4;

      ( Euclid n) = MetrStruct (# ( REAL n), ( Pitag_dist n) #) by EUCLID:def 7;

      hence thesis by A1, A2, Th14;

    end;

    registration

      let n be Nat;

      cluster ( Euclid n) -> complete;

      coherence

      proof

        ( MetricSpaceNorm ( REAL-NS n)) = ( Euclid n) by Th15;

        hence thesis;

      end;

    end

    begin

    definition

      let a,b be Real_Sequence;

      :: COUSIN:def1

      func IntervalSequence (a,b) -> SetSequence of ( REAL 1) means

      : Def1: for i be Nat holds (it . i) = ( product <* [.(a . i), (b . i).]*>);

      existence

      proof

        defpred P[ object, object] means $2 = ( product <* [.(a . $1), (b . $1).]*>);

        

         A1: for x be object st x in NAT holds ex y be object st y in ( bool ( REAL 1)) & P[x, y]

        proof

          let x be object;

          assume x in NAT ;

          set y = ( product <* [.(a . x), (b . x).]*>);

          take y;

          ( product <* [.(a . x), (b . x).]*>) c= ( REAL 1)

          proof

            let t be object;

            assume t in ( product <* [.(a . x), (b . x).]*>);

            then

            consider f be Function such that

             A2: t = f and

             A3: ( dom f) = ( dom <* [.(a . x), (b . x).]*>) and

             A4: for i be object st i in ( dom <* [.(a . x), (b . x).]*>) holds (f . i) in ( <* [.(a . x), (b . x).]*> . i) by CARD_3:def 5;

            

             A5: ( dom <* [.(a . x), (b . x).]*>) = ( Seg 1) by FINSEQ_1:def 8;

            

             A6: ( dom f) = ( Seg 1) by A3, FINSEQ_1:def 8;

            ( rng f) c= REAL

            proof

              let u be object;

              assume u in ( rng f);

              then

              consider t be object such that

               A7: t in ( dom f) and

               A8: u = (f . t) by FUNCT_1:def 3;

              t in {1} by FINSEQ_1: 2, A7, A3, FINSEQ_1:def 8;

              then

               A9: t = 1 & 1 in ( Seg 1) by FINSEQ_1: 2, TARSKI:def 1;

              u = (f . 1) & 1 in ( dom <* [.(a . x), (b . x).]*>) by A7, A3, FINSEQ_1: 2, TARSKI:def 1, A8, A5;

              then (f . 1) in ( <* [.(a . x), (b . x).]*> . 1) by A4;

              then u in [.(a . x), (b . x).] by A9, A8, FINSEQ_1:def 8;

              hence thesis;

            end;

            then t in ( Funcs (( Seg 1), REAL )) by A2, FUNCT_2:def 2, A6;

            then t in (1 -tuples_on REAL ) by FINSEQ_2: 93;

            hence t in ( REAL 1) by EUCLID:def 1;

          end;

          hence y in ( bool ( REAL 1));

          thus P[x, y];

        end;

        ex f be Function of NAT , ( bool ( REAL 1)) st for x be object st x in NAT holds P[x, (f . x)] from FUNCT_2:sch 1( A1);

        then

        consider f be Function of NAT , ( bool ( REAL 1)) such that

         A10: for x be object st x in NAT holds P[x, (f . x)];

        now

          take f;

          for x be Nat holds P[x, (f . x)] by ORDINAL1:def 12, A10;

          hence ex f be Function of NAT , ( bool ( REAL 1)) st for x be Nat holds P[x, (f . x)];

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be SetSequence of ( REAL 1) such that

         A11: for i be Nat holds (f1 . i) = ( product <* [.(a . i), (b . i).]*>) and

         A12: for i be Nat holds (f2 . i) = ( product <* [.(a . i), (b . i).]*>);

        consider g1 be Function of NAT , ( bool ( REAL 1)) such that

         A13: g1 = f1 and

         A14: for i be Nat holds (g1 . i) = ( product <* [.(a . i), (b . i).]*>) by A11;

        consider g2 be Function of NAT , ( bool ( REAL 1)) such that

         A15: g2 = f2 and

         A16: for i be Nat holds (g2 . i) = ( product <* [.(a . i), (b . i).]*>) by A12;

        

         A17: ( dom g1) = NAT & ( dom g2) = NAT by FUNCT_2:def 1;

        for x be object st x in ( dom g1) holds (g1 . x) = (g2 . x)

        proof

          let x be object;

          assume x in ( dom g1);

          then (g1 . x) = ( product <* [.(a . x), (b . x).]*>) & (g2 . x) = ( product <* [.(a . x), (b . x).]*>) by A14, A16;

          hence thesis;

        end;

        hence f1 = f2 by A13, A15, A17;

      end;

    end

    theorem :: COUSIN:20

    

     Th17: for a,b be Real_Sequence holds ( IntervalSequence (a,b)) is SetSequence of ( Euclid 1)

    proof

      let a,b be Real_Sequence;

      ( REAL 1) = the carrier of ( TOP-REAL 1) by EUCLID: 22

      .= the carrier of ( Euclid 1) by EUCLID: 67;

      hence thesis;

    end;

    theorem :: COUSIN:21

    

     Th18: ( product <* REAL *>) = ( REAL 1)

    proof

      

       A8: ( product <* REAL *>) c= ( REAL 1)

      proof

        let x be object;

        assume x in ( product <* REAL *>);

        then

        consider g be Function such that

         A1: x = g and

         A2: ( dom g) = ( dom <* REAL *>) and

         A3: for j be object st j in ( dom <* REAL *>) holds (g . j) in ( <* REAL *> . j) by CARD_3:def 5;

        

         A4: ( dom g) = ( Seg 1) by A2, FINSEQ_1:def 8;

        ( rng g) c= REAL

        proof

          let u be object;

          assume u in ( rng g);

          then

          consider t be object such that

           A5: t in ( dom g) and

           A6: u = (g . t) by FUNCT_1:def 3;

          t in {1} by A5, FINSEQ_1: 2, A2, FINSEQ_1:def 8;

          then

           A7: t = 1 & 1 in ( Seg 1) by FINSEQ_1: 2, TARSKI:def 1;

          u = (g . 1) & 1 in ( dom <* REAL *>) by A6, A7, FINSEQ_1:def 8;

          then (g . 1) in ( <* REAL *> . 1) by A3;

          hence thesis by A7, A6, FINSEQ_1:def 8;

        end;

        then x in ( Funcs (( Seg 1), REAL )) by A1, FUNCT_2:def 2, A4;

        then x in (1 -tuples_on REAL ) by FINSEQ_2: 93;

        hence x in ( REAL 1) by EUCLID:def 1;

      end;

      ( REAL 1) c= ( product <* REAL *>)

      proof

        let x be object;

        assume

         A9: x in ( REAL 1);

        then x in (1 -tuples_on REAL ) by EUCLID:def 1;

        then

         A10: x in ( Funcs (( Seg 1), REAL )) by FINSEQ_2: 93;

        reconsider g = x as Function by A9;

        now

          consider h be Function such that

           A11: h = g and

           A12: ( dom h) = ( Seg 1) and

           A13: ( rng h) c= REAL by A10, FUNCT_2:def 2;

          thus ( dom g) = ( dom <* REAL *>) by A11, A12, FINSEQ_1:def 8;

          hereby

            let j be object;

            assume

             A14: j in ( dom <* REAL *>);

            then

             A15: j in ( Seg 1) by FINSEQ_1:def 8;

            j in {1} by FINSEQ_1: 2, A14, FINSEQ_1:def 8;

            then

             A16: j = 1 by TARSKI:def 1;

            (g . j) in REAL by A11, A13, A12, A15, FUNCT_1: 3;

            hence (g . j) in ( <* REAL *> . j) by A16, FINSEQ_1:def 8;

          end;

          hence for j be object st j in ( dom <* REAL *>) holds (g . j) in ( <* REAL *> . j);

        end;

        hence x in ( product <* REAL *>) by CARD_3:def 5;

      end;

      hence thesis by A8;

    end;

    theorem :: COUSIN:22

    

     Th19: for a,b be Real, xa,xb be Point of ( Euclid 1) st xa = <*a*> & xb = <*b*> holds ( dist (xa,xb)) = |.(a - b).|

    proof

      let a,b be Real, xa,xb be Point of ( Euclid 1);

      assume that

       A1: xa = <*a*> and

       A2: xb = <*b*>;

      xa in ( Euclid 1) & xb in ( Euclid 1);

      then xa in ( TOP-REAL 1) & xb in ( TOP-REAL 1) by EUCLID: 67;

      then

      reconsider ra = xa, rb = xb as Element of ( REAL 1) by EUCLID: 22;

      

       A3: ( Euclid 1) = MetrStruct (# ( REAL 1), ( Pitag_dist 1) #) by EUCLID:def 7;

      

       A4: ra = (1 |-> a) by A1, FINSEQ_2: 59;

      rb = (1 |-> b) by A2, FINSEQ_2: 59;

      

      then |.(ra - rb).| = (( sqrt 1) * |.(a - b).|) by A4, TOPREALC: 11

      .= |.(a - b).| by SQUARE_1: 18;

      hence thesis by A3, EUCLID:def 6;

    end;

    theorem :: COUSIN:23

    

     Th20: for a,b be Real, S be Subset of ( Euclid 1) st a <= b & S = ( product <* [.a, b.]*>) holds for x,y be Point of ( Euclid 1) st x in S & y in S holds ( dist (x,y)) <= (b - a)

    proof

      let a,b be Real, S be Subset of ( Euclid 1);

      assume that

       A1: a <= b and

       A2: S = ( product <* [.a, b.]*>);

      set si = ( product <* [.a, b.]*>);

      reconsider si as Subset of ( Euclid 1) by A2;

      set r = (b - a);

      for x,y be Point of ( Euclid 1) st x in si & y in si holds ( dist (x,y)) <= (b - a)

      proof

        set r = (b - a);

        per cases by A1, XREAL_1: 48;

          suppose

           A3: r = 0 ;

          

          then

           A4: ( product <* [.a, b.]*>) = ( product <* {a}*>) by XXREAL_1: 17

          .= { <*a*>} by Th5;

          now

            set r = (b - a);

            hereby

              let x,y be Point of ( Euclid 1);

              assume x in si & y in si;

              then

               A5: x = <*a*> & y = <*a*> by A4, TARSKI:def 1;

              ( Euclid 1) is Reflexive;

              hence ( dist (x,y)) <= (b - a) by A3, A5, METRIC_1:def 2;

            end;

          end;

          hence for x,y be Point of ( Euclid 1) st x in si & y in si holds ( dist (x,y)) <= (b - a);

        end;

          suppose 0 < r;

          hereby

            let x,y be Point of ( Euclid 1);

            assume that

             A6: x in si and

             A7: y in si;

            consider gx be Function such that

             A8: x = gx and ( dom gx) = ( dom <* [.a, b.]*>) and

             A9: for j be object st j in ( dom <* [.a, b.]*>) holds (gx . j) in ( <* [.a, b.]*> . j) by A6, CARD_3:def 5;

            consider gy be Function such that

             A10: y = gy and ( dom gy) = ( dom <* [.a, b.]*>) and

             A11: for j be object st j in ( dom <* [.a, b.]*>) holds (gy . j) in ( <* [.a, b.]*> . j) by A7, CARD_3:def 5;

            x in ( Euclid 1) & y in ( Euclid 1);

            then x in ( TOP-REAL 1) & y in ( TOP-REAL 1) by EUCLID: 67;

            then

            reconsider rx = x, ry = y as Element of ( REAL 1) by EUCLID: 22;

            ( Euclid 1) = MetrStruct (# ( REAL 1), ( Pitag_dist 1) #) by EUCLID:def 7;

            then

             A12: ( dist (x,y)) = |.(rx - ry).| by EUCLID:def 6;

            consider ux be Real such that

             A13: rx = <*ux*> by Th6;

            consider uy be Real such that

             A14: ry = <*uy*> by Th6;

            rx = (1 |-> ux) & ry = (1 |-> uy) by A13, A14, FINSEQ_2: 59;

            

            then

             A15: |.(rx - ry).| = (( sqrt 1) * |.(ux - uy).|) by TOPREALC: 11

            .= |.(ux - uy).| by SQUARE_1: 18;

            1 in ( Seg 1) by TARSKI:def 1, FINSEQ_1: 2;

            then 1 in ( dom <* [.a, b.]*>) by FINSEQ_1:def 8;

            then (gx . 1) in ( <* [.a, b.]*> . 1) & (gy . 1) in ( <* [.a, b.]*> . 1) by A9, A11;

            then (gx . 1) in [.a, b.] & (gy . 1) in [.a, b.] by FINSEQ_1:def 8;

            then ux in [.a, b.] & uy in [.a, b.] by A8, A10, A13, A14, FINSEQ_1:def 8;

            hence ( dist (x,y)) <= r by A12, A15, UNIFORM1: 12;

          end;

        end;

      end;

      hence thesis by A2;

    end;

    theorem :: COUSIN:24

    

     Th21: for a,b be Real, S be Subset of ( Euclid 1) st a <= b & S = ( product <* [.a, b.]*>) holds S is bounded

    proof

      let a,b be Real, S be Subset of ( Euclid 1);

      assume that

       A1: a <= b and

       A2: S = ( product <* [.a, b.]*>);

      set si = ( product <* [.a, b.]*>);

      reconsider si as Subset of ( Euclid 1) by A2;

      ex r be Real st 0 < r & for x,y be Point of ( Euclid 1) st x in si & y in si holds ( dist (x,y)) <= r

      proof

        set r = (b - a);

        per cases by A1, XREAL_1: 48;

          suppose r = 0 ;

          

          then

           A3: ( product <* [.a, b.]*>) = ( product <* {a}*>) by XXREAL_1: 17

          .= { <*a*>} by Th5;

          now

            set r = 1;

            take r;

            thus 0 < r;

            hereby

              let x,y be Point of ( Euclid 1);

              assume x in si & y in si;

              then

               A4: x = <*a*> & y = <*a*> by A3, TARSKI:def 1;

              ( Euclid 1) is Reflexive;

              hence ( dist (x,y)) <= r by A4, METRIC_1:def 2;

            end;

          end;

          hence ex r be Real st 0 < r & for x,y be Point of ( Euclid 1) st x in si & y in si holds ( dist (x,y)) <= r;

        end;

          suppose

           A5: 0 < r;

          take r;

          thus 0 < r by A5;

          hereby

            let x,y be Point of ( Euclid 1);

            assume that

             A6: x in si and

             A7: y in si;

            consider gx be Function such that

             A8: x = gx and ( dom gx) = ( dom <* [.a, b.]*>) and

             A9: for j be object st j in ( dom <* [.a, b.]*>) holds (gx . j) in ( <* [.a, b.]*> . j) by A6, CARD_3:def 5;

            consider gy be Function such that

             A10: y = gy and ( dom gy) = ( dom <* [.a, b.]*>) and

             A11: for j be object st j in ( dom <* [.a, b.]*>) holds (gy . j) in ( <* [.a, b.]*> . j) by A7, CARD_3:def 5;

            x in ( Euclid 1) & y in ( Euclid 1);

            then x in ( TOP-REAL 1) & y in ( TOP-REAL 1) by EUCLID: 67;

            then

            reconsider rx = x, ry = y as Element of ( REAL 1) by EUCLID: 22;

            ( Euclid 1) = MetrStruct (# ( REAL 1), ( Pitag_dist 1) #) by EUCLID:def 7;

            then

             A12: ( dist (x,y)) = |.(rx - ry).| by EUCLID:def 6;

            consider ux be Real such that

             A13: rx = <*ux*> by Th6;

            consider uy be Real such that

             A14: ry = <*uy*> by Th6;

            rx = (1 |-> ux) & ry = (1 |-> uy) by A13, A14, FINSEQ_2: 59;

            

            then

             A15: |.(rx - ry).| = (( sqrt 1) * |.(ux - uy).|) by TOPREALC: 11

            .= |.(ux - uy).| by SQUARE_1: 18;

            1 in ( Seg 1) by TARSKI:def 1, FINSEQ_1: 2;

            then 1 in ( dom <* [.a, b.]*>) by FINSEQ_1:def 8;

            then (gx . 1) in ( <* [.a, b.]*> . 1) & (gy . 1) in ( <* [.a, b.]*> . 1) by A9, A11;

            then (gx . 1) in [.a, b.] & (gy . 1) in [.a, b.] by FINSEQ_1:def 8;

            then ux in [.a, b.] & uy in [.a, b.] by A8, A10, A13, A14, FINSEQ_1:def 8;

            hence ( dist (x,y)) <= r by UNIFORM1: 12, A15, A12;

          end;

        end;

      end;

      hence thesis by A2;

    end;

    theorem :: COUSIN:25

    

     Th22: for a,b be Real_Sequence st (for i be Nat holds (a . i) <= (b . i) & (a . i) <= (a . (i + 1)) & (b . (i + 1)) <= (b . i)) holds ( IntervalSequence (a,b)) is non-empty pointwise_bounded closed SetSequence of ( Euclid 1)

    proof

      let a,b be Real_Sequence;

      assume

       A1: for i be Nat holds (a . i) <= (b . i) & (a . i) <= (a . (i + 1)) & (b . (i + 1)) <= (b . i);

      reconsider s = ( IntervalSequence (a,b)) as SetSequence of ( Euclid 1) by Th17;

      

       A2: s is non-empty

      proof

        assume not thesis;

        then

        consider i be object such that

         A3: i in ( dom s) and

         A4: (s . i) = {} ;

        ( product <* [.(a . i), (b . i).]*>) = {} by A3, A4, Def1;

        then {} in ( rng <* [.(a . i), (b . i).]*>) by CARD_3: 26;

        then

        consider j be object such that

         A5: j in ( dom <* [.(a . i), (b . i).]*>) and

         A6: ( <* [.(a . i), (b . i).]*> . j) = {} by FUNCT_1:def 3;

        j in {1} by FINSEQ_1: 2, A5, FINSEQ_1:def 8;

        then ( <* [.(a . i), (b . i).]*> . 1) = {} by A6, TARSKI:def 1;

        then [.(a . i), (b . i).] is empty by FINSEQ_1:def 8;

        hence contradiction by A1, A3, XXREAL_1: 30;

      end;

      

       A7: s is pointwise_bounded

      proof

        now

          let i be Nat;

          

           A8: (s . i) = ( product <* [.(a . i), (b . i).]*>) by Def1;

          set si = ( product <* [.(a . i), (b . i).]*>);

          reconsider si as Subset of ( Euclid 1) by A8;

          ex r be Real st 0 < r & for x,y be Point of ( Euclid 1) st x in si & y in si holds ( dist (x,y)) <= r

          proof

            set r = ((b . i) - (a . i));

            per cases by A1, XREAL_1: 48;

              suppose r = 0 ;

              

              then

               A9: ( product <* [.(a . i), (b . i).]*>) = ( product <* {(a . i)}*>) by XXREAL_1: 17

              .= { <*(a . i)*>} by Th5;

              now

                take r = 1;

                thus 0 < r;

                hereby

                  let x,y be Point of ( Euclid 1);

                  assume x in si & y in si;

                  then

                   A10: x = <*(a . i)*> & y = <*(a . i)*> by A9, TARSKI:def 1;

                  ( Euclid 1) is Reflexive;

                  hence ( dist (x,y)) <= r by A10, METRIC_1:def 2;

                end;

              end;

              hence ex r be Real st 0 < r & for x,y be Point of ( Euclid 1) st x in si & y in si holds ( dist (x,y)) <= r;

            end;

              suppose

               A11: 0 < r;

              take r;

              thus 0 < r by A11;

              hereby

                let x,y be Point of ( Euclid 1);

                assume that

                 A12: x in si and

                 A13: y in si;

                consider gx be Function such that

                 A14: x = gx and ( dom gx) = ( dom <* [.(a . i), (b . i).]*>) and

                 A15: for j be object st j in ( dom <* [.(a . i), (b . i).]*>) holds (gx . j) in ( <* [.(a . i), (b . i).]*> . j) by A12, CARD_3:def 5;

                consider gy be Function such that

                 A16: y = gy and ( dom gy) = ( dom <* [.(a . i), (b . i).]*>) and

                 A17: for j be object st j in ( dom <* [.(a . i), (b . i).]*>) holds (gy . j) in ( <* [.(a . i), (b . i).]*> . j) by A13, CARD_3:def 5;

                x in ( Euclid 1) & y in ( Euclid 1);

                then x in ( TOP-REAL 1) & y in ( TOP-REAL 1) by EUCLID: 67;

                then

                reconsider rx = x, ry = y as Element of ( REAL 1) by EUCLID: 22;

                ( Euclid 1) = MetrStruct (# ( REAL 1), ( Pitag_dist 1) #) by EUCLID:def 7;

                then

                 A18: ( dist (x,y)) = |.(rx - ry).| by EUCLID:def 6;

                consider ux be Real such that

                 A19: rx = <*ux*> by Th6;

                consider uy be Real such that

                 A20: ry = <*uy*> by Th6;

                rx = (1 |-> ux) & ry = (1 |-> uy) by A19, A20, FINSEQ_2: 59;

                

                then

                 A21: |.(rx - ry).| = (( sqrt 1) * |.(ux - uy).|) by TOPREALC: 11

                .= |.(ux - uy).| by SQUARE_1: 18;

                1 in ( Seg 1) by TARSKI:def 1, FINSEQ_1: 2;

                then 1 in ( dom <* [.(a . i), (b . i).]*>) by FINSEQ_1:def 8;

                then (gx . 1) in ( <* [.(a . i), (b . i).]*> . 1) & (gy . 1) in ( <* [.(a . i), (b . i).]*> . 1) by A15, A17;

                then (gx . 1) in [.(a . i), (b . i).] & (gy . 1) in [.(a . i), (b . i).] by FINSEQ_1:def 8;

                then ux in [.(a . i), (b . i).] & uy in [.(a . i), (b . i).] by A14, A16, A19, A20, FINSEQ_1:def 8;

                hence ( dist (x,y)) <= r by A21, A18, UNIFORM1: 12;

              end;

            end;

          end;

          then si is bounded;

          hence (s . i) is bounded by Def1;

        end;

        hence thesis by COMPL_SP:def 1;

      end;

      s is closed

      proof

        for i be Nat holds (s . i) is closed

        proof

          let i be Nat;

          

           A22: (s . i) = ( product <* [.(a . i), (b . i).]*>) by Def1;

          then

          reconsider si = ( product <* [.(a . i), (b . i).]*>) as Subset of ( Euclid 1);

          

           A23: (si ` ) = ( product <*( ]. -infty , (a . i).[ \/ ].(b . i), +infty .[)*>)

          proof

            (si ` ) = (the carrier of ( TOP-REAL 1) \ si) by EUCLID: 67

            .= (( REAL 1) \ ( product <* [.(a . i), (b . i).]*>)) by EUCLID: 22

            .= ( product <*( REAL \ [.(a . i), (b . i).])*>) by Th18, SRINGS_4: 27;

            hence thesis by XXREAL_1: 385;

          end;

          (si ` ) is open

          proof

            (si ` ) in ( Family_open_set ( Euclid 1))

            proof

              for x be Element of ( Euclid 1) st x in (si ` ) holds ex r be Real st r > 0 & ( Ball (x,r)) c= (si ` )

              proof

                let x be Element of ( Euclid 1);

                assume

                 A24: x in (si ` );

                set A = ]. -infty , (a . i).[, B = ].(b . i), +infty .[, f = <*(A \/ B)*>;

                consider g be Function such that

                 A25: x = g and ( dom g) = ( dom f) and

                 A26: for j be object st j in ( dom f) holds (g . j) in (f . j) by A24, A23, CARD_3:def 5;

                1 in ( Seg 1) by TARSKI:def 1, FINSEQ_1: 2;

                then 1 in ( dom f) by FINSEQ_1:def 8;

                then (g . 1) in (f . 1) by A26;

                then (g . 1) in (A \/ B) by FINSEQ_1:def 8;

                per cases by XBOOLE_0:def 3;

                  suppose

                   A27: (g . 1) in A;

                  then

                  reconsider g1 = (g . 1) as ExtReal;

                  now

                    x is Element of ( TOP-REAL 1) by EUCLID: 67;

                    then x is Element of ( REAL 1) by EUCLID: 22;

                    then x in ( REAL 1);

                    then x in (1 -tuples_on REAL ) by EUCLID:def 1;

                    then g in ( Funcs (( Seg 1), REAL )) by A25, FINSEQ_2: 93;

                    then

                    consider h be Function such that

                     A28: g = h and

                     A29: ( dom h) = ( Seg 1) and

                     A30: ( rng h) c= REAL by FUNCT_2:def 2;

                    1 in ( dom h) by A29, TARSKI:def 1, FINSEQ_1: 2;

                    then (h . 1) in REAL by A30, FUNCT_1: 3;

                    then

                    reconsider g1 as Real by A28;

                    set r = |.(g1 - (a . i)).|;

                    take r;

                    (g1 - (a . i)) <> 0 by A27, XXREAL_1: 233;

                    hence r > 0 ;

                    thus ( Ball (x,r)) c= (si ` )

                    proof

                      let t be object;

                      assume

                       A31: t in ( Ball (x,r));

                      then

                      reconsider t1 = t as Element of ( Euclid 1);

                      t1 in ( Euclid 1) & x in ( Euclid 1);

                      then t1 in ( TOP-REAL 1) & x in ( TOP-REAL 1) by EUCLID: 67;

                      then

                      reconsider rt1 = t1, rx = x as Element of ( REAL 1) by EUCLID: 22;

                      ( Euclid 1) = MetrStruct (# ( REAL 1), ( Pitag_dist 1) #) by EUCLID:def 7;

                      then

                       A32: ( dist (x,t1)) = |.(rx - rt1).| by EUCLID:def 6;

                      now

                        take rt1;

                        thus t = rt1;

                        rt1 in ( REAL 1);

                        then rt1 in (1 -tuples_on REAL ) by EUCLID:def 1;

                        then rt1 in ( Funcs (( Seg 1), REAL )) by FINSEQ_2: 93;

                        then

                        consider h be Function such that

                         A33: rt1 = h and

                         A34: ( dom h) = ( Seg 1) and ( rng h) c= REAL by FUNCT_2:def 2;

                        thus ( dom rt1) = ( dom f) by A33, A34, FINSEQ_1:def 8;

                        hereby

                          let j be object;

                          assume j in ( dom f);

                          then

                           A35: j in {1} by FINSEQ_1: 2, FINSEQ_1:def 8;

                          then

                           A36: j = 1 by TARSKI:def 1;

                          consider rt2 be Real such that

                           A37: rt1 = <*rt2*> by Th6;

                          

                           A38: (rt1 . j) = (rt1 . 1) by A35, TARSKI:def 1

                          .= rt2 by A37, FINSEQ_1:def 8;

                          consider ux be Real such that

                           A39: rx = <*ux*> by Th6;

                          rx = (1 |-> ux) & rt1 = (1 |-> rt2) by A37, A39, FINSEQ_2: 59;

                          

                          then

                           A40: |.(rx - rt1).| = (( sqrt 1) * |.(ux - rt2).|) by TOPREALC: 11

                          .= |.(ux - rt2).| by SQUARE_1: 18;

                          rt2 in (A \/ B)

                          proof

                            

                             A41: |.(ux - rt2).| < |.(g1 - (a . i)).| by A40, A32, A31, METRIC_1: 11;

                            (g1 - (a . i)) < 0 by A27, XXREAL_1: 233, XREAL_1: 49;

                            then |.(g1 - (a . i)).| = ( - (g1 - (a . i))) by ABSVALUE:def 1;

                            then

                             A42: |.(g1 - rt2).| < ((a . i) - g1) by A25, A39, FINSEQ_1:def 8, A41;

                            per cases ;

                              suppose 0 <= (g1 - rt2);

                              then ( 0 + rt2) <= ((g1 - rt2) + rt2) by XREAL_1: 7;

                              then rt2 < (a . i) by A27, XXREAL_1: 233, XXREAL_0: 2;

                              then rt2 in A or rt2 in B by XXREAL_1: 233;

                              hence thesis by XBOOLE_0:def 3;

                            end;

                              suppose (g1 - rt2) < 0 ;

                              then ( - (g1 - rt2)) < ((a . i) - g1) by A42, ABSVALUE:def 1;

                              then ((rt2 - g1) + g1) < (((a . i) - g1) + g1) by XREAL_1: 8;

                              then rt2 in A or rt2 in B by XXREAL_1: 233;

                              hence thesis by XBOOLE_0:def 3;

                            end;

                          end;

                          hence (rt1 . j) in (f . j) by A36, FINSEQ_1:def 8, A38;

                        end;

                      end;

                      hence thesis by A23, CARD_3:def 5;

                    end;

                  end;

                  hence thesis;

                end;

                  suppose

                   A43: (g . 1) in B;

                  then

                  reconsider g1 = (g . 1) as ExtReal;

                  now

                    x is Element of ( TOP-REAL 1) by EUCLID: 67;

                    then x is Element of ( REAL 1) by EUCLID: 22;

                    then x in ( REAL 1);

                    then x in (1 -tuples_on REAL ) by EUCLID:def 1;

                    then g in ( Funcs (( Seg 1), REAL )) by A25, FINSEQ_2: 93;

                    then

                    consider h be Function such that

                     A44: g = h and

                     A45: ( dom h) = ( Seg 1) and

                     A46: ( rng h) c= REAL by FUNCT_2:def 2;

                    1 in ( Seg 1) by TARSKI:def 1, FINSEQ_1: 2;

                    then (h . 1) in REAL by A45, A46, FUNCT_1: 3;

                    then

                    reconsider g1 as Real by A44;

                    set r = |.(g1 - (b . i)).|;

                    take r;

                    (g1 - (b . i)) <> 0 by A43, XXREAL_1: 235;

                    hence r > 0 ;

                    thus ( Ball (x,r)) c= (si ` )

                    proof

                      let t be object;

                      assume

                       A46bis: t in ( Ball (x,r));

                      then

                      reconsider t1 = t as Element of ( Euclid 1);

                      t1 in ( Euclid 1) & x in ( Euclid 1);

                      then t1 in ( TOP-REAL 1) & x in ( TOP-REAL 1) by EUCLID: 67;

                      then

                      reconsider rt1 = t1, rx = x as Element of ( REAL 1) by EUCLID: 22;

                      ( Euclid 1) = MetrStruct (# ( REAL 1), ( Pitag_dist 1) #) by EUCLID:def 7;

                      then

                       A46ter: ( dist (x,t1)) = |.(rx - rt1).| by EUCLID:def 6;

                      now

                        take rt1;

                        thus t = rt1;

                        rt1 in ( REAL 1);

                        then rt1 in (1 -tuples_on REAL ) by EUCLID:def 1;

                        then rt1 in ( Funcs (( Seg 1), REAL )) by FINSEQ_2: 93;

                        then

                        consider h be Function such that

                         A47: rt1 = h and

                         A48: ( dom h) = ( Seg 1) and ( rng h) c= REAL by FUNCT_2:def 2;

                        thus ( dom rt1) = ( dom f) by A47, A48, FINSEQ_1:def 8;

                        hereby

                          let j be object;

                          assume j in ( dom f);

                          then

                           A49: j in {1} by FINSEQ_1: 2, FINSEQ_1:def 8;

                          then

                           A50: j = 1 by TARSKI:def 1;

                          consider rt2 be Real such that

                           A51: rt1 = <*rt2*> by Th6;

                          

                           A52: (rt1 . j) = (rt1 . 1) by A49, TARSKI:def 1

                          .= rt2 by A51, FINSEQ_1:def 8;

                          consider ux be Real such that

                           A53: rx = <*ux*> by Th6;

                          rx = (1 |-> ux) & rt1 = (1 |-> rt2) by A51, A53, FINSEQ_2: 59;

                          

                          then

                           A54: |.(rx - rt1).| = (( sqrt 1) * |.(ux - rt2).|) by TOPREALC: 11

                          .= |.(ux - rt2).| by SQUARE_1: 18;

                          rt2 in (A \/ B)

                          proof

                            ux = g1 by A25, A53, FINSEQ_1:def 8;

                            then

                             A55: |.(g1 - rt2).| < |.(g1 - (b . i)).| by A54, A46bis, A46ter, METRIC_1: 11;

                             0 < (g1 - (b . i)) by A43, XXREAL_1: 235, XREAL_1: 50;

                            then

                             A56: |.(g1 - rt2).| < (g1 - (b . i)) by A55, ABSVALUE:def 1;

                            (g1 - rt2) < (g1 - (b . i)) by A56, ABSVALUE:def 1;

                            then ((g1 - rt2) - g1) < ((g1 - (b . i)) - g1) by XREAL_1: 14;

                            then ( - rt2) < ( - (b . i));

                            then rt2 in A or rt2 in B by XREAL_1: 24, XXREAL_1: 235;

                            hence thesis by XBOOLE_0:def 3;

                          end;

                          hence (rt1 . j) in (f . j) by A52, A50, FINSEQ_1:def 8;

                        end;

                      end;

                      hence thesis by A23, CARD_3:def 5;

                    end;

                  end;

                  hence thesis;

                end;

              end;

              hence thesis by PCOMPS_1:def 4;

            end;

            hence thesis by COMPL_SP:def 3;

          end;

          hence thesis by A22, COMPL_SP:def 4;

        end;

        hence thesis by COMPL_SP:def 8;

      end;

      hence thesis by A2, A7;

    end;

    theorem :: COUSIN:26

    

     Th23: for a,b be Real_Sequence st for i be Nat holds (a . i) <= (b . i) & (a . i) <= (a . (i + 1)) & (b . (i + 1)) <= (b . i) holds ( IntervalSequence (a,b)) is non-ascending

    proof

      let a,b be Real_Sequence;

      assume

       A1: for i be Nat holds (a . i) <= (b . i) & (a . i) <= (a . (i + 1)) & (b . (i + 1)) <= (b . i);

      now

        let n,m be Nat;

        assume

         A2: n <= m;

        ( product <* [.(a . m), (b . m).]*>) c= ( product <* [.(a . n), (b . n).]*>)

        proof

          let x be object;

          assume x in ( product <* [.(a . m), (b . m).]*>);

          then

          consider f be Function such that

           A3: x = f and

           A4: ( dom f) = ( dom <* [.(a . m), (b . m).]*>) and

           A5: for i be object st i in ( dom <* [.(a . m), (b . m).]*>) holds (f . i) in ( <* [.(a . m), (b . m).]*> . i) by CARD_3:def 5;

          

           A6: ( dom <* [.(a . m), (b . m).]*>) = ( Seg 1) by FINSEQ_1:def 8;

          now

            thus x = f by A3;

            thus ( dom f) = ( dom <* [.(a . n), (b . n).]*>) by A6, A4, FINSEQ_1:def 8;

            hereby

              let i be object;

              assume

               A7: i in ( dom <* [.(a . n), (b . n).]*>);

              then

               A8: i in ( dom <* [.(a . m), (b . m).]*>) by A6, FINSEQ_1:def 8;

              i in ( Seg 1) by A7, FINSEQ_1:def 8;

              then

               A9: i = 1 by TARSKI:def 1, FINSEQ_1: 2;

              then

               A10: ( <* [.(a . m), (b . m).]*> . i) = [.(a . m), (b . m).] by FINSEQ_1:def 8;

              

               A11: ( <* [.(a . n), (b . n).]*> . i) = [.(a . n), (b . n).] by A9, FINSEQ_1:def 8;

              

               A12: a is non-decreasing by A1;

              ( dom a) = NAT by SEQ_1: 1;

              then n in ( dom a) & m in ( dom a) by ORDINAL1:def 12;

              then

               A13: (a . n) <= (a . m) by A12, A2;

              

               A14: b is non-increasing by A1;

              ( dom b) = NAT by SEQ_1: 1;

              then n in ( dom b) & m in ( dom b) by ORDINAL1:def 12;

              then (b . m) <= (b . n) by A14, A2;

              then [.(a . m), (b . m).] c= [.(a . n), (b . n).] by A13, XXREAL_1: 34;

              hence (f . i) in ( <* [.(a . n), (b . n).]*> . i) by A8, A5, A10, A11;

            end;

          end;

          hence thesis by CARD_3:def 5;

        end;

        then (( IntervalSequence (a,b)) . m) c= ( product <* [.(a . n), (b . n).]*>) by Def1;

        hence (( IntervalSequence (a,b)) . m) c= (( IntervalSequence (a,b)) . n) by Def1;

      end;

      hence thesis by PROB_1:def 4;

    end;

    theorem :: COUSIN:27

    

     Th24: for a,b,x be Real st a <= x <= b holds <*x*> in ( product <* [.a, b.]*>)

    proof

      let a,b,x be Real;

      assume

       A1: a <= x <= b;

      reconsider P = <*x*> as Point of ( Euclid 1) by Th7;

      set f = <* [.a, b.]*>;

      

       A2: ( dom f) = ( Seg 1) by FINSEQ_1:def 8;

      ex g be Function st g = P & ( dom g) = ( dom <* [.a, b.]*>) & for y be object st y in ( dom <* [.a, b.]*>) holds (g . y) in ( <* [.a, b.]*> . y)

      proof

        reconsider g = P as Function;

        now

          take g;

          thus g = P;

          thus ( dom g) = ( dom f) by A2, FINSEQ_1:def 8;

          hereby

            let y be object;

            assume y in ( dom f);

            then y in {1} by FINSEQ_1:def 8, FINSEQ_1: 2;

            then

             A3: y = 1 by TARSKI:def 1;

            (g . 1) = x & (f . 1) = [.a, b.] by FINSEQ_1:def 8;

            hence (g . y) in (f . y) by A3, A1, XXREAL_1: 1;

          end;

        end;

        hence thesis;

      end;

      hence thesis by CARD_3:def 5;

    end;

    theorem :: COUSIN:28

    

     Th25: for a,b be Real, S be Subset of ( Euclid 1) st a <= b & S = ( product <* [.a, b.]*>) holds ( diameter S) = (b - a)

    proof

      let a,b be Real, S be Subset of ( Euclid 1);

      assume that

       A1: a <= b and

       A2: S = ( product <* [.a, b.]*>);

      set f = <* [.a, b.]*>;

      

       A3: S is bounded by A1, A2, Th21;

      

       A4: S is non empty by A1, A2, Th24;

      ((for x,y be Point of ( Euclid 1) st x in S & y in S holds ( dist (x,y)) <= (b - a)) & (for s be Real st (for x,y be Point of ( Euclid 1) st x in S & y in S holds ( dist (x,y)) <= s) holds (b - a) <= s))

      proof

        thus for x,y be Point of ( Euclid 1) st x in S & y in S holds ( dist (x,y)) <= (b - a) by A1, A2, Th20;

        thus for s be Real st (for x,y be Point of ( Euclid 1) st x in S & y in S holds ( dist (x,y)) <= s) holds (b - a) <= s

        proof

          let s be Real;

          assume

           A5: for x,y be Point of ( Euclid 1) st x in S & y in S holds ( dist (x,y)) <= s;

          assume

           A6: s < (b - a);

          

           A7: <*a*> in S & <*b*> in S by A2, A1, Th24;

          reconsider sa = <*a*>, sb = <*b*> as Point of ( Euclid 1) by Th7;

          

           A8: ( dist (sa,sb)) <= s by A5, A7;

          (a - a) <= (b - a) by A1, XREAL_1: 9;

          then |.(b - a).| = (b - a) by ABSVALUE:def 1;

          hence contradiction by A6, A8, Th19;

        end;

      end;

      hence thesis by A3, A4, TBSP_1:def 8;

    end;

    theorem :: COUSIN:29

    

     Th26: for a,b be Real_Sequence st (for i be Nat holds (a . i) <= (b . i)) & a is non-decreasing & b is non-increasing holds a is convergent & b is convergent

    proof

      let a,b be Real_Sequence;

      assume that

       A1: for i be Nat holds (a . i) <= (b . i) and

       A2: a is non-decreasing and

       A3: b is non-increasing;

      now

        take r = ((b . 0 ) + 1);

        hereby

          let n be Nat;

          reconsider n0 = n as ExtReal;

           0 in NAT ;

          then

           A4: 0 in ( dom b) by SEQ_1: 1;

          n in NAT by ORDINAL1:def 12;

          then n0 in ( dom b) by SEQ_1: 1;

          then

           A5: (b . n0) <= (b . 0 ) by A4, A3;

          (a . n) <= (b . n) by A1;

          then (a . n) <= (b . 0 ) by A5, XXREAL_0: 2;

          then ((a . n) + 0 ) < ((b . 0 ) + 1) by XREAL_1: 8;

          hence (a . n) < r;

        end;

      end;

      then

       A6: a is bounded_above by SEQ_2:def 3;

      now

        take r = ((a . 0 ) - 1);

        hereby

          let n be Nat;

          reconsider n0 = n as ExtReal;

           0 in NAT ;

          then

           A7: 0 in ( dom a) by SEQ_1: 1;

          n in NAT by ORDINAL1:def 12;

          then n0 in ( dom a) by SEQ_1: 1;

          then

           A8: (a . 0 ) <= (a . n0) by A7, A2;

          (a . n) <= (b . n) by A1;

          then (a . 0 ) <= (b . n) by A8, XXREAL_0: 2;

          then ((a . 0 ) - 1) < ((b . n) - 0 ) by XREAL_1: 15;

          hence r < (b . n);

        end;

      end;

      then b is bounded_below by SEQ_2:def 4;

      hence thesis by A2, A3, A6;

    end;

    theorem :: COUSIN:30

    

     Th27: for a,b be Real_Sequence st (a . 0 ) <= (b . 0 ) & for i be Nat holds (((a . (i + 1)) = (a . i) & (b . (i + 1)) = (((a . i) + (b . i)) / 2)) or ((a . (i + 1)) = (((a . i) + (b . i)) / 2) & (b . (i + 1)) = (b . i))) holds for i be Nat holds (a . i) <= (b . i)

    proof

      let a,b be Real_Sequence;

      assume that

       A1: (a . 0 ) <= (b . 0 ) and

       A2: for i be Nat holds (((a . (i + 1)) = (a . i) & (b . (i + 1)) = (((a . i) + (b . i)) / 2)) or ((a . (i + 1)) = (((a . i) + (b . i)) / 2) & (b . (i + 1)) = (b . i)));

      defpred P[ object] means ex i be Nat st $1 = i & (a . i) <= (b . i);

      

       A3: P[ 0 ] by A1;

      

       A4: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume P[k];

        then

        consider i be Nat such that k = i and

         A5: (a . k) <= (b . k);

        (((a . (k + 1)) = (a . k) & (b . (k + 1)) = (((a . k) + (b . k)) / 2)) or ((a . (k + 1)) = (((a . k) + (b . k)) / 2) & (b . (k + 1)) = (b . k))) by A2;

        hence thesis by A5, Th8;

      end;

      

       A6: for k be Nat holds P[k] from NAT_1:sch 2( A3, A4);

      let k be Nat;

      ex i be Nat st i = k & (a . i) <= (b . i) by A6;

      hence (a . k) <= (b . k);

    end;

    theorem :: COUSIN:31

    

     Th28: for a,b be Real_Sequence, S be SetSequence of ( Euclid 1) st (a . 0 ) <= (b . 0 ) & S = ( IntervalSequence (a,b)) & (for i be Nat holds (((a . (i + 1)) = (a . i) & (b . (i + 1)) = (((a . i) + (b . i)) / 2)) or ((a . (i + 1)) = (((a . i) + (b . i)) / 2) & (b . (i + 1)) = (b . i)))) holds for i be Nat holds (a . i) <= (b . i) & (a . i) <= (a . (i + 1)) & (b . (i + 1)) <= (b . i) & (( diameter S) . i) = ((b . i) - (a . i))

    proof

      let a,b be Real_Sequence, S be SetSequence of ( Euclid 1);

      assume that

       A1: (a . 0 ) <= (b . 0 ) and

       A2: S = ( IntervalSequence (a,b)) and

       A3: for i be Nat holds ((a . (i + 1)) = (a . i) & (b . (i + 1)) = (((a . i) + (b . i)) / 2)) or ((a . (i + 1)) = (((a . i) + (b . i)) / 2) & (b . (i + 1)) = (b . i));

      

       A4: for i be Nat holds (a . i) <= (b . i) & (a . i) <= (a . (i + 1)) & (b . (i + 1)) <= (b . i)

      proof

        let i be Nat;

        thus

         A6: (a . i) <= (b . i) by Th27, A1, A3;

        thus (a . i) <= (a . (i + 1))

        proof

          (a . (i + 1)) = (a . i) or (a . (i + 1)) = (((a . i) + (b . i)) / 2) by A3;

          hence thesis by A6, Th8;

        end;

        thus (b . (i + 1)) <= (b . i)

        proof

          (b . (i + 1)) = (b . i) or (b . (i + 1)) = (((a . i) + (b . i)) / 2) by A3;

          hence thesis by A6, Th8;

        end;

      end;

      now

        let i be Nat;

        

         A7: ( IntervalSequence (a,b)) is SetSequence of ( Euclid 1) by Th17;

        reconsider IntervalSequence1 = (( IntervalSequence (a,b)) . i) as Subset of ( Euclid 1) by ORDINAL1:def 12, A7, FUNCT_2: 5;

        (S . i) = ( product <* [.(a . i), (b . i).]*>) by A2, Def1;

        then

        reconsider IntervalSequence2 = ( product <* [.(a . i), (b . i).]*>) as Subset of ( Euclid 1);

        ( diameter (S . i)) = ( diameter IntervalSequence2) by A2, Def1

        .= ((b . i) - (a . i)) by A4, Th25;

        hence (( diameter S) . i) = ((b . i) - (a . i)) by COMPL_SP:def 2;

      end;

      hence thesis by A4;

    end;

    theorem :: COUSIN:32

    

     Th29: for a,b be Real_Sequence, S be SetSequence of ( Euclid 1) st (a . 0 ) = (b . 0 ) & S = ( IntervalSequence (a,b)) & (for i be Nat holds (((a . (i + 1)) = (a . i) & (b . (i + 1)) = (((a . i) + (b . i)) / 2)) or ((a . (i + 1)) = (((a . i) + (b . i)) / 2) & (b . (i + 1)) = (b . i)))) holds for i be Nat holds (a . i) = (a . 0 ) & (b . i) = (b . 0 ) & (( diameter S) . i) = 0

    proof

      let a,b be Real_Sequence, S be SetSequence of ( Euclid 1);

      assume that

       A1: (a . 0 ) = (b . 0 ) and

       A2: S = ( IntervalSequence (a,b)) and

       A3: for i be Nat holds ((a . (i + 1)) = (a . i) & (b . (i + 1)) = (((a . i) + (b . i)) / 2)) or ((a . (i + 1)) = (((a . i) + (b . i)) / 2) & (b . (i + 1)) = (b . i));

      defpred P[ Nat] means (a . $1) = (a . 0 ) & (b . $1) = (b . 0 );

      

       A4: P[ 0 ];

      

       A5: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         A6: P[k];

        ((a . (k + 1)) = (a . k) & (b . (k + 1)) = (((a . k) + (b . k)) / 2)) or ((a . (k + 1)) = (((a . k) + (b . k)) / 2) & (b . (k + 1)) = (b . k)) by A3;

        hence thesis by A1, A6;

      end;

      

       A7: for k be Nat holds P[k] from NAT_1:sch 2( A4, A5);

      let i be Nat;

      thus

       A8: (a . i) = (a . 0 ) by A7;

      thus

       A9: (b . i) = (b . 0 ) by A7;

      (( diameter S) . i) = ((b . i) - (a . i)) by A1, A2, A3, Th28;

      hence (( diameter S) . i) = 0 by A1, A8, A9;

    end;

    theorem :: COUSIN:33

    

     Th30: for a,b be Real_Sequence st (for i be Nat holds ((a . (i + 1)) = (a . i) & (b . (i + 1)) = (((a . i) + (b . i)) / 2)) or ((a . (i + 1)) = (((a . i) + (b . i)) / 2) & (b . (i + 1)) = (b . i))) holds (for i be Nat, r be Real st r = (2 |^ i) & r <> 0 holds ((b . i) - (a . i)) <= (((b . 0 ) - (a . 0 )) / r))

    proof

      let a,b be Real_Sequence;

      assume that

       A1: for i be Nat holds ((a . (i + 1)) = (a . i) & (b . (i + 1)) = (((a . i) + (b . i)) / 2)) or ((a . (i + 1)) = (((a . i) + (b . i)) / 2) & (b . (i + 1)) = (b . i));

      defpred P[ object] means ex i be Nat, r be Real st $1 = i & r = (2 |^ i) & r <> 0 & ((b . i) - (a . i)) <= (((b . 0 ) - (a . 0 )) / r);

      

       A2: P[ 0 ]

      proof

        reconsider i0 = 0 as Nat;

        reconsider r0 = (2 |^ 0 ) as Real;

        take i0;

        take r0;

        (2 |^ 0 ) = 1 by NEWTON: 4;

        hence thesis;

      end;

      

       A3: for k be Nat holds P[k] implies P[(k + 1)]

      proof

        let k be Nat;

        assume P[k];

        then

        consider i1 be Nat, r1 be Real such that

         A4: k = i1 and

         A5: r1 = (2 |^ i1) and r1 <> 0 and

         A6: ((b . i1) - (a . i1)) <= (((b . 0 ) - (a . 0 )) / r1);

        reconsider i0 = (k + 1) as Nat;

        reconsider r0 = (2 |^ (k + 1)) as Real;

        

         A7: r0 <> 0 by NEWTON: 87;

        ((b . i0) - (a . i0)) <= (((b . 0 ) - (a . 0 )) / r0)

        proof

          

           A8: ((a . (k + 1)) = (a . k) & (b . (k + 1)) = (((a . k) + (b . k)) / 2)) or ((a . (k + 1)) = (((a . k) + (b . k)) / 2) & (b . (k + 1)) = (b . k)) by A1;

          

           A9: (((b . i1) - (a . i1)) / 2) <= ((((b . 0 ) - (a . 0 )) / r1) / 2) by A6, XREAL_1: 72;

          (r1 * 2) = r0 by A4, A5, NEWTON: 6;

          hence thesis by A8, A4, XCMPLX_1: 78, A9;

        end;

        hence thesis by A7;

      end;

      

       A10: for k be Nat holds P[k] from NAT_1:sch 2( A2, A3);

      let i be Nat, r be Real;

      assume that

       A11: r = (2 |^ i) and r <> 0 ;

      consider i0 be Nat, r0 be Real such that

       A12: i = i0 and

       A13: r0 = (2 |^ i0) & r0 <> 0 & ((b . i0) - (a . i0)) <= (((b . 0 ) - (a . 0 )) / r0) by A10;

      thus ((b . i) - (a . i)) <= (((b . 0 ) - (a . 0 )) / r) by A11, A12, A13;

    end;

    theorem :: COUSIN:34

    

     Th31: for a,b be Real_Sequence, S be SetSequence of ( Euclid 1) st (a . 0 ) <= (b . 0 ) & S = ( IntervalSequence (a,b)) & (for i be Nat holds (((a . (i + 1)) = (a . i) & (b . (i + 1)) = (((a . i) + (b . i)) / 2)) or ((a . (i + 1)) = (((a . i) + (b . i)) / 2) & (b . (i + 1)) = (b . i)))) holds ( diameter S) is convergent & ( lim ( diameter S)) = 0

    proof

      let a,b be Real_Sequence, S be SetSequence of ( Euclid 1);

      assume that

       A1: (a . 0 ) <= (b . 0 ) and

       A2: S = ( IntervalSequence (a,b)) and

       A3: (for i be Nat holds (((a . (i + 1)) = (a . i) & (b . (i + 1)) = (((a . i) + (b . i)) / 2)) or ((a . (i + 1)) = (((a . i) + (b . i)) / 2) & (b . (i + 1)) = (b . i))));

      per cases by A1, XXREAL_0: 1;

        suppose

         A4: (a . 0 ) = (b . 0 );

        for x,y be object st x in ( dom ( diameter S)) & y in ( dom ( diameter S)) holds (( diameter S) . x) = (( diameter S) . y)

        proof

          let x,y be object;

          assume that

           A5: x in ( dom ( diameter S)) and

           A6: y in ( dom ( diameter S));

          (( diameter S) . x) = 0 & (( diameter S) . y) = 0 by A5, A6, A4, A2, A3, Th29;

          hence thesis;

        end;

        then

         A7: ( diameter S) is constant;

        hence ( diameter S) is convergent;

        ( lim ( diameter S)) = (( diameter S) . 0 ) by A7, SEQ_4: 26;

        hence ( lim ( diameter S)) = 0 by A4, A2, A3, Th29;

      end;

        suppose (a . 0 ) < (b . 0 );

        then

         A8: ((a . 0 ) - (a . 0 )) < ((b . 0 ) - (a . 0 )) by XREAL_1: 14;

        

         A9: ( diameter S) = (b + ( - a))

        proof

          now

            let i be Nat;

            (( - a) . i) = ( - (a . i)) by SEQ_1: 10;

            then ((b . i) - (a . i)) = ((b . i) + (( - a) . i));

            hence (( diameter S) . i) = ((b . i) + (( - a) . i)) by A1, A2, A3, Th28;

          end;

          hence thesis by SEQ_1: 7;

        end;

        set S2 = ( diameter S);

        

         A10: for i be Nat holds (a . i) <= (b . i) by A1, A3, Th27;

        

         A11: a is non-decreasing by A1, A2, A3, Th28;

        b is non-increasing by A1, A2, A3, Th28;

        then

         A12: a is convergent & b is convergent by A10, A11, Th26;

        ( lim ( diameter S)) = 0

        proof

          for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.((S2 . m) - 0 ).| < p

          proof

            let p be Real;

            assume

             A13: 0 < p;

             A14:

            now

              ( 0 + 1) < ((((b . 0 ) - (a . 0 )) / p) + 1) by A13, A8, XREAL_1: 8;

              then

               A15: 0 <= ( log (2,((((b . 0 ) - (a . 0 )) / p) + 1))) by Th2;

              reconsider i0 = [/( log (2,((((b . 0 ) - (a . 0 )) / p) + 1)))\] as Integer;

              

               A16: ( log (2,((((b . 0 ) - (a . 0 )) / p) + 1))) <= i0 by INT_1:def 7;

              then

               A17: i0 in NAT by A15, INT_1: 3;

              

               A18: (( log (2,((((b . 0 ) - (a . 0 )) / p) + 1))) + 0 ) < (i0 + 1) by A16, XREAL_1: 8;

              reconsider n0 = (i0 + 1) as Nat by A17;

              take n0;

              let m be Nat;

              assume

               A19: n0 <= m;

              

               A20: 0 < (2 to_power n0) by POWER: 34;

              (2 to_power ( log (2,((((b . 0 ) - (a . 0 )) / p) + 1)))) < (2 to_power n0) by A18, POWER: 39;

              then

               A21: ((((b . 0 ) - (a . 0 )) / p) + 1) < (2 to_power n0) by A13, A8, POWER:def 3;

              (((b . 0 ) - (a . 0 )) / p) < ((((b . 0 ) - (a . 0 )) / p) + 1) by XREAL_1: 29;

              then (((b . 0 ) - (a . 0 )) / p) < (2 to_power n0) by A21, XXREAL_0: 2;

              then ((((b . 0 ) - (a . 0 )) / p) * p) < ((2 to_power n0) * p) by A13, XREAL_1: 68;

              then ((b . 0 ) - (a . 0 )) < (p * (2 to_power n0)) by A13, XCMPLX_1: 87;

              then (((b . 0 ) - (a . 0 )) / (2 to_power n0)) < ((p * (2 to_power n0)) / (2 to_power n0)) by A20, XREAL_1: 74;

              then

               A22: (((b . 0 ) - (a . 0 )) / (2 to_power n0)) < p by A20, XCMPLX_1: 89;

              

               A23: (2 to_power n0) <= (2 to_power m) by A19, NAT_6: 1;

               0 < (2 to_power n0) by POWER: 34;

              then (((b . 0 ) - (a . 0 )) / (2 to_power m)) <= (((b . 0 ) - (a . 0 )) / (2 to_power n0)) by A23, A8, XREAL_1: 118;

              hence (((b . 0 ) - (a . 0 )) / (2 to_power m)) < p by A22, XXREAL_0: 2;

            end;

            now

              consider n0 be Nat such that

               A24: for m be Nat st n0 <= m holds (((b . 0 ) - (a . 0 )) / (2 to_power m)) < p by A14;

              take n0;

              hereby

                let m be Nat;

                assume

                 A25: n0 <= m;

                (a . m) <= (b . m) by A1, A2, A3, Th28;

                then

                 A26: ((a . m) - (a . m)) <= ((b . m) - (a . m)) by XREAL_1: 9;

                ((b - a) . m) = ((b + ( - a)) . m) by SEQ_1: 11

                .= ((b . m) + (( - a) . m)) by SEQ_1: 7

                .= ((b . m) + ( - (a . m))) by SEQ_1: 10

                .= ((b . m) - (a . m));

                

                then

                 A27: |.((S2 . m) - 0 ).| = |.((b . m) - (a . m)).| by A9, SEQ_1: 11

                .= ((b . m) - (a . m)) by A26, ABSVALUE:def 1;

                reconsider m0 = m as Element of NAT by ORDINAL1:def 12;

                (2 |^ m0) is Element of NAT ;

                then

                reconsider r = (2 |^ m) as Real;

                r <> 0 by NEWTON: 83;

                then

                 A28: |.((S2 . m) - 0 ).| <= (((b . 0 ) - (a . 0 )) / r) by A27, Th30, A3;

                (((b . 0 ) - (a . 0 )) / (2 to_power m)) < p by A24, A25;

                hence |.((S2 . m) - 0 ).| < p by A28, XXREAL_0: 2;

              end;

            end;

            hence thesis;

          end;

          hence thesis by A12, A9, SEQ_2:def 7;

        end;

        hence thesis by A12, A9;

      end;

    end;

    theorem :: COUSIN:35

    

     Th32: for a,b be Real_Sequence st (a . 0 ) <= (b . 0 ) & (for i be Nat holds (((a . (i + 1)) = (a . i) & (b . (i + 1)) = (((a . i) + (b . i)) / 2)) or ((a . (i + 1)) = (((a . i) + (b . i)) / 2) & (b . (i + 1)) = (b . i)))) holds ( meet ( IntervalSequence (a,b))) is non empty

    proof

      let a,b be Real_Sequence;

      assume that

       A1: (a . 0 ) <= (b . 0 ) and

       A2: for i be Nat holds (((a . (i + 1)) = (a . i) & (b . (i + 1)) = (((a . i) + (b . i)) / 2)) or ((a . (i + 1)) = (((a . i) + (b . i)) / 2) & (b . (i + 1)) = (b . i)));

      ( IntervalSequence (a,b)) is SetSequence of ( Euclid 1) by Th17;

      then

       A3: for i be Nat holds (a . i) <= (b . i) & (a . i) <= (a . (i + 1)) & (b . (i + 1)) <= (b . i) by A1, A2, Th28;

      reconsider S = ( IntervalSequence (a,b)) as non-empty pointwise_bounded closed SetSequence of ( Euclid 1) by A3, Th22;

      

       A4: S is non-ascending by A3, Th23;

      ( lim ( diameter S)) = 0 by A1, A2, Th31;

      then ( meet S) is non empty by A4, COMPL_SP: 10;

      hence thesis;

    end;

    theorem :: COUSIN:36

    for r be Real, a,b be Real_Sequence st 0 < r & (a . 0 ) <= (b . 0 ) & (for i be Nat holds (((a . (i + 1)) = (a . i) & (b . (i + 1)) = (((a . i) + (b . i)) / 2)) or ((a . (i + 1)) = (((a . i) + (b . i)) / 2) & (b . (i + 1)) = (b . i)))) holds ex c be Real st (for j be Nat holds (a . j) <= c <= (b . j)) & ex k be Nat st (c - r) < (a . k) & (b . k) < (c + r)

    proof

      let r be Real, a,b be Real_Sequence;

      assume that

       A1: 0 < r and

       A2: (a . 0 ) <= (b . 0 ) and

       A3: for i be Nat holds (((a . (i + 1)) = (a . i) & (b . (i + 1)) = (((a . i) + (b . i)) / 2)) or ((a . (i + 1)) = (((a . i) + (b . i)) / 2) & (b . (i + 1)) = (b . i)));

      ( meet ( IntervalSequence (a,b))) is non empty by A2, A3, Th32;

      then

      consider y be object such that

       A4: y in ( meet ( IntervalSequence (a,b)));

      

       A5: y in ( meet ( rng ( IntervalSequence (a,b)))) by A4, FUNCT_6:def 4;

      

       A6: ( dom ( IntervalSequence (a,b))) = NAT by FUNCT_2:def 1;

      set f = ( IntervalSequence (a,b));

      (( IntervalSequence (a,b)) . 0 ) in ( rng ( IntervalSequence (a,b))) by A6, FUNCT_1: 3;

      then y in (( IntervalSequence (a,b)) . 0 ) by A5, SETFAM_1:def 1;

      then

       A8: y in ( product <* [.(a . 0 ), (b . 0 ).]*>) by Def1;

      consider g be Function such that

       A10: y = g and ( dom g) = ( dom <* [.(a . 0 ), (b . 0 ).]*>) and for t be object st t in ( dom <* [.(a . 0 ), (b . 0 ).]*>) holds (g . t) in ( <* [.(a . 0 ), (b . 0 ).]*> . t) by A8, CARD_3:def 5;

      y is Element of ( TOP-REAL 1) by EUCLID: 22, A4;

      then

      consider c be Real such that

       A11: y = <*c*> by JORDAN2B: 20;

      take c;

       A12:

      now

        let i be Nat;

        (( IntervalSequence (a,b)) . i) in ( rng ( IntervalSequence (a,b))) by A6, ORDINAL1:def 12, FUNCT_1: 3;

        then y in (( IntervalSequence (a,b)) . i) by A5, SETFAM_1:def 1;

        then y in ( product <* [.(a . i), (b . i).]*>) by Def1;

        then

        consider h be Function such that

         A13: y = h and ( dom h) = ( dom <* [.(a . i), (b . i).]*>) and

         A14: for t be object st t in ( dom <* [.(a . i), (b . i).]*>) holds (h . t) in ( <* [.(a . i), (b . i).]*> . t) by CARD_3:def 5;

        

         A15: ( dom <* [.(a . i), (b . i).]*>) = ( Seg 1) by FINSEQ_1:def 8;

        1 in ( Seg 1) by TARSKI:def 1, FINSEQ_1: 2;

        then (h . 1) in ( <* [.(a . i), (b . i).]*> . 1) by A14, A15;

        then (g . 1) in [.(a . i), (b . i).] by A10, A13, FINSEQ_1:def 8;

        then c in [.(a . i), (b . i).] by A10, A11, FINSEQ_1:def 8;

        hence (a . i) <= c <= (b . i) by XXREAL_1: 1;

      end;

      hence for j be Nat holds (a . j) <= c <= (b . j);

      thus ex k be Nat st (c - r) < (a . k) & (b . k) < (c + r)

      proof

        

         A16: ( IntervalSequence (a,b)) is SetSequence of ( Euclid 1) by Th17;

        then

         A17: for i be Nat holds (a . i) <= (b . i) & (a . i) <= (a . (i + 1)) & (b . (i + 1)) <= (b . i) by A2, A3, Th28;

        reconsider S = ( IntervalSequence (a,b)) as non-empty pointwise_bounded closed SetSequence of ( Euclid 1) by A17, Th22;

        

         A18: ( diameter S) is convergent & ( lim ( diameter S)) = 0 by A2, A3, Th31;

        consider m0 be Nat such that

         A19: for l be Nat st m0 <= l holds |.((( diameter S) . l) - 0 ).| < r by A1, A18, SEQ_2:def 7;

        (a . m0) <= (b . m0) by A16, A2, A3, Th28;

        then ((a . m0) - (a . m0)) <= ((b . m0) - (a . m0)) by XREAL_1: 9;

        then |.((b . m0) - (a . m0)).| = ((b . m0) - (a . m0)) by ABSVALUE:def 1;

        then |.((( diameter S) . m0) - 0 ).| = ((b . m0) - (a . m0)) by A2, A3, Th28;

        then

         A20: ((b . m0) - (a . m0)) < r by A19;

        (c - (a . m0)) <= ((b . m0) - (a . m0)) by A12, XREAL_1: 9;

        then

         A21: (c - (a . m0)) < r by A20, XXREAL_0: 2;

        take m0;

        ((c - (a . m0)) + (a . m0)) < (r + (a . m0)) by A21, XREAL_1: 8;

        then (c - r) < (((a . m0) + r) - r) by XREAL_1: 9;

        hence (c - r) < (a . m0);

        ((b . m0) - c) <= ((b . m0) - (a . m0)) by A12, XREAL_1: 10;

        then ((b . m0) - c) < r by A20, XXREAL_0: 2;

        then (((b . m0) - c) + c) < (r + c) by XREAL_1: 8;

        hence (b . m0) < (c + r);

      end;

    end;

    begin

    theorem :: COUSIN:37

    

     Th33: for I be non empty closed_interval Subset of REAL holds ex a,b be Real st a <= b & I = [.a, b.]

    proof

      let I be non empty closed_interval Subset of REAL ;

      ex a,b be Real st I = [.a, b.] by MEASURE5:def 3;

      hence thesis by XXREAL_1: 29;

    end;

    theorem :: COUSIN:38

    for I1,I2 be non empty closed_interval Subset of REAL st ( upper_bound I1) = ( lower_bound I2) holds ex a,b,c be Real st a <= c <= b & I1 = [.a, c.] & I2 = [.c, b.]

    proof

      let I1,I2 be non empty closed_interval Subset of REAL ;

      assume

       A1: ( upper_bound I1) = ( lower_bound I2);

      consider a1,b1 be Real such that

       A2: a1 <= b1 and

       A3: I1 = [.a1, b1.] by Th33;

      consider a2,b2 be Real such that

       A4: a2 <= b2 and

       A5: I2 = [.a2, b2.] by Th33;

      

       A6: ( upper_bound I1) = b1 by A2, A3, JORDAN5A: 19;

      ( lower_bound I2) = a2 by A4, A5, JORDAN5A: 19;

      hence thesis by A1, A2, A4, A3, A5, A6;

    end;

    definition

      let A be non empty closed_interval Subset of REAL , D be Division of A;

      :: COUSIN:def2

      func set_of_tagged_Division (D) -> Subset of ( REAL * ) means

      : Def2: for x be object holds x in it iff ex s be non empty non-decreasing FinSequence of REAL st x = s & ( dom s) = ( dom D) & for i be Nat st i in ( dom s) holds (s . i) in ( divset (D,i));

      existence

      proof

        defpred P[ object] means ex s be non empty non-decreasing FinSequence of REAL st $1 = s & ( dom s) = ( dom D) & for i be Nat st i in ( dom s) holds (s . i) in ( divset (D,i));

        consider S be set such that

         A1: for x be object holds x in S iff x in ( REAL * ) & P[x] from XBOOLE_0:sch 1;

        take S;

        S c= ( REAL * ) by A1;

        hence S is Subset of ( REAL * );

        let x be object;

        thus x in S implies ex s be non empty non-decreasing FinSequence of REAL st x = s & ( dom s) = ( dom D) & for i be Nat st i in ( dom s) holds (s . i) in ( divset (D,i)) by A1;

        given s be non empty non-decreasing FinSequence of REAL such that

         A2: x = s and

         A3: ( dom s) = ( dom D) and

         A4: for i be Nat st i in ( dom s) holds (s . i) in ( divset (D,i));

        x in ( REAL * ) by A2, FINSEQ_1:def 11;

        hence x in S by A2, A3, A4, A1;

      end;

      uniqueness

      proof

        let TD1,TD2 be Subset of ( REAL * ) such that

         A1: for x be object holds x in TD1 iff ex s be non empty non-decreasing FinSequence of REAL st x = s & ( dom s) = ( dom D) & for i be Nat st i in ( dom s) holds (s . i) in ( divset (D,i)) and

         A2: for x be object holds x in TD2 iff ex s be non empty non-decreasing FinSequence of REAL st x = s & ( dom s) = ( dom D) & for i be Nat st i in ( dom s) holds (s . i) in ( divset (D,i));

        

         A3: TD1 c= TD2

        proof

          let x be object;

          assume x in TD1;

          then ex s be non empty non-decreasing FinSequence of REAL st x = s & ( dom s) = ( dom D) & for i be Nat st i in ( dom s) holds (s . i) in ( divset (D,i)) by A1;

          hence thesis by A2;

        end;

        TD2 c= TD1

        proof

          let x be object;

          assume x in TD2;

          then ex s be non empty non-decreasing FinSequence of REAL st x = s & ( dom s) = ( dom D) & for i be Nat st i in ( dom s) holds (s . i) in ( divset (D,i)) by A2;

          hence thesis by A1;

        end;

        hence thesis by A3;

      end;

    end

    theorem :: COUSIN:39

    

     Th34: for A be non empty closed_interval Subset of REAL , D be Division of A holds D in ( set_of_tagged_Division D)

    proof

      let A be non empty closed_interval Subset of REAL , D be Division of A;

      for i be Nat st i in ( dom D) holds (D . i) in ( divset (D,i))

      proof

        let i be Nat;

        assume

         A1: i in ( dom D);

        consider a,b be Real such that

         A2: ( divset (D,i)) = [.a, b.] by MEASURE5:def 3;

        a <= b by A2, XXREAL_1: 29;

        then

         A3: ( upper_bound ( divset (D,i))) = b & b in [.a, b.] by A2, JORDAN5A: 19, XXREAL_1: 1;

        1 <= i by A1, FINSEQ_3: 25;

        per cases by XXREAL_0: 1;

          suppose i = 1;

          hence thesis by A3, A2, A1, INTEGRA1:def 4;

        end;

          suppose 1 < i;

          hence thesis by A3, A2, A1, INTEGRA1:def 4;

        end;

      end;

      hence thesis by Def2;

    end;

    theorem :: COUSIN:40

    

     Th35: for a,b be Real, Iab be non empty closed_interval Subset of REAL st Iab = [.a, b.] holds <*b*> is Division of Iab

    proof

      let a,b be Real, Iab be non empty closed_interval Subset of REAL ;

      assume

       A1: Iab = [.a, b.];

      

       A2: a <= b by A1, XXREAL_1: 29;

      set D = <*b*>;

      

       A3: ( rng D) c= Iab

      proof

        let x be object;

        assume x in ( rng D);

        then x in {b} by FINSEQ_1: 39;

        then x = b by TARSKI:def 1;

        hence thesis by A1, A2, XXREAL_1: 1;

      end;

      (D . ( len D)) = ( upper_bound Iab)

      proof

        ( dom D) = ( Seg 1) by FINSEQ_1:def 8;

        

        then (D . ( len D)) = ( <*b*> . 1) by FINSEQ_1:def 3

        .= b by FINSEQ_1:def 8;

        hence thesis by A1, A2, JORDAN5A: 19;

      end;

      hence thesis by A3, INTEGRA1:def 2;

    end;

    definition

      let I be non empty closed_interval Subset of REAL ;

      :: COUSIN:def3

      mode tagged_division of I means

      : Def3: ex D be Division of I, T be Element of ( set_of_tagged_Division D) st it = [D, T];

      existence

      proof

        consider a,b be Real such that

         A1: I = [.a, b.] by MEASURE5:def 3;

        

         A2: a <= b by A1, XXREAL_1: 29;

        reconsider B = <*b*> as Division of I by A1, Th35;

        now

          thus ( dom <*b*>) = ( dom B);

          hereby

            let i be Nat;

            assume

             A3: i in ( dom B);

            then

             A4: i in {1} by FINSEQ_1: 2, FINSEQ_1:def 8;

            then

             A5: i = 1 by TARSKI:def 1;

            consider c,d be Real such that

             A6: ( divset (B,1)) = [.c, d.] by MEASURE5:def 3;

            

             A7: c <= d by A6, XXREAL_1: 29;

            1 in ( dom B) by A3, A4, TARSKI:def 1;

            then ( lower_bound ( divset (B,1))) = ( lower_bound [.a, b.]) & ( upper_bound ( divset (B,1))) = (B . 1) by A1, INTEGRA1:def 4;

            then c = ( lower_bound [.a, b.]) & d = (B . 1) by A7, A6, JORDAN5A: 19;

            then

             A8: c = a & d = b by FINSEQ_1:def 8, A2, JORDAN5A: 19;

            b in [.a, b.] by A2, XXREAL_1: 1;

            hence ( <*b*> . i) in ( divset (B,i)) by A8, A6, A5, FINSEQ_1:def 8;

          end;

        end;

        then

        reconsider T = <*b*> as Element of ( set_of_tagged_Division B) by Def2;

        take [B, T];

        thus thesis;

      end;

    end

    definition

      let I be non empty closed_interval Subset of REAL , jauge be positive-yielding Function of I, REAL , TD be tagged_division of I;

      :: COUSIN:def4

      attr TD is jauge -fine means ex D be Division of I, T be Element of ( set_of_tagged_Division D) st TD = [D, T] & for i be Nat st i in ( dom D) holds ( vol ( divset (D,i))) <= (jauge . (T . i));

    end

    begin

    theorem :: COUSIN:41

    for r be Real holds ( vol {r}) = 0

    proof

      let r be Real;

      ( vol {r}) = (( upper_bound {r}) - ( lower_bound {r})) by INTEGRA1:def 5

      .= (r - ( lower_bound {r})) by SEQ_4: 9

      .= (r - r) by SEQ_4: 9;

      hence thesis;

    end;

    theorem :: COUSIN:42

    for I1,I2 be non empty closed_interval Subset of REAL , jauge be positive-yielding Function of I1, REAL st I2 c= I1 holds (jauge | I2) is positive-yielding Function of I2, REAL by FUNCT_2: 32;

    theorem :: COUSIN:43

    for I be non empty closed_interval Subset of REAL , c be Real st c in I holds [.( lower_bound I), c.] is non empty closed_interval Subset of REAL & [.c, ( upper_bound I).] is non empty closed_interval Subset of REAL & ( upper_bound [.( lower_bound I), c.]) = ( lower_bound [.c, ( upper_bound I).])

    proof

      let I be non empty closed_interval Subset of REAL , c be Real;

      assume

       A1: c in I;

      consider a,b be Real such that

       A2: a <= b and

       A3: I = [.a, b.] by Th33;

      

       A4: ( lower_bound I) = a & ( upper_bound I) = b by A2, A3, JORDAN5A: 19;

      

       A5: a <= c <= b by A1, A3, XXREAL_1: 1;

      hence [.( lower_bound I), c.] is non empty closed_interval Subset of REAL & [.c, ( upper_bound I).] is non empty closed_interval Subset of REAL by A4, XXREAL_1: 30, MEASURE5:def 3;

      ( upper_bound [.( lower_bound I), c.]) = c by A4, A5, JORDAN5A: 19;

      hence ( upper_bound [.( lower_bound I), c.]) = ( lower_bound [.c, ( upper_bound I).]) by A4, A5, JORDAN5A: 19;

    end;

    definition

      let Iac,Icb be non empty closed_interval Subset of REAL , Dac be Division of Iac, Dcb be Division of Icb;

      assume

       A1: ( upper_bound Iac) <= ( lower_bound Icb);

      :: COUSIN:def5

      func Dac (#) Dcb -> non empty increasing FinSequence of REAL equals

      : Def4: (Dac ^ Dcb) if (Dcb . 1) <> ( upper_bound Iac)

      otherwise (Dac ^ (Dcb /^ 1));

      correctness

      proof

         Z1:

        now

          assume

           A2: (Dcb . 1) <> ( upper_bound Iac);

          

           A3: (Dac . ( len Dac)) = ( upper_bound Iac) by INTEGRA1:def 2;

          

           A4: (Dac . ( len Dac)) <= ( lower_bound Icb) by A1, INTEGRA1:def 2;

          

           A5: ( rng Dcb) c= Icb by INTEGRA1:def 2;

          ( rng Dcb) <> {} ;

          then 1 in ( dom Dcb) by FINSEQ_3: 32;

          then

           A6: (Dcb . 1) in Icb by A5, FUNCT_1: 3;

          consider c,b be Real such that

           A7: Icb = [.c, b.] by MEASURE5:def 3;

          c <= b by A7, XXREAL_1: 29;

          then ( lower_bound Icb) = c by A7, JORDAN5A: 19;

          then ( lower_bound Icb) <= (Dcb . 1) by A6, A7, XXREAL_1: 1;

          then (Dac . ( len Dac)) <= (Dcb . 1) by A4, XXREAL_0: 2;

          then (Dac . ( len Dac)) < (Dcb . 1) by A3, A2, XXREAL_0: 1;

          hence (Dac ^ Dcb) is non empty increasing FinSequence of REAL by Th1;

        end;

        now

          assume

           A8: (Dcb . 1) = ( upper_bound Iac);

          now

            assume

             A9: not (Dcb /^ 1) is empty;

            then

             A10: ( rng (Dcb /^ 1)) <> {} ;

            ( rng Dcb) <> {} ;

            then

             A11: 1 in ( dom Dcb) by FINSEQ_3: 32;

            then

             A12: 1 <= ( len Dcb) by FINSEQ_3: 25;

            then

            reconsider D2 = (Dcb /^ 1) as non empty increasing FinSequence of REAL by A9, INTEGRA1: 34;

            

             A13: (Dac . ( len Dac)) = ( upper_bound Iac) by INTEGRA1:def 2;

            1 in ( dom (Dcb /^ 1)) by A10, FINSEQ_3: 32;

            then

             A14: ((Dcb /^ 1) . 1) = (Dcb . (1 + 1)) by A12, RFINSEQ:def 1;

            1 in ( dom (Dcb /^ 1)) by A10, FINSEQ_3: 32;

            then (1 + 1) in ( dom Dcb) by FINSEQ_5: 26;

            then ( upper_bound Iac) < (D2 . 1) by A8, A14, A11, VALUED_0:def 13;

            hence (Dac ^ (Dcb /^ 1)) is non empty increasing FinSequence of REAL by A13, Th1;

          end;

          hence (Dac ^ (Dcb /^ 1)) is non empty increasing FinSequence of REAL by FINSEQ_1: 34;

        end;

        hence thesis by Z1;

      end;

    end

    theorem :: COUSIN:44

    for Iac,Icb be non empty closed_interval Subset of REAL , Dac be Division of Iac, Dcb be Division of Icb st ( upper_bound Iac) = ( lower_bound Icb) & ( len Dcb) = 1 & (Dcb . 1) = ( lower_bound Icb) holds (Dac (#) Dcb) = Dac

    proof

      let Iac,Icb be non empty closed_interval Subset of REAL , Dac be Division of Iac, Dcb be Division of Icb;

      assume that

       A1: ( upper_bound Iac) = ( lower_bound Icb) and

       A2: ( len Dcb) = 1 and

       A3: (Dcb . 1) = ( lower_bound Icb);

      ( len (Dcb /^ 1)) = (( len Dcb) - 1) by A2, RFINSEQ:def 1;

      then (Dcb /^ 1) = {} by A2;

      then (Dac ^ (Dcb /^ 1)) = Dac by FINSEQ_1: 34;

      hence thesis by A1, A3, Def4;

    end;

    theorem :: COUSIN:45

    

     Th37: for I1,I2,I be non empty closed_interval Subset of REAL st ( upper_bound I1) <= ( lower_bound I2) & ( lower_bound I) <= ( lower_bound I1) & ( upper_bound I2) <= ( upper_bound I) holds (I1 \/ I2) c= I

    proof

      let I1,I2,I be non empty closed_interval Subset of REAL such that

       A1: ( upper_bound I1) <= ( lower_bound I2) and

       A2: ( lower_bound I) <= ( lower_bound I1) and

       A3: ( upper_bound I2) <= ( upper_bound I);

      consider a1,b1 be Real such that

       A4: I1 = [.a1, b1.] by MEASURE5:def 3;

      

       A5: a1 <= b1 by A4, XXREAL_1: 29;

      then

       A6: ( lower_bound I1) = a1 & ( upper_bound I1) = b1 by A4, JORDAN5A: 19;

      consider a2,b2 be Real such that

       A7: I2 = [.a2, b2.] by MEASURE5:def 3;

      

       A8: a2 <= b2 by A7, XXREAL_1: 29;

      

       A9: ( lower_bound I) <= a1 & b2 <= ( upper_bound I) by A2, A3, A5, A4, JORDAN5A: 19, A8, A7;

      

       A10: b1 <= a2 by A6, A1, A8, A7, JORDAN5A: 19;

      consider a3,b3 be Real such that

       A11: I = [.a3, b3.] by MEASURE5:def 3;

      a3 <= b3 by A11, XXREAL_1: 29;

      then

       A12: ( lower_bound I) = a3 & ( upper_bound I) = b3 by A11, JORDAN5A: 19;

      let x be object;

      assume

       A13: x in (I1 \/ I2);

      then

      reconsider x1 = x as Real;

      per cases by A13, XBOOLE_0:def 3;

        suppose x in I1;

        then a1 <= x1 <= b1 by A4, XXREAL_1: 1;

        then a1 <= x1 <= a2 by A10, XXREAL_0: 2;

        then a1 <= x1 <= b2 by A8, XXREAL_0: 2;

        then ( lower_bound I) <= x1 <= ( upper_bound I) by A9, XXREAL_0: 2;

        hence x in I by A12, A11, XXREAL_1: 1;

      end;

        suppose x in I2;

        then a2 <= x1 <= b2 by A7, XXREAL_1: 1;

        then b1 <= x1 <= b2 by A10, XXREAL_0: 2;

        then a1 <= x1 <= b2 by A5, XXREAL_0: 2;

        then ( lower_bound I) <= x1 <= ( upper_bound I) by A9, XXREAL_0: 2;

        hence x in I by A12, A11, XXREAL_1: 1;

      end;

    end;

    theorem :: COUSIN:46

    for I1,I2,I be non empty closed_interval Subset of REAL , D1 be Division of I1, D2 be Division of I2 st ( upper_bound I1) <= ( lower_bound I2) & I = [.( lower_bound I1), ( upper_bound I2).] holds (D1 (#) D2) is Division of I

    proof

      let Iac,Icb,I be non empty closed_interval Subset of REAL , Dac be Division of Iac, Dcb be Division of Icb;

      assume that

       A1: ( upper_bound Iac) <= ( lower_bound Icb) and

       A2: I = [.( lower_bound Iac), ( upper_bound Icb).];

      ( lower_bound Iac) <= ( upper_bound Iac) by BORSUK_4: 28;

      then

       A3: ( lower_bound Iac) <= ( lower_bound Icb) by A1, XXREAL_0: 2;

      ( lower_bound Icb) <= ( upper_bound Icb) by BORSUK_4: 28;

      then

       A4: ( lower_bound Iac) <= ( upper_bound Icb) by A3, XXREAL_0: 2;

      then ( lower_bound I) = ( lower_bound Iac) & ( upper_bound I) = ( upper_bound Icb) by A2, JORDAN5A: 19;

      then

       A5: (Iac \/ Icb) c= I by A1, Th37;

      

       A6: ( rng Dac) c= Iac by INTEGRA1:def 2;

      

       A7: ( rng Dcb) c= Icb by INTEGRA1:def 2;

      ( rng Dcb) <> {} ;

      then 1 in ( dom Dcb) by FINSEQ_3: 32;

      then

       A8: 1 in ( Seg ( len Dcb)) by FINSEQ_1:def 3;

      then 1 <= ( len Dcb) by FINSEQ_1: 1;

      then

       A9: (( len Dac) + 1) <= (( len Dac) + ( len Dcb)) by XREAL_1: 7;

      set Dacb = (Dac (#) Dcb);

      per cases ;

        suppose (Dcb . 1) <> ( upper_bound Iac);

        then

         A10: Dacb = (Dac ^ Dcb) by A1, Def4;

        ( rng Dacb) = (( rng Dac) \/ ( rng Dcb)) by A10, FINSEQ_1: 31;

        then ( rng Dacb) c= (Iac \/ Icb) by A6, A7, XBOOLE_1: 13;

        then

         A11: ( rng Dacb) c= I by A5;

        ( len Dacb) = (( len Dac) + ( len Dcb)) by A10, FINSEQ_1: 22;

        

        then (Dacb . ( len Dacb)) = (Dcb . ((( len Dac) + ( len Dcb)) - ( len Dac))) by A9, A10, FINSEQ_1: 23

        .= ( upper_bound Icb) by INTEGRA1:def 2

        .= ( upper_bound I) by A4, A2, JORDAN5A: 19;

        hence thesis by A11, INTEGRA1:def 2;

      end;

        suppose

         A12: (Dcb . 1) = ( upper_bound Iac);

        then

         A13: Dacb = (Dac ^ (Dcb /^ 1)) by A1, Def4;

        then

         A14: ( rng Dacb) c= (( rng Dac) \/ ( rng (Dcb /^ 1))) by FINSEQ_1: 31;

        ( rng (Dcb /^ 1)) c= ( rng Dcb) by FINSEQ_5: 33;

        then

         A15: (( rng Dac) \/ ( rng (Dcb /^ 1))) c= (( rng Dac) \/ ( rng Dcb)) by XBOOLE_1: 13;

        (( rng Dac) \/ ( rng Dcb)) c= (Iac \/ Icb) by A6, A7, XBOOLE_1: 13;

        then ( rng Dacb) c= (Iac \/ Icb) by A14, A15;

        then

         A16: ( rng Dacb) c= I by A5;

        

         A17: ( len Dacb) = (( len Dac) + ( len (Dcb /^ 1))) by A13, FINSEQ_1: 22;

        

         A18: 1 <= ( len Dcb) by A8, FINSEQ_1: 1;

        then

         A18bis: ( len (Dcb /^ 1)) = (( len Dcb) - 1) by RFINSEQ:def 1;

        per cases ;

          suppose

           A19: ( len Dcb) = 1;

          then (Dcb /^ 1) is empty by FINSEQ_5: 32;

          then Dacb = Dac by A13, FINSEQ_1: 34;

          

          then (Dacb . ( len Dacb)) = (Dcb . ( len Dcb)) by A12, A19, INTEGRA1:def 2

          .= ( upper_bound Icb) by INTEGRA1:def 2

          .= ( upper_bound I) by A4, A2, JORDAN5A: 19;

          hence thesis by A16, INTEGRA1:def 2;

        end;

          suppose ( len Dcb) <> 1;

          then

           A20: (2 - 1) <= (( len Dcb) - 1) by NAT_1: 23, XREAL_1: 9;

          

           A21: ( Seg ( len (Dcb /^ 1))) = ( dom (Dcb /^ 1)) by FINSEQ_1:def 3;

          

           A22: ( len (Dcb /^ 1)) = (( len Dcb) - 1) by A18, RFINSEQ:def 1;

          1 <= ( len (Dcb /^ 1)) by A18, RFINSEQ:def 1, A20;

          then

           A23: ( len (Dcb /^ 1)) in ( dom (Dcb /^ 1)) by A21, FINSEQ_1: 1;

          (Dcb /^ 1) <> {} by A22, A20;

          then ( rng (Dcb /^ 1)) <> {} ;

          then 1 in ( dom (Dcb /^ 1)) by FINSEQ_3: 32;

          then 1 <= ( len (Dcb /^ 1)) by FINSEQ_3: 25;

          then (( len Dac) + 1) <= (( len Dac) + ( len (Dcb /^ 1))) <= (( len Dac) + ( len (Dcb /^ 1))) by XREAL_1: 7;

          

          then (Dacb . ( len Dacb)) = ((Dcb /^ 1) . ((( len Dac) + ( len (Dcb /^ 1))) - ( len Dac))) by A17, A13, FINSEQ_1: 23

          .= (Dcb . (( len (Dcb /^ 1)) + 1)) by A18, RFINSEQ:def 1, A23

          .= ( upper_bound Icb) by A18bis, INTEGRA1:def 2

          .= ( upper_bound I) by A4, A2, JORDAN5A: 19;

          hence thesis by A16, INTEGRA1:def 2;

        end;

      end;

    end;

    registration

      let I be non empty closed_interval Subset of REAL , D be Division of I;

      cluster ( set_of_tagged_Division D) -> non empty;

      coherence by Th34;

    end

    theorem :: COUSIN:47

    

     Th38: for s be non empty increasing FinSequence of REAL , r be Real st (s . ( len s)) < r holds (s ^ <*r*>) is non empty increasing FinSequence of REAL

    proof

      let s be non empty increasing FinSequence of REAL , r be Real;

      assume (s . ( len s)) < r;

      then (s . ( len s)) < ( <*r*> . 1) by FINSEQ_1:def 8;

      hence thesis by Th1;

    end;

    theorem :: COUSIN:48

    for s1,s2 be non empty increasing FinSequence of REAL , r be Real st (s1 . ( len s1)) < r < (s2 . 1) holds ((s1 ^ <*r*>) ^ s2) is non empty increasing FinSequence of REAL

    proof

      let s1,s2 be non empty increasing FinSequence of REAL , r be Real;

      assume

       A1: (s1 . ( len s1)) < r < (s2 . 1);

      then

      reconsider s = (s1 ^ <*r*>) as non empty increasing FinSequence of REAL by Th38;

      (s . ( len s)) = (s . (( len s1) + 1)) by FINSEQ_2: 16

      .= r by FINSEQ_1: 42;

      hence thesis by A1, Th1;

    end;

    theorem :: COUSIN:49

    for I1,I2,I be non empty closed_interval Subset of REAL st ( upper_bound I1) = ( lower_bound I2) & I = (I1 \/ I2) holds ( lower_bound I) = ( lower_bound I1) & ( upper_bound I) = ( upper_bound I2)

    proof

      let I1,I2,I be non empty closed_interval Subset of REAL ;

      assume that

       A1: ( upper_bound I1) = ( lower_bound I2) and

       A2: I = (I1 \/ I2);

      

       A3: I1 = [.( lower_bound I1), ( upper_bound I1).] by INTEGRA1: 4;

      then

       A4: ( lower_bound I1) <= ( upper_bound I1) by XXREAL_1: 29;

      

       A5: I2 = [.( lower_bound I2), ( upper_bound I2).] by INTEGRA1: 4;

      then

       A6: ( lower_bound I2) <= ( upper_bound I2) by XXREAL_1: 29;

      

       A7: I = [.( lower_bound I1), ( upper_bound I2).] by A2, A3, A5, A1, A4, A6, XXREAL_1: 165;

      

       A8: I = [.( lower_bound I), ( upper_bound I).] by INTEGRA1: 4;

      then ( lower_bound I) <= ( upper_bound I) by XXREAL_1: 29;

      hence thesis by A7, A8, XXREAL_1: 66;

    end;

    theorem :: COUSIN:50

    for I be non empty closed_interval Subset of REAL , D be Division of I holds ( divset (D,1)) = [.( lower_bound I), (D . 1).] & for j be Nat st j in ( dom D) & j <> 1 holds ( divset (D,j)) = [.(D . (j - 1)), (D . j).]

    proof

      let I be non empty closed_interval Subset of REAL , D be Division of I;

      ( rng D) <> {} ;

      then 1 in ( dom D) by FINSEQ_3: 32;

      then ( lower_bound ( divset (D,1))) = ( lower_bound I) & ( upper_bound ( divset (D,1))) = (D . 1) by INTEGRA1:def 4;

      hence ( divset (D,1)) = [.( lower_bound I), (D . 1).] by INTEGRA1: 4;

      thus for j be Nat st j in ( dom D) & j <> 1 holds ( divset (D,j)) = [.(D . (j - 1)), (D . j).]

      proof

        let j be Nat;

        assume that

         A1: j in ( dom D) and

         A2: j <> 1;

        ( lower_bound ( divset (D,j))) = (D . (j - 1)) & ( upper_bound ( divset (D,j))) = (D . j) by A1, A2, INTEGRA1:def 4;

        hence thesis by INTEGRA1: 4;

      end;

    end;

    theorem :: COUSIN:51

    for r be Real, p,q be FinSequence of REAL holds ( len ((p ^ <*r*>) ^ q)) = ((( len p) + ( len q)) + 1)

    proof

      let r be Real, p,q be FinSequence of REAL ;

      

       A1: ( len ((p ^ <*r*>) ^ q)) = (( len (p ^ <*r*>)) + ( len q)) by FINSEQ_1: 22

      .= ((( len p) + ( len <*r*>)) + ( len q)) by FINSEQ_1: 22;

      ( len <*r*>) = 1 by FINSEQ_1: 40;

      hence thesis by A1;

    end;

    registration

      let I be non empty closed_interval Subset of REAL , D be Division of I;

      cluster -> non empty for Element of ( set_of_tagged_Division D);

      coherence

      proof

        let T be Element of ( set_of_tagged_Division D);

        consider s be non empty non-decreasing FinSequence of REAL such that

         A1: T = s and ( dom s) = ( dom D) and for i be Nat st i in ( dom s) holds (s . i) in ( divset (D,i)) by Def2;

        thus thesis by A1;

      end;

    end

    theorem :: COUSIN:52

    for I be non empty closed_interval Subset of REAL , D be Division of I, T be Element of ( set_of_tagged_Division D) holds ( rng T) c= REAL

    proof

      let I be non empty closed_interval Subset of REAL , D be Division of I, T be Element of ( set_of_tagged_Division D);

      ex s be non empty non-decreasing FinSequence of REAL st T = s & ( dom s) = ( dom D) & for i be Nat st i in ( dom s) holds (s . i) in ( divset (D,i)) by Def2;

      hence thesis by FINSEQ_1:def 4;

    end;

    definition

      let I be non empty closed_interval Subset of REAL , TD be tagged_division of I;

      :: COUSIN:def6

      func division_of (TD) -> Division of I means ex D be Division of I, T be Element of ( set_of_tagged_Division D) st it = D & TD = [D, T];

      existence

      proof

        consider D be Division of I, T be Element of ( set_of_tagged_Division D) such that

         A1: TD = [D, T] by Def3;

        take D;

        thus thesis by A1;

      end;

      uniqueness by XTUPLE_0: 1;

    end

    begin

    reserve r,s for Real;

    theorem :: COUSIN:53

    for jauge be Function of [.r, s.], ]. 0 , +infty .[ st r <= s holds the set of all ( ].(x - (jauge . x)), (x + (jauge . x)).[ /\ [.r, s.]) where x be Element of [.r, s.] is Subset-Family of ( Closed-Interval-TSpace (r,s))

    proof

      let jauge be Function of [.r, s.], ]. 0 , +infty .[;

      assume

       A1: r <= s;

      set A = the set of all ( ].(x - (jauge . x)), (x + (jauge . x)).[ /\ [.r, s.]) where x be Element of [.r, s.];

      A c= ( bool [.r, s.])

      proof

        let t be object;

        assume t in A;

        then

        consider x0 be Element of [.r, s.] such that

         A2: t = ( ].(x0 - (jauge . x0)), (x0 + (jauge . x0)).[ /\ [.r, s.]);

        reconsider t as set by TARSKI: 1;

        t c= [.r, s.] by A2, XBOOLE_1: 17;

        hence thesis;

      end;

      hence thesis by A1, TOPMETR: 18;

    end;

    theorem :: COUSIN:54

    

     Th39: for jauge be Function of [.r, s.], ]. 0 , +infty .[, S be Subset-Family of ( Closed-Interval-TSpace (r,s)) st r <= s & S = the set of all ( ].(x - (jauge . x)), (x + (jauge . x)).[ /\ [.r, s.]) where x be Element of [.r, s.] holds S is Cover of ( Closed-Interval-TSpace (r,s))

    proof

      let jauge be Function of [.r, s.], ]. 0 , +infty .[, S be Subset-Family of ( Closed-Interval-TSpace (r,s));

      assume that

       A1: r <= s and

       A2: S = the set of all ( ].(x - (jauge . x)), (x + (jauge . x)).[ /\ [.r, s.]) where x be Element of [.r, s.];

       [.r, s.] c= ( union S)

      proof

        let x be object;

        assume

         A3: x in [.r, s.];

        then

        reconsider x0 = x as Element of [.r, s.];

        x0 in ( dom jauge) by A3, PARTFUN1:def 2;

        then (jauge . x0) in ( rng jauge) by FUNCT_1: 3;

        then 0 < (jauge . x0) by XXREAL_1: 4;

        then (x0 - (jauge . x0)) < (x0 - 0 ) & (x0 + 0 ) < (x0 + (jauge . x0)) by XREAL_1: 15, XREAL_1: 8;

        then x0 in ].(x0 - (jauge . x0)), (x0 + (jauge . x0)).[ by XXREAL_1: 4;

        then

         A5: x0 in ( ].(x0 - (jauge . x0)), (x0 + (jauge . x0)).[ /\ [.r, s.]) by A3, XBOOLE_0:def 4;

        ( ].(x0 - (jauge . x0)), (x0 + (jauge . x0)).[ /\ [.r, s.]) in S by A2;

        hence thesis by A5, TARSKI:def 4;

      end;

      then S is Cover of [.r, s.] by SETFAM_1:def 11;

      hence thesis by A1, TOPMETR: 18;

    end;

    theorem :: COUSIN:55

    

     Th40: for jauge be Function of [.r, s.], ]. 0 , +infty .[, S be Subset-Family of ( Closed-Interval-TSpace (r,s)) st r <= s & S = the set of all ( ].(x - (jauge . x)), (x + (jauge . x)).[ /\ [.r, s.]) where x be Element of [.r, s.] holds S is open

    proof

      let jauge be Function of [.r, s.], ]. 0 , +infty .[, S be Subset-Family of ( Closed-Interval-TSpace (r,s));

      assume that

       A1: r <= s and

       A2: S = the set of all ( ].(x - (jauge . x)), (x + (jauge . x)).[ /\ [.r, s.]) where x be Element of [.r, s.];

      for P be Subset of ( Closed-Interval-TSpace (r,s)) st P in S holds P is open

      proof

        let P be Subset of ( Closed-Interval-TSpace (r,s));

        assume P in S;

        then

        consider x0 be Element of [.r, s.] such that

         A4: P = ( ].(x0 - (jauge . x0)), (x0 + (jauge . x0)).[ /\ [.r, s.]) by A2;

        set CIT = ( Closed-Interval-TSpace (r,s)), CIM = ( Closed-Interval-MSpace (r,s));

        

         A5: CIT = ( TopSpaceMetr CIM) by TOPMETR:def 7;

        

         A6: ( TopSpaceMetr CIM) = TopStruct (# the carrier of CIM, ( Family_open_set CIM) #) by PCOMPS_1:def 5;

        reconsider I = [.r, s.] as non empty Subset of RealSpace by A1, XXREAL_1: 30;

        reconsider P1 = P as Subset of CIM by TOPMETR:def 7, A6;

        for t be Element of CIM st t in P1 holds ex r be Real st r > 0 & ( Ball (t,r)) c= P1

        proof

          let t be Element of CIM;

          assume

           A7: t in P1;

          the carrier of CIM c= the carrier of RealSpace by TOPMETR:def 1;

          then

          reconsider tr = t as Point of RealSpace ;

          reconsider XJ = ].(x0 - (jauge . x0)), (x0 + (jauge . x0)).[ as Subset of RealSpace ;

          reconsider XK = XJ as Subset of R^1 by TOPMETR: 17;

           [.r, s.] is non empty by A1, XXREAL_1: 30;

          then x0 in [.r, s.];

          then

          reconsider p = x0 as Point of RealSpace ;

          tr in XK by A7, A4, XBOOLE_0:def 4;

          then

          consider r0 be Real such that

           A8: r0 > 0 and

           A9: ( Ball (tr,r0)) c= XK by JORDAN6: 35, TOPMETR: 15, TOPMETR:def 6;

          take r0;

          ( Ball (t,r0)) = (( Ball (tr,r0)) /\ the carrier of CIM) by TOPMETR: 9;

          then ( Ball (t,r0)) = (( Ball (tr,r0)) /\ [.r, s.]) by A1, TOPMETR: 10;

          hence thesis by A4, A8, A9, XBOOLE_1: 27;

        end;

        then P in ( Family_open_set CIM) by PCOMPS_1:def 4;

        hence thesis by A5, A6, PRE_TOPC:def 2;

      end;

      hence thesis by TOPS_2:def 1;

    end;

    theorem :: COUSIN:56

    

     Th41: for jauge be Function of [.r, s.], ]. 0 , +infty .[, S be Subset-Family of ( Closed-Interval-TSpace (r,s)) st S = the set of all ( ].(x - (jauge . x)), (x + (jauge . x)).[ /\ [.r, s.]) where x be Element of [.r, s.] holds S is connected

    proof

      let jauge be Function of [.r, s.], ]. 0 , +infty .[, S be Subset-Family of ( Closed-Interval-TSpace (r,s));

      assume

       A1: S = the set of all ( ].(x - (jauge . x)), (x + (jauge . x)).[ /\ [.r, s.]) where x be Element of [.r, s.];

      for X be Subset of ( Closed-Interval-TSpace (r,s)) st X in S holds X is connected

      proof

        let X be Subset of ( Closed-Interval-TSpace (r,s));

        assume X in S;

        then

        consider x0 be Element of [.r, s.] such that

         A2: X = ( ].(x0 - (jauge . x0)), (x0 + (jauge . x0)).[ /\ [.r, s.]) by A1;

        thus thesis by A2, RCOMP_3: 43;

      end;

      hence thesis by RCOMP_3:def 1;

    end;

    theorem :: COUSIN:57

    for jauge be Function of [.r, s.], ]. 0 , +infty .[, S be Subset-Family of ( Closed-Interval-TSpace (r,s)) st r <= s & S = the set of all ( ].(x - (jauge . x)), (x + (jauge . x)).[ /\ [.r, s.]) where x be Element of [.r, s.] holds for IC be IntervalCover of S holds IC is FinSequence of ( bool REAL ) & ( rng IC) c= S & ( union ( rng IC)) = [.r, s.] & (for n be Nat st 1 <= n holds (n <= ( len IC) implies (IC /. n) is non empty) & ((n + 1) <= ( len IC) implies ( lower_bound (IC /. n)) <= ( lower_bound (IC /. (n + 1))) & ( upper_bound (IC /. n)) <= ( upper_bound (IC /. (n + 1))) & ( lower_bound (IC /. (n + 1))) < ( upper_bound (IC /. n))) & ((n + 2) <= ( len IC) implies ( upper_bound (IC /. n)) <= ( lower_bound (IC /. (n + 2))))) & ( [.r, s.] in S implies IC = <* [.r, s.]*>) & ( not [.r, s.] in S implies (ex p be Real st r < p & p <= s & (IC . 1) = [.r, p.[) & (ex p be Real st r <= p & p < s & (IC . ( len IC)) = ].p, s.]) & for n be Nat st 1 < n & n < ( len IC) holds ex p,q be Real st r <= p & p < q & q <= s & (IC . n) = ].p, q.[)

    proof

      let jauge be Function of [.r, s.], ]. 0 , +infty .[, S be Subset-Family of ( Closed-Interval-TSpace (r,s));

      assume that

       A1: r <= s and

       A2: S = the set of all ( ].(x - (jauge . x)), (x + (jauge . x)).[ /\ [.r, s.]) where x be Element of [.r, s.];

      let IC be IntervalCover of S;

      S is Subset-Family of ( Closed-Interval-TSpace (r,s)) & S is Cover of ( Closed-Interval-TSpace (r,s)) & S is open connected & r <= s by A1, A2, Th39, Th40, Th41;

      hence thesis by RCOMP_3:def 2;

    end;

    theorem :: COUSIN:58

    

     Th42: for r,s,t,x be Real holds (r <= (x - t) & (x + t) <= s implies ( ].(x - t), (x + t).[ /\ [.r, s.]) = ].(x - t), (x + t).[) & (r <= (x - t) & s < (x + t) implies ( ].(x - t), (x + t).[ /\ [.r, s.]) = ].(x - t), s.]) & ((x - t) < r & (x + t) <= s implies ( ].(x - t), (x + t).[ /\ [.r, s.]) = [.r, (x + t).[) & ((x - t) < r & s < (x + t) implies ( ].(x - t), (x + t).[ /\ [.r, s.]) = [.r, s.])

    proof

      let r,s,t,x be Real;

      hereby

        assume that

         A1: r <= (x - t) and

         A2: (x + t) <= s;

         ].(x - t), (x + t).[ c= [.r, s.]

        proof

          let u be object;

          assume

           A3: u in ].(x - t), (x + t).[;

          then

          reconsider u1 = u as Real;

          (x - t) < u1 < (x + t) by A3, XXREAL_1: 4;

          then r <= u1 <= s by A1, A2, XXREAL_0: 2;

          hence thesis by XXREAL_1: 1;

        end;

        hence ( ].(x - t), (x + t).[ /\ [.r, s.]) = ].(x - t), (x + t).[ by XBOOLE_1: 17, XBOOLE_1: 19;

      end;

      hereby

        assume that

         A4: r <= (x - t) and

         A5: s < (x + t);

        

         A6: ( ].(x - t), (x + t).[ /\ [.r, s.]) c= ].(x - t), s.]

        proof

          let u be object;

          assume

           A7: u in ( ].(x - t), (x + t).[ /\ [.r, s.]);

          then

           A8: u in ].(x - t), (x + t).[ & u in [.r, s.] by XBOOLE_0:def 4;

          reconsider u1 = u as Real by A7;

          (x - t) < u1 <= s by A8, XXREAL_1: 1, XXREAL_1: 4;

          hence thesis by XXREAL_1: 2;

        end;

         ].(x - t), s.] c= ( ].(x - t), (x + t).[ /\ [.r, s.])

        proof

          let u be object;

          assume

           A9: u in ].(x - t), s.];

          then

          reconsider u1 = u as Real;

          (x - t) < u1 <= s by A9, XXREAL_1: 2;

          then (x - t) < u1 < (x + t) & r <= u1 <= s by A4, A5, XXREAL_0: 2;

          then u in ].(x - t), (x + t).[ & u in [.r, s.] by XXREAL_1: 1, XXREAL_1: 4;

          hence thesis by XBOOLE_0:def 4;

        end;

        hence ( ].(x - t), (x + t).[ /\ [.r, s.]) = ].(x - t), s.] by A6;

      end;

      hereby

        assume that

         A10: (x - t) < r and

         A11: (x + t) <= s;

        

         A12: ( ].(x - t), (x + t).[ /\ [.r, s.]) c= [.r, (x + t).[

        proof

          let u be object;

          assume

           A13: u in ( ].(x - t), (x + t).[ /\ [.r, s.]);

          then

           A14: u in ].(x - t), (x + t).[ & u in [.r, s.] by XBOOLE_0:def 4;

          reconsider u1 = u as Real by A13;

          r <= u1 < (x + t) by A14, XXREAL_1: 4, XXREAL_1: 1;

          hence thesis by XXREAL_1: 3;

        end;

         [.r, (x + t).[ c= ( ].(x - t), (x + t).[ /\ [.r, s.])

        proof

          let u be object;

          assume

           A15: u in [.r, (x + t).[;

          then

          reconsider u1 = u as Real;

          r <= u1 < (x + t) by A15, XXREAL_1: 3;

          then (x - t) < u1 < (x + t) & r <= u1 <= s by A10, A11, XXREAL_0: 2;

          then u in ].(x - t), (x + t).[ & u in [.r, s.] by XXREAL_1: 1, XXREAL_1: 4;

          hence thesis by XBOOLE_0:def 4;

        end;

        hence ( ].(x - t), (x + t).[ /\ [.r, s.]) = [.r, (x + t).[ by A12;

      end;

      hereby

        assume that

         A16: (x - t) < r and

         A17: s < (x + t);

         [.r, s.] c= ].(x - t), (x + t).[

        proof

          let u be object;

          assume

           A18: u in [.r, s.];

          then

          reconsider u1 = u as Real;

          r <= u1 <= s by A18, XXREAL_1: 1;

          then (x - t) < u1 < (x + t) by A16, A17, XXREAL_0: 2;

          hence thesis by XXREAL_1: 4;

        end;

        hence ( ].(x - t), (x + t).[ /\ [.r, s.]) = [.r, s.] by XBOOLE_1: 17, XBOOLE_1: 19;

      end;

    end;

    theorem :: COUSIN:59

    for r,s,t,x be Real, XT be Subset of REAL st 0 < t & r <= x <= s & XT = ( ].(x - t), (x + t).[ /\ [.r, s.]) holds (r <= (x - t) & (x + t) <= s implies ( lower_bound XT) = (x - t) & ( upper_bound XT) = (x + t)) & (r <= (x - t) & s < (x + t) implies ( lower_bound XT) = (x - t) & ( upper_bound XT) = s) & ((x - t) < r & (x + t) <= s implies ( lower_bound XT) = r & ( upper_bound XT) = (x + t)) & ((x - t) < r & s < (x + t) implies ( lower_bound XT) = r & ( upper_bound XT) = s)

    proof

      let r,s,t,x be Real, XT be Subset of REAL ;

      assume that

       A1: 0 < t and

       A2: r <= x <= s and

       A3: XT = ( ].(x - t), (x + t).[ /\ [.r, s.]);

      hereby

        assume that

         A4: r <= (x - t) and

         A5: (x + t) <= s;

        (x - t) < (x - 0 ) & (x + 0 ) < (x + t) by A1, XREAL_1: 15, XREAL_1: 8;

        then

         A6: (x - t) < (x + t) by XXREAL_0: 2;

        XT = ].(x - t), (x + t).[ by A3, A4, A5, Th42;

        hence ( lower_bound XT) = (x - t) & ( upper_bound XT) = (x + t) by A6, TOPREAL6: 17;

      end;

      hereby

        assume that

         A7: r <= (x - t) and

         A8: s < (x + t);

        

         A9: (x - t) < (s - 0 ) by A2, A1, XREAL_1: 15;

        XT = ].(x - t), s.] by A3, A7, A8, Th42;

        hence ( lower_bound XT) = (x - t) & ( upper_bound XT) = s by A9, RCOMP_3: 6, RCOMP_3: 7;

      end;

      hereby

        assume that

         A10: (x - t) < r and

         A11: (x + t) <= s;

        

         A12: (r + 0 ) < (x + t) by A2, A1, XREAL_1: 8;

        XT = [.r, (x + t).[ by A10, A11, A3, Th42;

        hence ( lower_bound XT) = r & ( upper_bound XT) = (x + t) by A12, RCOMP_3: 4, RCOMP_3: 5;

      end;

      assume that

       A13: (x - t) < r and

       A14: s < (x + t);

      

       A15: r <= s by A2, XXREAL_0: 2;

      XT = [.r, s.] by A3, A13, A14, Th42;

      hence ( lower_bound XT) = r & ( upper_bound XT) = s by A15, JORDAN5A: 19;

    end;

    theorem :: COUSIN:60

    

     Th45: for a,b be Real st a < b holds <*a, b*> is non empty increasing FinSequence of REAL

    proof

      let a,b be Real;

      assume

       A1: a < b;

      set s = <*a, b*>;

      

       A2: ( rng s) c= REAL ;

      s is increasing

      proof

        now

          let e1,e2 be ExtReal;

          assume that

           A3: e1 in ( dom s) and

           A4: e2 in ( dom s) and

           A5: e1 < e2;

          ( dom s) = ( Seg ( len s)) by FINSEQ_1:def 3

          .= ( Seg 2) by FINSEQ_1: 44;

          then (e1 = 1 or e1 = 2) & (e2 = 1 or e2 = 2) by TARSKI:def 2, A3, A4, FINSEQ_1: 2;

          then (s . e1) = a & (s . e2) = b by A5, FINSEQ_1: 44;

          hence (s . e1) < (s . e2) by A1;

        end;

        hence thesis;

      end;

      hence thesis by A2, FINSEQ_1:def 4;

    end;

    theorem :: COUSIN:61

    

     Th43: for a,b,c be Real, Iac,Icb be non empty compact Subset of REAL st a <= c <= b & Iac = [.a, c.] & Icb = [.c, b.] holds for Dac be Division of Iac, Dcb be Division of Icb, i,j be Nat st i in ( dom Dac) & j in ( dom Dcb) holds (i < ( len Dac) implies (Dac . i) < (Dcb . j)) & ((i = ( len Dac) & c < (Dcb . 1)) implies (Dac . i) < (Dcb . j)) & ((Dcb . 1) = c implies (Dac . ( len Dac)) = (Dcb . 1))

    proof

      let a,b,c be Real, Iac,Icb be non empty compact Subset of REAL ;

      assume that

       A1: a <= c <= b and

       A2: Iac = [.a, c.] and

       A3: Icb = [.c, b.];

      let Dac be Division of Iac, Dcb be Division of Icb, i,j be Nat;

      assume that

       A4: i in ( dom Dac) and

       A5: j in ( dom Dcb);

      

       A6: (Dac . ( len Dac)) = ( upper_bound Iac) by INTEGRA1:def 2

      .= c by A1, A2, JORDAN5A: 19;

      ( rng Dcb) c= [.c, b.] by A3, INTEGRA1:def 2;

      then (Dcb . j) in [.c, b.] by A5, FUNCT_1: 3;

      then

       A7: c <= (Dcb . j) by XXREAL_1: 1;

      thus i < ( len Dac) implies (Dac . i) < (Dcb . j)

      proof

        assume

         A8: i < ( len Dac);

        ( Seg ( len Dac)) = ( dom Dac) by FINSEQ_1:def 3;

        then ( len Dac) in ( dom Dac) by FINSEQ_1: 3;

        then (Dac . i) < c by A6, A8, A4, VALUED_0:def 13;

        hence (Dac . i) < (Dcb . j) by A7, XXREAL_0: 2;

      end;

      thus i = ( len Dac) & c < (Dcb . 1) implies (Dac . i) < (Dcb . j)

      proof

        assume

         A9: i = ( len Dac) & c < (Dcb . 1);

        

         A10: 1 in ( dom Dcb) by FINSEQ_5: 6;

        j in ( Seg ( len Dcb)) by A5, FINSEQ_1:def 3;

        then j = 1 or ... or j = ( len Dcb) by FINSEQ_1: 91;

        per cases by XXREAL_0: 1;

          suppose j = 1;

          hence thesis by A9, A6;

        end;

          suppose 1 < j;

          then (Dcb . 1) < (Dcb . j) by A10, A5, VALUED_0:def 13;

          hence thesis by A9, A6, XXREAL_0: 2;

        end;

      end;

      thus (Dcb . 1) = c implies (Dac . ( len Dac)) = (Dcb . 1) by A6;

    end;

    theorem :: COUSIN:62

    

     Th44: for a,b,c be Real, Iac,Icb be non empty compact Subset of REAL st a <= c <= b & Iac = [.a, c.] & Icb = [.c, b.] holds for Dac be Division of Iac, Dcb be Division of Icb, i,j be Nat st i in ( dom Dac) & j in ( dom Dcb) holds c < (Dcb . 1) implies (Dac . i) < (Dcb . j)

    proof

      let a,b,c be Real, Iac,Icb be non empty compact Subset of REAL ;

      assume that

       A1: a <= c <= b and

       A2: Iac = [.a, c.] and

       A3: Icb = [.c, b.];

      let Dac be Division of Iac, Dcb be Division of Icb, i,j be Nat;

      assume that

       A4: i in ( dom Dac) and

       A5: j in ( dom Dcb);

      assume

       A6: c < (Dcb . 1);

      i <= ( len Dac) by A4, FINSEQ_3: 25;

      then i < ( len Dac) or i = ( len Dac) by XXREAL_0: 1;

      hence thesis by A6, A1, A2, A3, A4, A5, Th43;

    end;

    theorem :: COUSIN:63

    for a,b,c be Real, Iab,Iac,Icb be non empty compact Subset of REAL st a <= c <= b & Iab = [.a, b.] & Iac = [.a, c.] & Icb = [.c, b.] holds for Dac be Division of Iac, Dcb be Division of Icb st c < (Dcb . 1) holds (Dac ^ Dcb) is Division of Iab

    proof

      let a,b,c be Real, Iab,Iac,Icb be non empty compact Subset of REAL ;

      assume that

       A1: a <= c <= b and

       A2: Iab = [.a, b.] and

       A3: Iac = [.a, c.] and

       A4: Icb = [.c, b.];

      let Dac be Division of Iac, Dcb be Division of Icb;

      assume

       A5: c < (Dcb . 1);

      set Dacb = (Dac ^ Dcb);

      for e1,e2 be ExtReal st e1 in ( dom Dacb) & e2 in ( dom Dacb) & e1 < e2 holds (Dacb . e1) < (Dacb . e2)

      proof

        let e1,e2 be ExtReal;

        assume that

         A6: e1 in ( dom Dacb) and

         A7: e2 in ( dom Dacb) and

         A8: e1 < e2;

        per cases by A6, A7, FINSEQ_1: 25;

          suppose

           A9: e1 in ( dom Dac) & e2 in ( dom Dac);

          then

           A10: (Dacb . e1) = (Dac . e1) & (Dacb . e2) = (Dac . e2) by FINSEQ_1:def 7;

          e1 < e2 & Dac is increasing by A8;

          hence thesis by A9, A10;

        end;

          suppose

           A11: e1 in ( dom Dac) & ex n be Nat st n in ( dom Dcb) & e2 = (( len Dac) + n);

          then

          consider n0 be Nat such that

           A12: n0 in ( dom Dcb) and

           A13: e2 = (( len Dac) + n0);

          (Dacb . e1) = (Dac . e1) & (Dacb . e2) = (Dcb . n0) by A11, A13, FINSEQ_1:def 7;

          hence thesis by A11, A12, A3, A4, A5, Th44, A1;

        end;

          suppose

           A14: (ex n be Nat st n in ( dom Dcb) & e1 = (( len Dac) + n)) & e2 in ( dom Dac);

          then

          consider n0 be Nat such that n0 in ( dom Dcb) and

           A15: e1 = (( len Dac) + n0);

          

           A16: ( len Dac) <= e1 by A15, NAT_1: 11;

          e2 in ( Seg ( len Dac)) by FINSEQ_1:def 3, A14;

          then e2 <= ( len Dac) by FINSEQ_1: 1;

          hence thesis by A8, A16, XXREAL_0: 2;

        end;

          suppose

           A17: (ex n be Nat st n in ( dom Dcb) & e1 = (( len Dac) + n)) & (ex n be Nat st n in ( dom Dcb) & e2 = (( len Dac) + n));

          then

          consider n1 be Nat such that

           A18: n1 in ( dom Dcb) and

           A19: e1 = (( len Dac) + n1);

          consider n2 be Nat such that

           A20: n2 in ( dom Dcb) and

           A21: e2 = (( len Dac) + n2) by A17;

          

           A22: ((( len Dac) + n1) - ( len Dac)) < ((( len Dac) + n2) - ( len Dac)) by A8, A19, A21, XREAL_1: 14;

          (Dcb . n1) = (Dacb . e1) & (Dcb . n2) = (Dacb . e2) by A17, A19, A21, FINSEQ_1:def 7;

          hence thesis by A22, A18, A20, VALUED_0:def 13;

        end;

      end;

      then

       A23: Dacb is increasing;

      

       A24: ( rng Dacb) c= Iab

      proof

        let x be object;

        assume

         A25: x in ( rng Dacb);

        

         A26: ( rng Dac) c= [.a, c.] by A3, INTEGRA1:def 2;

        ( rng Dcb) c= [.c, b.] by A4, INTEGRA1:def 2;

        then (( rng Dac) \/ ( rng Dcb)) c= ( [.a, c.] \/ [.c, b.]) by XBOOLE_1: 13, A26;

        then ( rng Dacb) c= ( [.a, c.] \/ [.c, b.]) by FINSEQ_1: 31;

        then ( rng Dacb) c= [.a, b.] by A1, XXREAL_1: 165;

        hence thesis by A25, A2;

      end;

      (Dacb . ( len Dacb)) = ( upper_bound Iab)

      proof

        

         A27: a <= b by A1, XXREAL_0: 2;

        

         A28: ( len Dcb) in ( Seg ( len Dcb)) by FINSEQ_1: 3;

        

         A29: ( Seg ( len Dcb)) = ( dom Dcb) by FINSEQ_1:def 3;

        ( len Dacb) = (( len Dac) + ( len Dcb)) by FINSEQ_1: 22;

        

        then (Dacb . ( len Dacb)) = (Dcb . ( len Dcb)) by A29, A28, FINSEQ_1:def 7

        .= ( upper_bound Icb) by INTEGRA1:def 2

        .= b by JORDAN5A: 19, A1, A4

        .= ( upper_bound [.a, b.]) by A27, JORDAN5A: 19;

        hence thesis by A2;

      end;

      hence thesis by A23, A24, INTEGRA1:def 2;

    end;

    theorem :: COUSIN:64

    for a,b be Real, Iab be non empty closed_interval Subset of REAL st a <= b & Iab = [.a, b.] holds for Dab be Division of Iab st ( len Dab) = 1 holds Dab = <*b*>

    proof

      let a,b be Real, Iab be non empty closed_interval Subset of REAL ;

      assume that

       A1: a <= b and

       A2: Iab = [.a, b.];

      let Dab be Division of Iab;

      assume

       A3: ( len Dab) = 1;

      then

      consider d be Real such that

       A4: Dab = <*(Dab . 1)*> by FINSEQ_1: 40;

      (Dab . 1) = ( upper_bound Iab) by A3, INTEGRA1:def 2

      .= b by A1, A2, JORDAN5A: 19;

      hence thesis by A4;

    end;

    theorem :: COUSIN:65

    for a,b be Real, Iab be non empty compact Subset of REAL , Dab be Division of Iab st 2 <= ( len Dab) holds (Dab /^ 1) is Division of Iab

    proof

      let a,b be Real, Iab be non empty compact Subset of REAL , Dab be Division of Iab;

      assume

       A1: 2 <= ( len Dab);

      set D = (Dab /^ 1);

      

       A2: 1 <= ( len Dab) by A1, XXREAL_0: 2;

      then

       A3: ( len D) = (( len Dab) - 1) by RFINSEQ:def 1;

      

       A5: D is non empty

      proof

        (2 - 1) <= (( len Dab) - 1) by A1, XREAL_1: 13;

        hence thesis by A3;

      end;

      

       A4: D is non empty increasing

      proof

        D is increasing

        proof

          now

            let e1,e2 be ExtReal;

            assume that

             A6: e1 in ( dom D) and

             A7: e2 in ( dom D) and

             A8: e1 < e2;

            reconsider ne1 = e1, ne2 = e2 as Nat by A6, A7;

            

             A9: (D . e1) = (Dab . (ne1 + 1)) by A2, A6, RFINSEQ:def 1;

            ne1 in ( Seg ( len D)) by A6, FINSEQ_1:def 3;

            then (ne1 + 1) in ( Seg (( len D) + 1)) by FINSEQ_1: 60;

            then

             A10: (ne1 + 1) in ( dom Dab) by A3, FINSEQ_1:def 3;

            ne2 in ( Seg ( len D)) & ne2 in ( Seg ( len D)) by A7, FINSEQ_1:def 3;

            then (ne2 + 1) in ( Seg (( len D) + 1)) by FINSEQ_1: 60;

            then

             A11: (ne2 + 1) in ( dom Dab) by A3, FINSEQ_1:def 3;

            

             A12: (D . e2) = (Dab . (ne2 + 1)) by A2, A7, RFINSEQ:def 1;

            (ne1 + 1) < (ne2 + 1) by A8, XREAL_1: 8;

            hence (D . e1) < (D . e2) by A9, A12, A10, A11, VALUED_0:def 13;

          end;

          hence thesis;

        end;

        hence thesis by A5;

      end;

      

       A13: ( rng D) c= Iab

      proof

        

         A14: ( rng D) c= ( rng Dab) by FINSEQ_5: 33;

        ( rng Dab) c= Iab by INTEGRA1:def 2;

        hence thesis by A14;

      end;

      (D . ( len D)) = ( upper_bound Iab)

      proof

        (2 - 1) <= (( len Dab) - 1) by A1, XREAL_1: 13;

        then ( Seg ( len D)) = ( dom D) & ( len D) in ( Seg ( len D)) by A3, FINSEQ_1:def 3, FINSEQ_1: 3;

        

        then (D . ( len D)) = (Dab . (( len D) + 1)) by A2, RFINSEQ:def 1

        .= (Dab . ( len Dab)) by A3;

        hence thesis by INTEGRA1:def 2;

      end;

      hence thesis by A4, A13, INTEGRA1:def 2;

    end;

    theorem :: COUSIN:66

    for a,b be Real, Iab be non empty closed_interval Subset of REAL st a < b & Iab = [.a, b.] holds <*a, b*> is Division of Iab

    proof

      let a,b be Real, Iab be non empty closed_interval Subset of REAL ;

      assume that

       A1: a < b and

       A2: Iab = [.a, b.];

      set D = <*a, b*>;

      

       A3: D is non empty increasing FinSequence of REAL by A1, Th45;

      

       A4: ( rng D) c= Iab

      proof

        let x be object;

        assume x in ( rng D);

        then x in {a, b} by FINSEQ_2: 127;

        then x = a or x = b by TARSKI:def 2;

        hence thesis by A1, A2, XXREAL_1: 1;

      end;

      (D . ( len D)) = ( upper_bound Iab)

      proof

        

         A5: ( len D) = 2 by FINSEQ_1: 44;

        ( upper_bound Iab) = b by A1, A2, JORDAN5A: 19;

        hence thesis by A5, FINSEQ_1: 44;

      end;

      hence thesis by A3, A4, INTEGRA1:def 2;

    end;

    begin

    theorem :: COUSIN:67

    

     Th46: for a,b be Real, jauge be positive-yielding Function of [.a, b.], REAL st a <= b holds ex x be non empty increasing FinSequence of REAL , t be non empty FinSequence of REAL st (x . 1) = a & (x . ( len x)) = b & (t . 1) = a & ( dom x) = ( dom t) & (for i be Nat st (i - 1) in ( dom t) & i in ( dom t) holds ((t . i) - (jauge . (t . i))) <= (x . (i - 1)) <= (t . i)) & (for i be Nat st i in ( dom t) holds (t . i) <= (x . i) <= ((t . i) + (jauge . (t . i))))

    proof

      let a,b be Real, jauge be positive-yielding Function of [.a, b.], REAL ;

      assume

       A1: a <= b;

      defpred P[ object] means ex x be non empty increasing FinSequence of REAL , t be non empty FinSequence of REAL st (x . 1) = a & (x . ( len x)) = $1 & (t . 1) = a & ( dom x) = ( dom t) & (for i be Nat st (i - 1) in ( dom t) & i in ( dom t) holds ((t . i) - (jauge . (t . i))) <= (x . (i - 1)) <= (t . i)) & (for i be Nat st i in ( dom t) holds (t . i) <= (x . i) <= ((t . i) + (jauge . (t . i))));

      consider C be set such that

       A2: for x be object holds x in C iff x in [.a, b.] & P[x] from XBOOLE_0:sch 1;

      for x be object st x in C holds x is real

      proof

        let x be object;

        assume x in C;

        then x in [.a, b.] by A2;

        hence thesis;

      end;

      then

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

       A3:

      now

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

        now

          set x = <*a*>, t = <*a*>;

          take x, t;

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

          thus ( dom x) = ( dom t);

          thus for i be Nat st (i - 1) in ( dom t) & i in ( dom t) holds ((t . i) - (jauge . (t . i))) <= (x . (i - 1)) <= (t . i)

          proof

            let i be Nat;

            assume (i - 1) in ( dom t) & i in ( dom t);

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

          end;

          thus for i be Nat st i in ( dom t) holds (t . i) <= (x . i) <= ((t . i) + (jauge . (t . i)))

          proof

            let i be Nat;

            assume i in ( dom t);

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

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

          end;

        end;

        hence P[a];

      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 C is non empty bounded_above 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.];

        per cases by XXREAL_1: 1;

          suppose c < a;

          hence thesis by A3, A2, XXREAL_2: 4;

        end;

          suppose b < c;

          hence thesis by A6, XXREAL_2:def 3;

        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 be Element of ExtREAL such that

       A10: d in C and

       A11: (c - (jauge . c)) < d by A9, XXREAL_2: 94;

      consider D0 be non empty increasing FinSequence of REAL , T0 be 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 be Nat st (i - 1) in ( dom T0) & i in ( dom T0) holds ((T0 . i) - (jauge . (T0 . i))) <= (D0 . (i - 1)) <= (T0 . i)) and

       A16: (for i be Nat st i in ( dom T0) holds (T0 . i) <= (D0 . i) <= ((T0 . i) + (jauge . (T0 . i)))) by A10, A2;

      set D1 = (D0 ^ <*c*>), T1 = (T0 ^ <*c*>);

      

       A17: c in C & P[c]

      proof

        per cases ;

          suppose d = c;

          hence thesis by A10, A12, A13, A13bis, A14, A15, A16;

        end;

          suppose

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

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

            now

              reconsider D2 = D1 as non empty increasing FinSequence of REAL by A20, Th1;

              reconsider T2 = T1 as non empty FinSequence of REAL ;

              take D2, T2;

              ( rng D0) <> {} ;

              then 1 in ( dom D0) by FINSEQ_3: 32;

              hence (D2 . 1) = a by A12, FINSEQ_1:def 7;

              

               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;

              ( rng T0) <> {} ;

              then 1 in ( dom T0) by FINSEQ_3: 32;

              hence (T2 . 1) = a by A13bis, FINSEQ_1:def 7;

              

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

              

               A24: ( Seg ( len D2)) = ( dom T2) by A23, FINSEQ_1:def 3;

              hereby

                let i be Nat;

                assume that

                 A25: (i - 1) in ( dom T2) and

                 A26: i in ( dom T2);

                

                 A27: (i - 1) in ( dom T0) or ex n1 be Nat st n1 in ( dom <*c*>) & (i - 1) = (( len T0) + n1) by A25, FINSEQ_1: 25;

                

                 A28: (ex n1 be Nat st n1 in ( dom <*c*>) & (i - 1) = (( len T0) + n1)) implies i = (( len T0) + 2)

                proof

                  given n1 be Nat such that

                   A29: n1 in ( dom <*c*>) and

                   A30: (i - 1) = (( len T0) + n1);

                  n1 in ( Seg 1) by A29, FINSEQ_1:def 8;

                  then n1 = 1 by TARSKI:def 1, FINSEQ_1: 2;

                  hence thesis by A30;

                end;

                per cases by A26, FINSEQ_1: 25;

                  suppose

                   A40: i in ( dom T0);

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

                    then ((T0 . i) - (jauge . (T0 . i))) <= (D0 . (i - 1)) <= (T0 . i) by A40, A15;

                    hence ((T2 . i) - (jauge . (T2 . i))) <= (D2 . (i - 1)) <= (T2 . i) by A41, A42, A14, FINSEQ_1:def 7;

                  end;

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

                    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)) <= (T2 . i);

                  end;

                end;

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

                  then

                  consider n0 be 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)) <= (T2 . i) by A11, A19, A47, A45, A44, A27, A28, A14, FINSEQ_1:def 7, TARSKI:def 1, FINSEQ_1: 2;

                end;

              end;

              hereby

                let i be Nat;

                assume i in ( dom T2);

                per cases by FINSEQ_1: 25;

                  suppose

                   A48: i in ( dom T0);

                  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) <= ((T2 . i) + (jauge . (T2 . i))) by A16, A49, A48;

                end;

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

                  then

                  consider n0 be 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) <= ((T2 . i) + (jauge . (T2 . i))) by A55, FINSEQ_1:def 8, A57;

                end;

              end;

            end;

            hence P[c];

          end;

          hence thesis by A2;

        end;

      end;

      c = b

      proof

        assume

         A58: c <> b;

        

         A59: a <= c <= b by A7, XXREAL_1: 1;

        set c2 = ( min ((c + ((jauge . c) / 2)),b));

        

         A60: c2 in C & P[c2]

        proof

          set D1 = (D0 ^ <*c2*>), T1 = (T0 ^ <*c*>);

          per cases ;

            suppose d = c2;

            hence thesis by A10, A2;

          end;

            suppose

             A61: d <> c2;

            

             A62: 0 < (jauge . c) by A8, PARTFUN3:def 1;

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

              d in [.a, b.] by A10, A2;

              then a <= d <= b by XXREAL_1: 1;

              then c2 = ( min (d,(c + ((jauge . c) / 2)))) by A65, XXREAL_0: 1;

              hence thesis by A63, XXREAL_0:def 9, A61;

            end;

            (d + 0 ) < (c + ((jauge . c) / 2)) by A10, XXREAL_2: 4, A62, XREAL_1: 8;

            then (D0 . ( len D0)) < c2 by A13, A64, XXREAL_0: 21;

            then

             A66: (D0 . ( len D0)) < ( <*c2*> . 1) by FINSEQ_1:def 8;

            now

              thus

               A67: c2 in [.a, b.]

              proof

                

                 A68: c2 <= b by XXREAL_0: 17;

                c in [.a, b.] by A17, A2;

                then

                 A69: a <= 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 <= c2 by A1, XXREAL_0: 20;

                hence thesis by A68, XXREAL_1: 1;

              end;

              now

                reconsider D2 = D1 as non empty increasing FinSequence of REAL by A66, Th1;

                reconsider T2 = T1 as non empty FinSequence of REAL ;

                take D2, T2;

                ( rng D0) <> {} ;

                then 1 in ( dom D0) by FINSEQ_3: 32;

                hence (D2 . 1) = a by A12, FINSEQ_1:def 7;

                

                 A70: ( len D2) = (( len D0) + ( len <*c2*>)) by FINSEQ_1: 22

                .= (( len D0) + 1) by FINSEQ_1: 39;

                1 in ( Seg 1) by FINSEQ_1: 1;

                then 1 in ( dom <*c2*>) by FINSEQ_1:def 8;

                

                then (D2 . ( len D2)) = ( <*c2*> . 1) by A70, FINSEQ_1:def 7

                .= c2 by FINSEQ_1:def 8;

                hence (D2 . ( len D2)) = c2;

                ( rng T0) <> {} ;

                then 1 in ( dom T0) by FINSEQ_3: 32;

                hence (T2 . 1) = a by A13bis, FINSEQ_1:def 7;

                

                 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 ^ <*c2*>))) 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);

                

                 A73: ( Seg ( len D2)) = ( dom T2) by A72, FINSEQ_1:def 3;

                hereby

                  let i be Nat;

                  assume that

                   A74: (i - 1) in ( dom T2) and

                   A75: i in ( dom T2);

                  

                   A76: (ex n1 be Nat st n1 in ( dom <*c*>) & (i - 1) = (( len T0) + n1)) implies i = (( len T0) + 2)

                  proof

                    given n1 be Nat such that

                     A77: n1 in ( dom <*c*>) and

                     A78: (i - 1) = (( len T0) + n1);

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

                  end;

                  per cases by A75, FINSEQ_1: 25;

                    suppose

                     A79: i in ( dom T0);

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

                      then ((T0 . i) - (jauge . (T0 . i))) <= (D0 . (i - 1)) <= (T0 . i) by A79, A15;

                      hence ((T2 . i) - (jauge . (T2 . i))) <= (D2 . (i - 1)) <= (T2 . i) by A80, A81, A14, FINSEQ_1:def 7;

                    end;

                      suppose

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

                      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)) <= (T2 . i);

                    end;

                  end;

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

                    then

                    consider n0 be 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)) <= c by A10, XXREAL_2: 4, A11;

                    hence ((T2 . i) - (jauge . (T2 . i))) <= (D2 . (i - 1)) <= (T2 . i) by A88, A87, A14, FINSEQ_1:def 7;

                  end;

                end;

                hereby

                  let i be Nat;

                  assume i in ( dom T2);

                  per cases by FINSEQ_1: 25;

                    suppose

                     A89: i in ( dom T0);

                    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) <= ((T2 . i) + (jauge . (T2 . i))) by A16, A90, A89;

                  end;

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

                    then

                    consider n0 be 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 <*c2*>) by FINSEQ_1:def 8;

                    

                    then

                     A97: (D2 . i) = ( <*c2*> . 1) by A96, FINSEQ_1:def 7

                    .= c2 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;

                    c2 <= (c + ((jauge . c) / 2)) by XXREAL_0: 17;

                    hence (T2 . i) <= (D2 . i) <= ((T2 . i) + (jauge . (T2 . i))) by A101, XXREAL_0: 2, A95, A97, A100, A98, XXREAL_0: 20;

                  end;

                end;

              end;

              hence c2 in [.a, b.] & P[c2] by A67;

            end;

            hence c2 in C & P[c2] by A2;

          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 < c2 by A102, XXREAL_0:def 9;

        hence thesis by A60, XXREAL_2: 4;

      end;

      hence thesis by A17;

    end;

    ::$Notion-Name

    theorem :: COUSIN:68

    

     Th47: for I be non empty closed_interval Subset of REAL , jauge be positive-yielding Function of I, REAL holds ex TD be tagged_division of I st TD is jauge -fine

    proof

      let I be non empty closed_interval Subset of REAL , jauge be positive-yielding Function of I, REAL ;

      consider a,b be Real such that

       A1: a <= b and

       A2: I = [.a, b.] by Th33;

      

       A3: ( lower_bound I) = a & ( upper_bound I) = b by A1, A2, JORDAN5A: 19;

      reconsider r = (1 / 2) as positive Real;

      reconsider jauge2 = (r (#) jauge) as positive-yielding Function of I, REAL ;

      consider x be non empty increasing FinSequence of REAL , t be non empty FinSequence of REAL such that

       A4: (x . 1) = a and

       A5: (x . ( len x)) = b and

       A6: (t . 1) = a and

       A7: ( dom x) = ( dom t) and

       A8: for i be Nat st (i - 1) in ( dom t) & i in ( dom t) holds ((t . i) - (jauge2 . (t . i))) <= (x . (i - 1)) <= (t . i) and

       A9: for i be Nat st i in ( dom t) holds (t . i) <= (x . i) <= ((t . i) + (jauge2 . (t . i))) by A1, A2, Th46;

      now

        thus ( rng x) c= I

        proof

          let u be object;

          assume

           A10: u in ( rng x);

          then

          consider v be object such that

           A11: v in ( dom x) and

           A12: (x . v) = u by FUNCT_1:def 3;

          ( rng x) c= REAL ;

          then

          reconsider u1 = u as Element of REAL by A11, A12, FUNCT_1: 3;

          reconsider v1 = v as Nat by A11;

          

           A13: 1 in ( dom x) by A10, FINSEQ_3: 31;

          1 <= v1 by A11, FINSEQ_3: 25;

          per cases by XXREAL_0: 1;

            suppose v1 = 1;

            hence thesis by A1, A2, A4, A12, XXREAL_1: 1;

          end;

            suppose

             A14: 1 < v1;

            v1 <= ( len x) by A11, FINSEQ_3: 25;

            per cases by XXREAL_0: 1;

              suppose

               A15: v1 < ( len x);

              ( len x) in ( dom x) by FINSEQ_5: 6;

              then a <= u1 <= b by A5, A15, A14, A13, A4, A12, A11, VALUED_0:def 13;

              hence thesis by A2, XXREAL_1: 1;

            end;

              suppose v1 = ( len x);

              hence thesis by A1, A2, A5, A12, XXREAL_1: 1;

            end;

          end;

        end;

        thus (x . ( len x)) = ( upper_bound I) by A5, A1, A2, JORDAN5A: 19;

      end;

      then

      reconsider D = x as Division of I by INTEGRA1:def 2;

      now

        t is non-decreasing

        proof

          assume not t is non-decreasing;

          then

          consider e1,e2 be ExtReal such that

           A16: e1 in ( dom t) and

           A17: e2 in ( dom t) and

           A18: e1 <= e2 and

           A19: (t . e2) < (t . e1);

          1 <= e1 by FINSEQ_3: 25, A16;

          per cases by XXREAL_0: 1;

            suppose

             A20: e1 = 1;

            1 <= e2 by FINSEQ_3: 25, A17;

            per cases by XXREAL_0: 1;

              suppose e2 = 1;

              hence thesis by A19, A20;

            end;

              suppose

               A21: 1 < e2;

              reconsider f2 = e2 as Nat by A17;

              (f2 - 1) in ( dom t) by A17, A21, CGAMES_1: 20;

              then

               A22: (x . (f2 - 1)) <= (t . f2) by A8, A17;

              ( rng x) <> {} ;

              then

               A23: 1 in ( dom x) by FINSEQ_3: 32;

              (f2 - 1) in ( dom x) by A17, A21, CGAMES_1: 20, A7;

              then (x . 1) <= (x . (f2 - 1)) by A23, FINSEQ_3: 25, VALUED_0:def 15;

              hence thesis by A4, A22, XXREAL_0: 2, A19, A6, A20;

            end;

          end;

            suppose

             A24: 1 < e1;

            per cases by A18, XXREAL_0: 1;

              suppose e1 = e2;

              hence thesis by A19;

            end;

              suppose

               A25: e1 < e2;

              

               A26: (t . e1) <= (x . e1) by A16, A9;

              reconsider f2 = e2 as Nat by A17;

              1 < e2 by A24, A25, XXREAL_0: 2;

              then

               A27: (f2 - 1) in ( dom t) by A17, CGAMES_1: 20;

              then

               A28: (x . (f2 - 1)) <= (t . e2) by A17, A8;

              per cases ;

                suppose e1 = (f2 - 1);

                then (x . e1) <= (t . e2) by A27, A17, A8;

                hence thesis by A26, XXREAL_0: 2, A19;

              end;

                suppose

                 A29: e1 <> (f2 - 1);

                reconsider f1 = e1 as Nat by A16;

                f1 < (f2 - 1)

                proof

                  assume (f2 - 1) <= f1;

                  then ((f2 - 1) + 1) <= (f1 + 1) by XREAL_1: 6;

                  then f1 = f2 or f2 = (f1 + 1) by A18, NAT_1: 9;

                  hence thesis by A25, A29;

                end;

                then (x . e1) < (x . (f2 - 1)) by A27, A7, A16, VALUED_0:def 13;

                then (x . e1) <= (t . e2) by A28, XXREAL_0: 2;

                hence thesis by A19, A26, XXREAL_0: 2;

              end;

            end;

          end;

        end;

        then

        reconsider s = t as non empty non-decreasing FinSequence of REAL ;

        take s;

        thus t = s;

        thus ( dom s) = ( dom D) by A7;

        thus for i be Nat st i in ( dom s) holds (s . i) in ( divset (D,i))

        proof

          let i be Nat;

          assume

           A30: i in ( dom s);

          consider d1,d2 be Real such that

           A31: ( divset (D,i)) = [.d1, d2.] by MEASURE5:def 3;

          

           A32: d1 <= d2 by A31, XXREAL_1: 29;

          1 <= i by FINSEQ_3: 25, A30;

          per cases by XXREAL_0: 1;

            suppose

             A33: i = 1;

            then ( lower_bound ( divset (D,i))) = ( lower_bound I) & ( upper_bound ( divset (D,i))) = (D . 1) by A7, A30, INTEGRA1:def 4;

            then d1 = a & d2 = (D . 1) by A32, A31, JORDAN5A: 19, A3;

            hence thesis by A6, A4, A31, A33, XXREAL_1: 1;

          end;

            suppose

             A34: 1 < i;

            then ( lower_bound ( divset (D,i))) = (D . (i - 1)) & ( upper_bound ( divset (D,i))) = (D . i) by A7, A30, INTEGRA1:def 4;

            then

             A35: d1 = (D . (i - 1)) & d2 = (D . i) by A32, A31, JORDAN5A: 19;

            (i - 1) in ( dom t) by A30, CGAMES_1: 20, A34;

            then (D . (i - 1)) <= (s . i) <= (D . i) by A30, A8, A9;

            hence thesis by A31, A35, XXREAL_1: 1;

          end;

        end;

      end;

      then

      reconsider T = t as Element of ( set_of_tagged_Division D) by Def2;

      reconsider TD = [D, T] as tagged_division of I by Def3;

      take TD;

      now

        take D;

        thus D is Division of I;

        take T;

        thus T is Element of ( set_of_tagged_Division D);

        thus TD = [D, T];

        thus for i be Nat st i in ( dom D) holds ( vol ( divset (D,i))) <= (jauge . (T . i))

        proof

          let i be Nat;

          assume

           A36: i in ( dom D);

          consider u,v be Real such that

           A37: ( divset (D,i)) = [.u, v.] by MEASURE5:def 3;

          u <= v by A37, XXREAL_1: 29;

          then

           A38: ( lower_bound ( divset (D,i))) = u & ( upper_bound ( divset (D,i))) = v by A37, JORDAN5A: 19;

          1 <= i by FINSEQ_3: 25, A36;

          per cases by XXREAL_0: 1;

            suppose

             A39: i = 1;

            then

             A40: u = ( lower_bound I) & v = (D . 1) by A36, A38, INTEGRA1:def 4;

            

             A41: ( vol ( divset (D,i))) = (v - u) by A38, INTEGRA1:def 5

            .= ((D . 1) - a) by A40, A1, A2, JORDAN5A: 19

            .= 0 by A4;

            (T . i) in [.a, b.] by A39, A6, A1, XXREAL_1: 1;

            then (T . i) in ( dom jauge) by A2, FUNCT_2:def 1;

            then (jauge . (T . i)) in ( rng jauge) by FUNCT_1: 3;

            hence thesis by A41, PARTFUN3:def 1;

          end;

            suppose

             A42: 1 < i;

            then

             A43: u = (D . (i - 1)) & v = (D . i) by A36, A38, INTEGRA1:def 4;

            (i - 1) in ( dom t) by A36, A7, A42, CGAMES_1: 20;

            then

             A44: ((t . i) - (jauge2 . (t . i))) <= (x . (i - 1)) by A36, A7, A8;

            consider s be non empty non-decreasing FinSequence of REAL such that

             A46: T = s and

             A47: ( dom s) = ( dom D) and

             A48: for i be Nat st i in ( dom s) holds (s . i) in ( divset (D,i)) by Def2;

            ( divset (D,i)) c= I by A36, INTEGRA1: 8;

            then (t . i) in I by A46, A47, A48, A36;

            then

             A49: (t . i) in ( dom jauge2) by FUNCT_2:def 1;

            (x . i) <= ((t . i) + (jauge2 . (t . i))) by A36, A7, A9;

            then ((x . i) - (x . (i - 1))) <= (((t . i) + (jauge2 . (t . i))) - ((t . i) - (jauge2 . (t . i)))) by A44, XREAL_1: 13;

            then ((x . i) - (x . (i - 1))) <= (2 * (jauge2 . (t . i)));

            then ((x . i) - (x . (i - 1))) <= (2 * ((1 / 2) * (jauge . (t . i)))) by A49, VALUED_1:def 5;

            hence thesis by A38, INTEGRA1:def 5, A43;

          end;

        end;

      end;

      hence thesis;

    end;

    registration

      let I be non empty closed_interval Subset of REAL , jauge be positive-yielding Function of I, REAL ;

      cluster jauge -fine for tagged_division of I;

      existence by Th47;

    end