cousin2.miz



    begin

    reserve a,b,c,d,e for Real;

    theorem :: COUSIN2:1

    

     Th01: (a - b) <= c & b <= a implies |.(b - a).| <= c

    proof

      assume that

       A1: (a - b) <= c and

       A2: b <= a;

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

      then

       A3: 0 <= c by A1;

      (( - 1) * c) <= (( - 1) * (a - b)) by A1, XREAL_1: 65;

      then

       A5: ( - c) <= (b - a);

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

      hence thesis by ABSVALUE: 5, A5, A3;

    end;

    theorem :: COUSIN2:2

    

     Th02: (b - a) <= c & a <= b implies |.(b - a).| <= c

    proof

      assume that

       A1: (b - a) <= c and

       A2: a <= b;

      

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

      then ( - c) <= 0 by A1;

      hence thesis by A3, A1, ABSVALUE: 5;

    end;

    

     Lm01: a <= (b + c) & b <= d implies a <= (d + c)

    proof

      assume

       A1: a <= (b + c) & b <= d;

      then (b + c) <= (d + c) by XREAL_1: 7;

      hence thesis by A1, XXREAL_0: 2;

    end;

    

     Lm02: a < (b + c) & (b - c) < d implies (a - d) < (2 * c)

    proof

      assume that

       A1: a < (b + c) and

       A2: (b - c) < d;

      (a - d) < ((b + c) - (b - c)) by A1, A2, XREAL_1: 14;

      hence thesis;

    end;

    theorem :: COUSIN2:3

    

     Th03: a <= b <= c & |.(a - d).| <= e & |.(c - d).| <= e implies |.(b - d).| <= e

    proof

      assume that

       A1: a <= b <= c and

       A2: |.(a - d).| <= e and

       A3: |.(c - d).| <= e;

      b in [.a, c.] & a <= c by A1, XXREAL_1: 1, XXREAL_0: 2;

      then

      consider r be Real such that

       A4: 0 <= r & r <= 1 and

       A5: b = ((r * a) + ((1 - r) * c)) by SPRECT_1: 51;

      

       A6: |.((r * (a - d)) + ((1 - r) * (c - d))).| <= ( |.(r * (a - d)).| + |.((1 - r) * (c - d)).|) by COMPLEX1: 56;

       |.(r * (a - d)).| = ( |.r.| * |.(a - d).|) by COMPLEX1: 65

      .= (r * |.(a - d).|) by A4, ABSVALUE:def 1;

      then

       A7: |.(r * (a - d)).| <= (r * e) by A4, A2, XREAL_1: 64;

      

       A8: (r - r) <= (1 - r) by A4, XREAL_1: 9;

       |.((1 - r) * (c - d)).| = ( |.(1 - r).| * |.(c - d).|) by COMPLEX1: 65

      .= ((1 - r) * |.(c - d).|) by A8, ABSVALUE:def 1;

      then

       A9: |.((1 - r) * (c - d)).| <= ((1 - r) * e) by A8, A3, XREAL_1: 64;

       |.(b - d).| <= ((r * e) + |.((1 - r) * (c - d)).|) by A5, A6, A7, Lm01;

      then |.(b - d).| <= ((r * e) + ((1 - r) * e)) by A9, Lm01;

      hence thesis;

    end;

    theorem :: COUSIN2:4

    

     Th04: (for c st 0 < c holds |.(a - b).| <= c) implies a = b

    proof

      assume

       A1: for c st 0 < c holds |.(a - b).| <= c;

      assume a <> b;

      then

       A2: (a - b) <> 0 ;

      set e = ( |.(a - b).| / 2);

      (2 * e) <= e by A1;

      then ((2 * e) / e) <= (e / e) by XREAL_1: 72;

      then 2 <= (e / e) by A2, XCMPLX_1: 89;

      then 2 <= 1 by A2, XCMPLX_1: 60;

      hence contradiction;

    end;

    theorem :: COUSIN2:5

    

     Th05: for b,c,d be non negative Real st d < (e / ((2 * b) * |.c.|)) holds b is positive & c is positive

    proof

      let b,c,d be non negative Real;

      assume

       A1: d < (e / ((2 * b) * |.c.|));

      assume not (b is positive & c is positive);

      per cases ;

        suppose b <= 0 ;

        then ((2 * b) * |.c.|) = 0 ;

        hence contradiction by A1, XCMPLX_1: 49;

      end;

        suppose c <= 0 ;

        then |.c.| = 0 ;

        hence contradiction by A1, XCMPLX_1: 49;

      end;

    end;

    theorem :: COUSIN2:6

    

     Th06: a <> 0 implies (a * (b / (2 * a))) = (b / 2)

    proof

      assume

       A1: a <> 0 ;

      (a * (b / (2 * a))) = ((a * b) / (a * 2)) by XCMPLX_1: 74

      .= (((a / a) * b) / 2) by XCMPLX_1: 83

      .= ((1 * b) / 2) by A1, XCMPLX_1: 60;

      hence thesis;

    end;

    theorem :: COUSIN2:7

    

     Th07: for b,c,d be non negative Real st a <= ((b * c) * d) & d < (e / ((2 * b) * |.c.|)) holds a <= (e / 2)

    proof

      let b,c,d be non negative Real;

      assume that

       A1: a <= ((b * c) * d) and

       A2: d < (e / ((2 * b) * |.c.|));

      

       A3: 0 < b & 0 < c by A2, Th05;

      

       A4: ((b * c) * d) <= ((b * c) * (e / ((2 * b) * |.c.|))) by A2, XREAL_1: 64;

      ((b * c) * (e / ((2 * b) * |.c.|))) = ((b * c) * (e / ((2 * b) * c))) by ABSVALUE:def 1

      .= ((b * c) * (e / (2 * (b * c))))

      .= (e / 2) by A3, Th06;

      hence thesis by A4, A1, XXREAL_0: 2;

    end;

    begin

    definition

      let X be non empty set;

      let f,g be Function of X, REAL ;

      :: COUSIN2:def1

      func min (f,g) -> Function of X, REAL means

      : DEFM1: for x be Element of X holds (it . x) = ( min ((f . x),(g . x)));

      existence

      proof

        deffunc F( object) = ( min ((f . ( In ($1,X))),(g . ( In ($1,X)))));

        

         A1: for x be object st x in X holds F(x) in REAL by XREAL_0:def 1;

        consider h be Function of X, REAL such that

         A2: for x be object st x in X holds (h . x) = F(x) from FUNCT_2:sch 2( A1);

        take h;

        let x be Element of X;

        (h . x) = ( min ((f . x),(g . ( In (x,X))))) by A2

        .= ( min ((f . x),(g . x)));

        hence thesis;

      end;

      uniqueness

      proof

        let m1,m2 be Function of X, REAL such that

         A3: for x be Element of X holds (m1 . x) = ( min ((f . x),(g . x))) and

         A4: for x be Element of X holds (m2 . x) = ( min ((f . x),(g . x)));

        now

          ( dom m1) = X by PARTFUN1:def 2;

          hence ( dom m1) = ( dom m2) by PARTFUN1:def 2;

          hereby

            let x be object;

            assume x in ( dom m1);

            then

            reconsider y = x as Element of X;

            (m1 . x) = ( min ((f . y),(g . y))) by A3;

            hence (m1 . x) = (m2 . x) by A4;

          end;

        end;

        hence thesis;

      end;

      commutativity ;

      :: COUSIN2:def2

      func max (f,g) -> Function of X, REAL means

      : DEFM2: for x be Element of X holds (it . x) = ( max ((f . x),(g . x)));

      existence

      proof

        deffunc F( object) = ( max ((f . ( In ($1,X))),(g . ( In ($1,X)))));

        

         A1: for x be object st x in X holds F(x) in REAL by XREAL_0:def 1;

        consider h be Function of X, REAL such that

         A2: for x be object st x in X holds (h . x) = F(x) from FUNCT_2:sch 2( A1);

        take h;

        let x be Element of X;

        (h . x) = ( max ((f . x),(g . ( In (x,X))))) by A2

        .= ( max ((f . x),(g . x)));

        hence thesis;

      end;

      uniqueness

      proof

        let m1,m2 be Function of X, REAL such that

         A3: for x be Element of X holds (m1 . x) = ( max ((f . x),(g . x))) and

         A4: for x be Element of X holds (m2 . x) = ( max ((f . x),(g . x)));

        now

          ( dom m1) = X by PARTFUN1:def 2;

          hence ( dom m1) = ( dom m2) by PARTFUN1:def 2;

          hereby

            let x be object;

            assume x in ( dom m1);

            then

            reconsider y = x as Element of X;

            (m1 . x) = ( max ((f . y),(g . y))) by A3;

            hence (m1 . x) = (m2 . x) by A4;

          end;

        end;

        hence thesis;

      end;

      commutativity ;

    end

    registration

      let X be non empty set;

      let f,g be positive-yielding Function of X, REAL ;

      cluster ( min (f,g)) -> positive-yielding;

      coherence

      proof

        now

          let r be Real;

          assume r in ( rng ( min (f,g)));

          then

          consider x be object such that

           A1: x in X and

           A2: (( min (f,g)) . x) = r by FUNCT_2: 11;

          reconsider y = x as Element of X by A1;

          r = ( min ((f . y),(g . y))) by A2, DEFM1;

          then (r = (f . y)) or (r = (g . y)) by XXREAL_0: 15;

          then r in ( rng f) or r in ( rng g) by FUNCT_2: 4;

          hence 0 < r by PARTFUN3:def 1;

        end;

        hence thesis by PARTFUN3:def 1;

      end;

    end

    registration

      let X be non empty set;

      let f,g be positive-yielding Function of X, REAL ;

      cluster ( max (f,g)) -> positive-yielding;

      coherence

      proof

        now

          let r be Real;

          assume r in ( rng ( max (f,g)));

          then

          consider x be object such that

           A1: x in X and

           A2: (( max (f,g)) . x) = r by FUNCT_2: 11;

          reconsider y = x as Element of X by A1;

          r = ( max ((f . y),(g . y))) by A2, DEFM2;

          then (r = (f . y)) or (r = (g . y)) by XXREAL_0: 16;

          then r in ( rng f) or r in ( rng g) by FUNCT_2: 4;

          hence 0 < r by PARTFUN3:def 1;

        end;

        hence thesis by PARTFUN3:def 1;

      end;

    end

    definition

      let X be non empty set;

      let f,g be Function of X, REAL ;

      :: COUSIN2:def3

      pred f <= g means for x be Element of X holds (f . x) <= (g . x);

    end

    theorem :: COUSIN2:8

    

     Th08: for X be non empty set holds for f,g be Function of X, REAL holds ( min (f,g)) <= f

    proof

      let X be non empty set;

      let f,g be Function of X, REAL ;

      now

        let x be Element of X;

        (( min (f,g)) . x) = ( min ((f . x),(g . x))) by DEFM1;

        hence (( min (f,g)) . x) <= (f . x) & (( min (f,g)) . x) <= (g . x) by XXREAL_0: 17;

      end;

      hence thesis;

    end;

    

     Lm03: for X be non empty set st (ex s be object st (for r be object st r in X holds s = r)) holds ex r be object st X = {r}

    proof

      let X be non empty set;

      assume ex s be object st (for r be object st r in X holds s = r);

      then

      consider s0 be object such that

       A1: for r be object st r in X holds s0 = r;

      set r0 = the Element of X;

      take r0;

      thus X c= {r0}

      proof

        let x be object;

        assume

         A3: x in X;

        r0 = s0 by A1

        .= x by A1, A3;

        hence thesis by TARSKI:def 1;

      end;

      let x be object;

      assume x in {r0};

      then x = r0 by TARSKI:def 1;

      hence thesis;

    end;

    theorem :: COUSIN2:9

    

     Th09: for X be non empty real-membered set st (for r be Real st r in X holds ( upper_bound X) = r) holds ex r be Real st X = {r}

    proof

      let X be non empty real-membered set;

      assume

       A1: for r be Real st r in X holds ( upper_bound X) = r;

      ex s be object st (for x be object st x in X holds s = x)

      proof

        set s = ( upper_bound X);

        take s;

        thus thesis by A1;

      end;

      then

      consider r be object such that

       A2: X = {r} by Lm03;

      reconsider r0 = the Element of X as Real;

      take r0;

      thus thesis by A2, TARSKI:def 1;

    end;

    theorem :: COUSIN2:10

    for X be non empty real-membered set st (for r be Real st r in X holds ( lower_bound X) = r) holds ex r be Real st X = {r}

    proof

      let X be non empty real-membered set;

      assume

       A1: for r be Real st r in X holds ( lower_bound X) = r;

      ex s be object st (for x be object st x in X holds s = x)

      proof

        set s = ( lower_bound X);

        take s;

        thus thesis by A1;

      end;

      then

      consider r be object such that

       A2: X = {r} by Lm03;

      set r0 = the Element of X;

      take r0;

      thus thesis by A2, TARSKI:def 1;

    end;

    theorem :: COUSIN2:11

    

     Th10: for X be non empty bounded_below bounded_above real-membered set st ( upper_bound X) = ( lower_bound X) holds ex r be Real st X = {r}

    proof

      let X be non empty bounded_below bounded_above real-membered set;

      assume

       A1: ( upper_bound X) = ( lower_bound X);

      for r be Real st r in X holds ( upper_bound X) = r

      proof

        let r be Real;

        assume r in X;

        then ( upper_bound X) <= r & r <= ( upper_bound X) by A1, SEQ_4:def 1, SEQ_4:def 2;

        hence thesis by XXREAL_0: 1;

      end;

      hence thesis by Th09;

    end;

    begin

    reserve X,Y for set,

Z for non empty set,

r for Real,

s for ExtReal,

A for Subset of REAL ,

f for real-valued Function;

    theorem :: COUSIN2:12

    

     Th11: ( chi (X,Y)) is Function of Y, REAL

    proof

      ( { 0 , 1} = {} implies X = {} ) & { 0 , 1} c= REAL by INT_1: 3, NUMBERS: 19;

      hence thesis by FUNCT_2: 7;

    end;

    theorem :: COUSIN2:13

    A c= ].r, s.[ implies A is bounded_below

    proof

      assume

       A1: A c= ].r, s.[;

       ].r, s.[ c= [.r, s.[ by XXREAL_1: 22;

      then A c= [.r, s.[ by A1;

      hence thesis by XXREAL_2: 44;

    end;

    theorem :: COUSIN2:14

    A c= ].s, r.[ implies A is bounded_above

    proof

      assume

       A1: A c= ].s, r.[;

       ].s, r.[ c= ].s, r.] by XXREAL_1: 21;

      then A c= ].s, r.] by A1;

      hence thesis by XXREAL_2: 43;

    end;

    theorem :: COUSIN2:15

    

     Th12: ( rng f) c= [.a, b.] implies f is bounded

    proof

      assume

       A1: ( rng f) c= [.a, b.];

       [.a, b.] c= [.a, +infty .[ & [.a, b.] c= ]. -infty , b.] by XXREAL_1: 251, XXREAL_1: 265;

      then ( rng f) c= [.a, +infty .[ & ( rng f) c= ]. -infty , b.] by A1;

      then ( rng f) is bounded_below & ( rng f) is bounded_above by XXREAL_2: 43, XXREAL_2: 44;

      then f is bounded_below & f is bounded_above by INTEGRA1: 12, INTEGRA1: 14;

      hence thesis;

    end;

    theorem :: COUSIN2:16

    

     Th13: a <= b implies {a, b} c= [.a, b.]

    proof

      assume

       A1: a <= b;

      let x be object;

      assume x in {a, b};

      then x = a or x = b by TARSKI:def 2;

      hence thesis by A1, XXREAL_1: 1;

    end;

    theorem :: COUSIN2:17

    

     Th14: ( chi (X,Y)) is bounded

    proof

       { 0 , 1} c= [. 0 , 1.] by Th13;

      then ( rng ( chi (X,Y))) c= [. 0 , 1.];

      hence thesis by Th12;

    end;

    theorem :: COUSIN2:18

    

     Th15: X misses Y implies (for x be Element of X holds (( chi (Y,X)) . x) = 0 )

    proof

      assume

       A1: X misses Y;

      let x be Element of X;

      per cases ;

        suppose

         A2: X is non empty;

        then not x in Y by A1, XBOOLE_0:def 4;

        then x in (X \ Y) by A2, XBOOLE_0:def 5;

        hence thesis by FUNCT_3: 37;

      end;

        suppose X is empty;

        hence thesis;

      end;

    end;

    theorem :: COUSIN2:19

    

     Th16: for f be Function of Z, REAL holds (f is constant iff (ex r be Real st f = (r (#) ( chi (Z,Z)))))

    proof

      let f be Function of Z, REAL ;

      hereby

        assume

         A1: f is constant;

        set y = the Element of ( rng f);

        consider x be object such that

         A2: x in ( dom f) and

         A3: y = (f . x) by FUNCT_1:def 3;

        reconsider r = y as Real;

        take r;

        now

          

          thus

           A3BIS: ( dom (r (#) ( chi (Z,Z)))) = ( dom ( chi (Z,Z))) by VALUED_1:def 5

          .= Z by FUNCT_3:def 3

          .= ( dom f) by PARTFUN1:def 2;

          thus for z be object st z in ( dom f) holds (f . z) = ((r (#) ( chi (Z,Z))) . z)

          proof

            let z be object;

            assume

             A4: z in ( dom f);

            

            then ((r (#) ( chi (Z,Z))) . z) = (r * (( chi (Z,Z)) . z)) by A3BIS, VALUED_1:def 5

            .= (r * 1) by A4, FUNCT_3:def 3

            .= (f . z) by A3, A1, A4, A2;

            hence thesis;

          end;

        end;

        hence f = (r (#) ( chi (Z,Z)));

      end;

      assume ex r be Real st f = (r (#) ( chi (Z,Z)));

      then

      consider r be Real such that

       A5: f = (r (#) ( chi (Z,Z)));

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

      proof

        let x,y be object;

        assume that

         A6: x in ( dom f) and

         A7: y in ( dom f);

        (f . x) = (r * (( chi (Z,Z)) . x)) by A5, A6, VALUED_1:def 5

        .= (r * 1) by A6, FUNCT_3:def 3

        .= (r * (( chi (Z,Z)) . y)) by A7, FUNCT_3:def 3

        .= (f . y) by A5, A7, VALUED_1:def 5;

        hence thesis;

      end;

      hence f is constant;

    end;

    theorem :: COUSIN2:20

    

     Th17: ( chi (X,X)) is positive-yielding

    proof

      now

        let r be Real;

        assume

         A1: r in ( rng ( chi (X,X)));

        r <> 0

        proof

          assume

           A2: r = 0 ;

          ex s be Element of X st s in ( dom ( chi (X,X))) & r = (( chi (X,X)) . s) by A1, PARTFUN1: 3;

          hence contradiction by A2, FUNCT_3:def 3;

        end;

        hence 0 < r by A1;

      end;

      hence thesis by PARTFUN3:def 1;

    end;

    begin

    reserve I for non empty closed_interval Subset of REAL ,

TD for tagged_division of I,

D for Division of I,

T for Element of ( set_of_tagged_Division D),

f for PartFunc of I, REAL ;

    theorem :: COUSIN2:21

    

     Th18: f is lower_integrable implies ( lower_sum (f,D)) <= ( lower_integral f)

    proof

      assume f is lower_integrable;

      then

       A1: ( rng ( lower_sum_set f)) is bounded_above by INTEGRA1:def 13;

      set r = ( lower_integral f);

      r = ( upper_bound ( rng ( lower_sum_set f))) by INTEGRA1:def 15;

      then

       A2: for s be Real st s in ( rng ( lower_sum_set f)) holds s <= r by A1, SEQ_4:def 1;

      

       A3: ( dom ( lower_sum_set f)) = ( divs I) by PARTFUN1:def 2;

      D in ( divs I) by INTEGRA1:def 3;

      then (( lower_sum_set f) . D) <= r by A3, A2, FUNCT_1: 3;

      hence thesis by INTEGRA1:def 11;

    end;

    theorem :: COUSIN2:22

    

     Th19: f is upper_integrable implies ( upper_integral f) <= ( upper_sum (f,D))

    proof

      assume f is upper_integrable;

      then

       A1: ( rng ( upper_sum_set f)) is bounded_below by INTEGRA1:def 12;

      set r = ( upper_integral f);

      r = ( lower_bound ( rng ( upper_sum_set f))) by INTEGRA1:def 14;

      then

       A2: for s be Real st s in ( rng ( upper_sum_set f)) holds r <= s by A1, SEQ_4:def 2;

      

       A3: ( dom ( upper_sum_set f)) = ( divs I) by PARTFUN1:def 2;

      D in ( divs I) by INTEGRA1:def 3;

      then r <= (( upper_sum_set f) . D) by A3, A2, FUNCT_1: 3;

      hence thesis by INTEGRA1:def 10;

    end;

    definition

      let A be non empty closed_interval Subset of REAL ;

      :: COUSIN2:def4

      func tagged_divs A -> set means

      : Def1: for x be set holds (x in it iff x is tagged_division of A);

      existence

      proof

        defpred P[ set] means $1 is tagged_division of A;

        consider R be set such that

         A1: for x be set holds (x in R iff x in [:( bool [: NAT , REAL :]), ( REAL * ):] & P[x]) from XFAMILY:sch 1;

        take R;

        let x be set;

        thus x in R implies x is tagged_division of A by A1;

        assume x is tagged_division of A;

        then

        reconsider p = x as tagged_division of A;

        consider D be Division of A, T be Element of ( set_of_tagged_Division D) such that

         A2: p = [D, T] by COUSIN:def 3;

         [D, T] in [:( bool [: NAT , REAL :]), ( REAL * ):] by ZFMISC_1: 87;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        let D1,D2 be set such that

         A3: for x be set holds (x in D1 iff x is tagged_division of A) and

         A4: for x be set holds (x in D2 iff x is tagged_division of A);

        for x be object holds x in D1 iff x in D2 by A3, A4;

        hence thesis by TARSKI: 2;

      end;

    end

    registration

      let A be non empty closed_interval Subset of REAL ;

      cluster ( tagged_divs A) -> non empty;

      coherence

      proof

        reconsider TD = the tagged_division of A as set by TARSKI: 1;

        TD in ( tagged_divs A) by Def1;

        hence thesis;

      end;

    end

    definition

      let A be non empty closed_interval Subset of REAL ;

      let TD be tagged_division of A;

      :: COUSIN2:def5

      func tagged_of TD -> non empty non-decreasing FinSequence of REAL means

      : Def2: ex D be Division of A, T be Element of ( set_of_tagged_Division D) st it = T & TD = [D, T];

      existence

      proof

        consider D be Division of A, T be Element of ( set_of_tagged_Division D) such that

         A1: TD = [D, T] by COUSIN:def 3;

        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 COUSIN:def 2;

        hence thesis by A1;

      end;

      uniqueness by XTUPLE_0: 1;

    end

    theorem :: COUSIN2:23

    

     Th20: TD = [D, T] implies T = ( tagged_of TD) & D = ( division_of TD)

    proof

      assume

       A1: TD = [D, T];

      ex D1 be Division of I, T1 be Element of ( set_of_tagged_Division D1) st ( tagged_of TD) = T1 & TD = [D1, T1] by Def2;

      hence thesis by A1, XTUPLE_0: 1, COUSIN:def 6;

    end;

    theorem :: COUSIN2:24

    

     Th21: ( len ( tagged_of TD)) = ( len ( division_of TD))

    proof

      consider D be Division of I, T be Element of ( set_of_tagged_Division D) such that

       A1: TD = [D, T] by COUSIN:def 3;

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

       A2: T = s and

       A3: ( dom s) = ( dom D) and for i be Nat st i in ( dom s) holds (s . i) in ( divset (D,i)) by COUSIN:def 2;

      ( tagged_of TD) = T & ( division_of TD) = D by A1, Th20;

      hence thesis by A2, A3, FINSEQ_3: 29;

    end;

    definition

      let A be non empty closed_interval Subset of REAL ;

      let TD be tagged_division of A;

      :: COUSIN2:def6

      func len TD -> Element of NAT equals ( len ( division_of TD));

      coherence ;

      :: COUSIN2:def7

      func dom TD -> set equals ( dom ( division_of TD));

      coherence ;

    end

    theorem :: COUSIN2:25

    

     Th22: 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= I

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

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

       A1: T = s & ( dom s) = ( dom D) & for i be Nat st i in ( dom s) holds (s . i) in ( divset (D,i)) by COUSIN:def 2;

      now

        let x be object;

        assume x in ( rng T);

        then

        consider y be object such that

         A2: y in ( dom T) and

         A3: x = (T . y) by FUNCT_1:def 3;

        reconsider y as Nat by A2;

        ( divset (D,y)) c= I by A1, A2, INTEGRA1: 8;

        hence x in I by A3, A1, A2;

      end;

      hence thesis;

    end;

    theorem :: COUSIN2:26

    

     Th23: for I be non empty closed_interval Subset of REAL holds for jauge1,jauge2 be positive-yielding Function of I, REAL holds for TD be jauge1 -fine tagged_division of I st jauge1 <= jauge2 holds TD is jauge2 -fine tagged_division of I

    proof

      let I be non empty closed_interval Subset of REAL ;

      let jauge1,jauge2 be positive-yielding Function of I, REAL ;

      let TD be jauge1 -fine tagged_division of I;

      assume

       A1: jauge1 <= jauge2;

      consider D be Division of I, T be Element of ( set_of_tagged_Division D) such that

       A2: TD = [D, T] and

       A3: for i be Nat st i in ( dom D) holds ( vol ( divset (D,i))) <= (jauge1 . (T . i)) by COUSIN:def 4;

      now

        let i be Nat;

        assume

         A4: i in ( dom D);

        then

         A5: ( vol ( divset (D,i))) <= (jauge1 . (T . i)) by A3;

        ( dom T) = ( Seg ( len T)) by FINSEQ_1:def 3

        .= ( Seg ( len ( tagged_of TD))) by A2, Th20

        .= ( Seg ( len ( division_of TD))) by Th21

        .= ( Seg ( len D)) by A2, Th20

        .= ( dom D) by FINSEQ_1:def 3;

        then

         A6: (T . i) in ( rng T) by A4, FUNCT_1: 3;

        ( rng T) c= I by Th22;

        then (jauge1 . (T . i)) <= (jauge2 . (T . i)) by A6, A1;

        hence ( vol ( divset (D,i))) <= (jauge2 . (T . i)) by A5, XXREAL_0: 2;

      end;

      hence thesis by A2, COUSIN:def 4;

    end;

    begin

    definition

      let I be non empty closed_interval Subset of REAL ;

      let f be PartFunc of I, REAL ;

      let TD be tagged_division of I;

      :: COUSIN2:def8

      func tagged_volume (f,TD) -> FinSequence of REAL means

      : Def4: ( len it ) = ( len TD) & for i be Nat st i in ( dom TD) holds (it . i) = ((f . (( tagged_of TD) . i)) * ( vol ( divset (( division_of TD),i))));

      existence

      proof

        deffunc F( Nat) = ( In (((f . (( tagged_of TD) . $1)) * ( vol ( divset (( division_of TD),$1)))), REAL ));

        consider IT be FinSequence of REAL such that

         A1: ( len IT) = ( len ( division_of TD)) & for i be Nat st i in ( dom IT) holds (IT . i) = F(i) from FINSEQ_2:sch 1;

        take IT;

        thus ( len IT) = ( len TD) by A1;

        let i be Nat;

        

         A2: F(i) = ((f . (( tagged_of TD) . i)) * ( vol ( divset (( division_of TD),i))));

        assume i in ( dom TD);

        then i in ( Seg ( len ( division_of TD))) by FINSEQ_1:def 3;

        then i in ( dom IT) by A1, FINSEQ_1:def 3;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        let s1,s2 be FinSequence of REAL such that

         A3: ( len s1) = ( len TD) and

         A4: for i be Nat st i in ( dom TD) holds (s1 . i) = ((f . (( tagged_of TD) . i)) * ( vol ( divset (( division_of TD),i)))) and

         A5: ( len s2) = ( len TD) and

         A6: for i be Nat st i in ( dom TD) holds (s2 . i) = ((f . (( tagged_of TD) . i)) * ( vol ( divset (( division_of TD),i))));

        

         A7: ( dom s1) = ( dom TD) by A3, FINSEQ_3: 29;

        for i be Nat st i in ( dom s1) holds (s1 . i) = (s2 . i)

        proof

          let i be Nat;

          assume

           A8: i in ( dom s1);

          then (s1 . i) = ((f . (( tagged_of TD) . i)) * ( vol ( divset (( division_of TD),i)))) by A4, A7;

          hence thesis by A6, A7, A8;

        end;

        hence thesis by A3, A5, FINSEQ_2: 9;

      end;

    end

    definition

      let I be non empty closed_interval Subset of REAL ;

      let f be PartFunc of I, REAL ;

      let TD be tagged_division of I;

      :: COUSIN2:def9

      func tagged_sum (f,TD) -> Real equals ( Sum ( tagged_volume (f,TD)));

      coherence ;

    end

    theorem :: COUSIN2:27

    

     Th24: Y c= X implies ( chi (X,Y)) = ( chi (Y,Y))

    proof

      assume

       A1: Y c= X;

      now

        

        thus ( dom ( chi (X,Y))) = Y by FUNCT_3:def 3

        .= ( dom ( chi (Y,Y))) by FUNCT_3:def 3;

        hereby

          let x be object;

          assume

           A2: x in ( dom ( chi (X,Y)));

          then x in Y & x in X by A1;

          

          hence (( chi (X,Y)) . x) = 1 by FUNCT_3:def 3

          .= (( chi (Y,Y)) . x) by A2, FUNCT_3:def 3;

        end;

      end;

      hence thesis;

    end;

    reserve f for Function of I, REAL ;

    theorem :: COUSIN2:28

    

     Th25: I is non empty trivial implies ( vol I) = 0

    proof

      assume I is non empty trivial;

      then

      consider x be object such that

       A1: I = {x} by ZFMISC_1: 131;

      x in I by A1, TARSKI:def 1;

      then

      reconsider x as Real;

      ( vol {x}) = 0 by COUSIN: 41;

      hence thesis by A1;

    end;

    theorem :: COUSIN2:29

    

     Th26: for r be Real st I = {r} holds (for D be Division of I holds D = <*r*>)

    proof

      let r be Real;

      assume

       A1: I = {r};

      

       A2: I = [.r, r.] by A1, XXREAL_1: 17;

      let D be Division of I;

      ( len D) = 1

      proof

        assume 1 <> ( len D);

        then 2 <= ( len D) by NAT_1: 23;

        then 1 <= ( len D) & 1 <= 2 <= ( len D) by XXREAL_0: 2;

        then

         A3: 1 in ( dom D) & 2 in ( dom D) by FINSEQ_3: 25;

        then (D . 1) in I & (D . 2) in I by INTEGRA1: 6;

        then (D . 1) = r & (D . 2) = r by A1, TARSKI:def 1;

        hence contradiction by A3, VALUED_0:def 13;

      end;

      hence thesis by A2, COUSIN: 64;

    end;

    

     Lm04: f = ( chi (I,I)) implies ( tagged_sum (f,TD)) = ( vol I)

    proof

      assume

       A1: f = ( chi (I,I));

      

       A2: for i be Nat st i in ( dom TD) holds (( tagged_volume (f,TD)) . i) = ( vol ( divset (( division_of TD),i)))

      proof

        let i be Nat;

        assume

         A3: i in ( dom TD);

        consider D be Division of I, T be Element of ( set_of_tagged_Division D) such that

         A4: ( tagged_of TD) = T and

         A5: TD = [D, T] by Def2;

        

         A6: i in ( dom D) by A3, Th20, A5;

        

         A7: ( dom T) = ( Seg ( len ( tagged_of TD))) by A4, FINSEQ_1:def 3

        .= ( Seg ( len ( division_of TD))) by Th21

        .= ( Seg ( len D)) by A5, Th20

        .= ( dom D) by FINSEQ_1:def 3;

        ( rng T) c= I by Th22;

        then (T . i) in I by A7, A6, FUNCT_1: 3;

        then (f . (( tagged_of TD) . i)) = 1 by A4, A1, FUNCT_3:def 3;

        

        then (( tagged_volume (f,TD)) . i) = (1 * ( vol ( divset (( division_of TD),i)))) by Def4, A3

        .= ( vol ( divset (( division_of TD),i)));

        hence thesis;

      end;

      

       T1: ( dom ( tagged_volume (f,TD))) = ( Seg ( len ( tagged_volume (f,TD)))) by FINSEQ_1:def 3

      .= ( Seg ( len TD)) by Def4

      .= ( Seg ( len ( division_of TD)));

      ( Seg ( len ( division_of TD))) = ( dom ( division_of TD)) by FINSEQ_1:def 3;

      hence thesis by INTEGR20: 6, T1, A2;

    end;

    definition

      let I be non empty closed_interval Subset of REAL ;

      let f be Function of I, REAL ;

      :: COUSIN2:def10

      attr f is HK-integrable means ex J be Real st for epsilon be Real st epsilon > 0 holds ex jauge be positive-yielding Function of I, REAL st for TD be tagged_division of I st TD is jauge -fine holds |.(( tagged_sum (f,TD)) - J).| <= epsilon;

    end

    definition

      let I be non empty closed_interval Subset of REAL ;

      let f be Function of I, REAL ;

      assume

       A1: f is HK-integrable;

      :: COUSIN2:def11

      func HK-integral f -> Real means

      : DEFCC: for epsilon be Real st epsilon > 0 holds ex jauge be positive-yielding Function of I, REAL st for TD be tagged_division of I st TD is jauge -fine holds |.(( tagged_sum (f,TD)) - it ).| <= epsilon;

      existence by A1;

      uniqueness

      proof

        let J1,J2 be Real such that

         A2: for epsilon be Real st epsilon > 0 holds ex jauge be positive-yielding Function of I, REAL st for TD be tagged_division of I st TD is jauge -fine holds |.(( tagged_sum (f,TD)) - J1).| <= epsilon and

         A3: for epsilon be Real st epsilon > 0 holds ex jauge be positive-yielding Function of I, REAL st for TD be tagged_division of I st TD is jauge -fine holds |.(( tagged_sum (f,TD)) - J2).| <= epsilon;

        now

          let epsilon be Real;

          assume

           A4: epsilon > 0 ;

          reconsider e = (epsilon / 2) as Real;

          consider jauge1 be positive-yielding Function of I, REAL such that

           A5: for TD be tagged_division of I st TD is jauge1 -fine holds |.(( tagged_sum (f,TD)) - J1).| <= e by A4, A2;

          consider jauge2 be positive-yielding Function of I, REAL such that

           A6: for TD be tagged_division of I st TD is jauge2 -fine holds |.(( tagged_sum (f,TD)) - J2).| <= e by A3, A4;

          reconsider jauge = ( min (jauge1,jauge2)) as positive-yielding Function of I, REAL ;

          consider TD be tagged_division of I such that

           A7: TD is jauge -fine by COUSIN: 68;

          TD is jauge1 -fine & TD is jauge2 -fine by A7, Th23, Th08;

          then |.(( tagged_sum (f,TD)) - J1).| <= e & |.(( tagged_sum (f,TD)) - J2).| <= e by A5, A6;

          then

           A8: |.(J1 - ( tagged_sum (f,TD))).| <= e & |.(J2 - ( tagged_sum (f,TD))).| <= e by COMPLEX1: 60;

           |.((J1 - ( tagged_sum (f,TD))) - (J2 - ( tagged_sum (f,TD)))).| <= ( |.(J1 - ( tagged_sum (f,TD))).| + |.(J2 - ( tagged_sum (f,TD))).|) by COMPLEX1: 57;

          then |.(J1 - J2).| <= (e + |.(J2 - ( tagged_sum (f,TD))).|) by A8, Lm01;

          then |.(J1 - J2).| <= (e + e) by A8, Lm01;

          hence |.(J1 - J2).| <= epsilon;

        end;

        hence thesis by Th04;

      end;

    end

    theorem :: COUSIN2:30

    

     Th27: for f be Function of I, REAL st I is trivial holds f is HK-integrable & ( HK-integral f) = 0

    proof

      let f be Function of I, REAL ;

      assume

       A1: I is trivial;

      reconsider J = 0 as Real;

       A2:

      now

        let epsilon be Real;

        assume

         A3: epsilon > 0 ;

        reconsider jauge = ( chi (I,I)) as positive-yielding Function of I, REAL by Th17, Th11;

        take jauge;

        thus for TD be tagged_division of I st TD is jauge -fine holds |.(( tagged_sum (f,TD)) - J).| <= epsilon

        proof

          let TD be tagged_division of I;

          assume TD is jauge -fine;

          consider x be object such that

           A4: I = {x} by A1, ZFMISC_1: 131;

          x in I by A4, TARSKI:def 1;

          then

          reconsider x as Real;

          

           A4Bis: ( division_of TD) = <*x*> by A4, Th26;

          

           A5: ( len ( tagged_volume (f,TD))) = ( len TD) & for i be Nat st i in ( dom TD) holds (( tagged_volume (f,TD)) . i) = ((f . (( tagged_of TD) . i)) * ( vol ( divset (( division_of TD),i)))) by Def4;

          

           A6: (( tagged_volume (f,TD)) . 1) = ((f . (( tagged_of TD) . 1)) * ( vol ( divset (( division_of TD),1)))) by A5, FINSEQ_5: 6;

          ( divset (( division_of TD),1)) = [.( lower_bound I), (( division_of TD) . 1).] by COUSIN: 50

          .= [.x, (( division_of TD) . 1).] by A4, SEQ_4: 9

          .= [.x, x.] by A4Bis, FINSEQ_1: 40

          .= {x} by XXREAL_1: 17;

          then

           A7: ( vol ( divset (( division_of TD),1))) = 0 by COUSIN: 41;

          ( len ( tagged_volume (f,TD))) = ( len TD) by Def4

          .= 1 by A4Bis, FINSEQ_1: 40;

          then ( tagged_volume (f,TD)) = <*(( tagged_volume (f,TD)) . 1)*> by FINSEQ_1: 40;

          then ( Sum ( tagged_volume (f,TD))) = 0 by A6, A7, RVSUM_1: 73;

          hence thesis by A3;

        end;

      end;

      then f is HK-integrable;

      hence thesis by A2, DEFCC;

    end;

    theorem :: COUSIN2:31

    

     Th28: A misses I & f = ( chi (A,I)) implies ( tagged_sum (f,TD)) = 0

    proof

      assume that

       A1: A misses I and

       A2: f = ( chi (A,I));

      

       A3: ( dom ( tagged_volume (f,TD))) = ( Seg ( len ( tagged_volume (f,TD)))) by FINSEQ_1:def 3

      .= ( Seg ( len TD)) by Def4

      .= ( dom TD) by FINSEQ_1:def 3;

      for i be Nat st i in ( dom TD) holds (( tagged_volume (f,TD)) . i) = 0

      proof

        let i be Nat;

        assume

         A4: i in ( dom TD);

        consider D be Division of I, T be Element of ( set_of_tagged_Division D) such that

         A5: ( tagged_of TD) = T and

         A6: TD = [D, T] by Def2;

        

         A7: i in ( dom D) by A4, Th20, A6;

        

         A8: ( dom T) = ( Seg ( len ( tagged_of TD))) by A5, FINSEQ_1:def 3

        .= ( Seg ( len ( division_of TD))) by Th21

        .= ( Seg ( len D)) by A6, Th20

        .= ( dom D) by FINSEQ_1:def 3;

        ( rng T) c= I by Th22;

        then (T . i) in I by A8, A7, FUNCT_1: 3;

        then (f . (( tagged_of TD) . i)) = 0 by A1, A5, A2, Th15;

        

        then (( tagged_volume (f,TD)) . i) = ( 0 * ( vol ( divset (( division_of TD),i)))) by Def4, A4

        .= 0 ;

        hence thesis;

      end;

      then for k be object st k in ( dom ( tagged_volume (f,TD))) holds (( tagged_volume (f,TD)) . k) = 0 by A3;

      

      then ( Sum ( tagged_volume (f,TD))) = ( Sum (( len ( tagged_volume (f,TD))) |-> 0 )) by INTEGR23: 5

      .= 0 by RVSUM_1: 81;

      hence thesis;

    end;

    theorem :: COUSIN2:32

    

     Th29: A misses I & f = ( chi (A,I)) implies f is HK-integrable & ( HK-integral f) = 0

    proof

      assume that

       A1: A misses I and

       A2: f = ( chi (A,I));

      reconsider J = 0 as Real;

       A3:

      now

        let epsilon be Real;

        assume

         A4: epsilon > 0 ;

        reconsider jauge = ( chi (I,I)) as Function of I, REAL by Th11;

        now

          let r be Real;

          assume r in ( rng jauge);

          then r in {1} by INTEGRA1: 17;

          hence 0 < r;

        end;

        then

        reconsider jauge as positive-yielding Function of I, REAL by PARTFUN3:def 1;

        now

          take jauge;

          hereby

            let TD be tagged_division of I;

            assume TD is jauge -fine;

             |.(( tagged_sum (f,TD)) - J).| = |. 0 .| by A1, A2, Th28

            .= 0 ;

            hence |.(( tagged_sum (f,TD)) - J).| <= epsilon by A4;

          end;

        end;

        hence ex jauge be positive-yielding Function of I, REAL st for TD be tagged_division of I st TD is jauge -fine holds |.(( tagged_sum (f,TD)) - J).| <= epsilon;

      end;

      then f is HK-integrable;

      hence thesis by A3, DEFCC;

    end;

    theorem :: COUSIN2:33

    

     Th30: I c= A & f = ( chi (A,I)) implies f is HK-integrable & ( HK-integral f) = ( vol I)

    proof

      assume that

       A1: I c= A and

       A2: f = ( chi (A,I));

      reconsider J = ( vol I) as Real;

       A3:

      now

        let epsilon be Real;

        assume

         A4: epsilon > 0 ;

        reconsider jauge = ( chi (I,I)) as Function of I, REAL by Th11;

        now

          let r be Real;

          assume r in ( rng jauge);

          then r in {1} by INTEGRA1: 17;

          hence 0 < r;

        end;

        then

        reconsider jauge as positive-yielding Function of I, REAL by PARTFUN3:def 1;

        now

          take jauge;

          hereby

            let TD be tagged_division of I;

            assume TD is jauge -fine;

            f = ( chi (I,I)) by A1, A2, Th24;

            then ( tagged_sum (f,TD)) = ( vol I) by Lm04;

            hence |.(( tagged_sum (f,TD)) - J).| <= epsilon by A4;

          end;

        end;

        hence ex jauge be positive-yielding Function of I, REAL st for TD be tagged_division of I st TD is jauge -fine holds |.(( tagged_sum (f,TD)) - J).| <= epsilon;

      end;

      then f is HK-integrable;

      hence thesis by A3, DEFCC;

    end;

    registration

      let I be non empty closed_interval Subset of REAL ;

      cluster HK-integrable for Function of I, REAL ;

      existence

      proof

        reconsider f = ( chi (( REAL \ I),I)) as Function of I, REAL by Th11;

        take f;

        ( REAL \ I) misses I by XBOOLE_1: 79;

        hence f is HK-integrable by Th29;

      end;

    end

    begin

    reserve f,g for HK-integrable Function of I, REAL ,

r for Real;

    theorem :: COUSIN2:34

    

     Th31: for i be Nat st i in ( dom TD) holds (( tagged_volume ((r (#) f),TD)) . i) = ((r * (f . (( tagged_of TD) . i))) * ( vol ( divset (( division_of TD),i))))

    proof

      let i be Nat;

      assume i in ( dom TD);

      then (( tagged_volume ((r (#) f),TD)) . i) = (((r (#) f) . (( tagged_of TD) . i)) * ( vol ( divset (( division_of TD),i)))) by Def4;

      hence thesis by VALUED_1: 6;

    end;

    theorem :: COUSIN2:35

    

     Th32: ( tagged_volume ((r (#) f),TD)) = (r * ( tagged_volume (f,TD)))

    proof

      

       Z1: ( len (r * ( tagged_volume (f,TD)))) = ( len ( tagged_volume (f,TD))) by RVSUM_1: 117

      .= ( len TD) by Def4

      .= ( len ( tagged_volume ((r (#) f),TD))) by Def4;

      for i be Nat st i in ( dom ( tagged_volume ((r (#) f),TD))) holds (( tagged_volume ((r (#) f),TD)) . i) = ((r * ( tagged_volume (f,TD))) . i)

      proof

        let i be Nat;

        assume i in ( dom ( tagged_volume ((r (#) f),TD)));

        then i in ( Seg ( len ( tagged_volume ((r (#) f),TD)))) by FINSEQ_1:def 3;

        then i in ( Seg ( len TD)) by Def4;

        then

         A1: i in ( dom TD) by FINSEQ_1:def 3;

        

        then (( tagged_volume ((r (#) f),TD)) . i) = ((r * (f . (( tagged_of TD) . i))) * ( vol ( divset (( division_of TD),i)))) by Th31

        .= (r * ((f . (( tagged_of TD) . i)) * ( vol ( divset (( division_of TD),i)))))

        .= (r * (( tagged_volume (f,TD)) . i)) by A1, Def4;

        hence thesis by RVSUM_1: 45;

      end;

      hence thesis by FINSEQ_2: 9, Z1;

    end;

    theorem :: COUSIN2:36

    

     Th33: for i be Nat st i in ( dom TD) holds (( tagged_volume ((f + g),TD)) . i) = (((f . (( tagged_of TD) . i)) * ( vol ( divset (( division_of TD),i)))) + ((g . (( tagged_of TD) . i)) * ( vol ( divset (( division_of TD),i)))))

    proof

      let i be Nat;

      assume

       A1: i in ( dom TD);

      consider D be Division of I, T be Element of ( set_of_tagged_Division D) such that

       A2: ( tagged_of TD) = T and

       A3: TD = [D, T] by Def2;

      

       A4: i in ( dom D) by A1, Th20, A3;

      

       A5: ( dom T) = ( Seg ( len ( tagged_of TD))) by A2, FINSEQ_1:def 3

      .= ( Seg ( len ( division_of TD))) by Th21

      .= ( Seg ( len D)) by A3, Th20

      .= ( dom D) by FINSEQ_1:def 3;

      ( rng T) c= I by Th22;

      then

      reconsider c = (( tagged_of TD) . i) as Element of I by A2, A4, A5, FUNCT_1: 3;

      (( tagged_volume ((f + g),TD)) . i) = (((f + g) . c) * ( vol ( divset (( division_of TD),i)))) by A1, Def4

      .= (((f . c) + (g . c)) * ( vol ( divset (( division_of TD),i)))) by VALUED_1: 1;

      hence thesis;

    end;

    theorem :: COUSIN2:37

    

     Th34: ( tagged_volume ((f + g),TD)) = (( tagged_volume (f,TD)) + ( tagged_volume (g,TD)))

    proof

      ( len ( tagged_volume (f,TD))) = ( len TD) & ( len ( tagged_volume (g,TD))) = ( len TD) by Def4;

      then

      reconsider R1 = ( tagged_volume (f,TD)), R2 = ( tagged_volume (g,TD)) as Element of (( len TD) -tuples_on REAL ) by FINSEQ_2: 92;

      ( len ( tagged_volume (f,TD))) = ( len TD) by Def4

      .= ( len ( tagged_volume (g,TD))) by Def4;

      

      then

       Z1: ( len (( tagged_volume (f,TD)) + ( tagged_volume (g,TD)))) = ( len ( tagged_volume (f,TD))) by RVSUM_1: 115

      .= ( len TD) by Def4

      .= ( len ( tagged_volume ((f + g),TD))) by Def4;

      for i be Nat st i in ( dom ( tagged_volume ((f + g),TD))) holds (( tagged_volume ((f + g),TD)) . i) = ((( tagged_volume (f,TD)) + ( tagged_volume (g,TD))) . i)

      proof

        let i be Nat;

        assume i in ( dom ( tagged_volume ((f + g),TD)));

        then i in ( Seg ( len ( tagged_volume ((f + g),TD)))) by FINSEQ_1:def 3;

        then i in ( Seg ( len TD)) by Def4;

        then

         A1: i in ( dom TD) by FINSEQ_1:def 3;

        

        then (( tagged_volume ((f + g),TD)) . i) = (((f . (( tagged_of TD) . i)) * ( vol ( divset (( division_of TD),i)))) + ((g . (( tagged_of TD) . i)) * ( vol ( divset (( division_of TD),i))))) by Th33

        .= ((( tagged_volume (f,TD)) . i) + ((g . (( tagged_of TD) . i)) * ( vol ( divset (( division_of TD),i))))) by A1, Def4

        .= ((R1 . i) + (R2 . i)) by A1, Def4

        .= ((( tagged_volume (f,TD)) + ( tagged_volume (g,TD))) . i) by RVSUM_1: 11;

        hence thesis;

      end;

      hence thesis by FINSEQ_2: 9, Z1;

    end;

    theorem :: COUSIN2:38

    

     Th35: f is HK-integrable implies (r (#) f) is HK-integrable Function of I, REAL & ( HK-integral (r (#) f)) = (r * ( HK-integral f))

    proof

      assume f is HK-integrable;

      then

      consider J be Real such that

       A1: for epsilon be Real st epsilon > 0 holds ex jauge be positive-yielding Function of I, REAL st for TD be tagged_division of I st TD is jauge -fine holds |.(( tagged_sum (f,TD)) - J).| <= epsilon;

      

       A2: for epsilon be Real st epsilon > 0 holds ex jauge be positive-yielding Function of I, REAL st for TD be tagged_division of I st TD is jauge -fine holds |.(( tagged_sum ((r (#) f),TD)) - (r * J)).| <= epsilon

      proof

        per cases ;

          suppose

           A3: r = 0 ;

          let epsilon be Real;

          assume

           A4: epsilon > 0 ;

          set jauge = the positive-yielding Function of I, REAL ;

          take jauge;

          for TD be tagged_division of I st TD is jauge -fine holds |.(( tagged_sum ((r (#) f),TD)) - (r * J)).| <= epsilon

          proof

            let TD be tagged_division of I;

            assume TD is jauge -fine;

            ( tagged_sum ((r (#) f),TD)) = ( Sum (r * ( tagged_volume (f,TD)))) by Th32

            .= (r * ( Sum ( tagged_volume (f,TD)))) by RVSUM_1: 87

            .= 0 by A3;

            hence |.(( tagged_sum ((r (#) f),TD)) - (r * J)).| <= epsilon by A3, A4;

          end;

          hence thesis;

        end;

          suppose

           A5: r <> 0 ;

          let epsilon be Real;

          assume

           A6: epsilon > 0 ;

          set e = (epsilon / |.r.|);

          consider jauge be positive-yielding Function of I, REAL such that

           A7: for TD be tagged_division of I st TD is jauge -fine holds |.(( tagged_sum (f,TD)) - J).| <= e by A1, A5, A6;

          take jauge;

          for TD be tagged_division of I st TD is jauge -fine holds |.(( tagged_sum ((r (#) f),TD)) - (r * J)).| <= epsilon

          proof

            let TD be tagged_division of I;

            assume

             A8: TD is jauge -fine;

             |.((r * ( tagged_sum (f,TD))) - (r * J)).| = |.(r * (( tagged_sum (f,TD)) - J)).|

            .= ( |.r.| * |.(( tagged_sum (f,TD)) - J).|) by COMPLEX1: 65;

            then

             z1: |.((r * ( tagged_sum (f,TD))) - (r * J)).| <= ( |.r.| * e) by A7, A8, XREAL_1: 64;

            ( tagged_sum ((r (#) f),TD)) = ( Sum (r * ( tagged_volume (f,TD)))) by Th32

            .= (r * ( tagged_sum (f,TD))) by RVSUM_1: 87;

            hence thesis by z1, A5, XCMPLX_1: 87;

          end;

          hence thesis;

        end;

      end;

      then

       A9: (r (#) f) is HK-integrable;

      

      then ( HK-integral (r (#) f)) = (r * J) by A2, DEFCC

      .= (r * ( HK-integral f)) by A1, DEFCC;

      hence thesis by A9;

    end;

    theorem :: COUSIN2:39

    (f + g) is HK-integrable Function of I, REAL & ( HK-integral (f + g)) = (( HK-integral f) + ( HK-integral g))

    proof

      f is HK-integrable;

      then

      consider J1 be Real such that

       A1: for epsilon be Real st epsilon > 0 holds ex jauge be positive-yielding Function of I, REAL st for TD be tagged_division of I st TD is jauge -fine holds |.(( tagged_sum (f,TD)) - J1).| <= epsilon;

      g is HK-integrable;

      then

      consider J2 be Real such that

       A2: for epsilon be Real st epsilon > 0 holds ex jauge be positive-yielding Function of I, REAL st for TD be tagged_division of I st TD is jauge -fine holds |.(( tagged_sum (g,TD)) - J2).| <= epsilon;

      

       A3: ( HK-integral g) = J2 by A2, DEFCC;

      

       A4: for epsilon be Real st epsilon > 0 holds ex jauge be positive-yielding Function of I, REAL st for TD be tagged_division of I st TD is jauge -fine holds |.(( tagged_sum ((f + g),TD)) - (J1 + J2)).| <= epsilon

      proof

        let epsilon be Real;

        assume

         A5: epsilon > 0 ;

        set e = (epsilon / 2);

        consider jauge1 be positive-yielding Function of I, REAL such that

         A6: for TD be tagged_division of I st TD is jauge1 -fine holds |.(( tagged_sum (f,TD)) - J1).| <= (epsilon / 2) by A5, A1;

        consider jauge2 be positive-yielding Function of I, REAL such that

         A7: for TD be tagged_division of I st TD is jauge2 -fine holds |.(( tagged_sum (g,TD)) - J2).| <= (epsilon / 2) by A5, A2;

        reconsider jauge = ( min (jauge1,jauge2)) as positive-yielding Function of I, REAL ;

        ex jauge be positive-yielding Function of I, REAL st for TD be tagged_division of I st TD is jauge -fine holds |.(( tagged_sum ((f + g),TD)) - (J1 + J2)).| <= epsilon

        proof

          take jauge;

          for TD be tagged_division of I st TD is jauge -fine holds |.(( tagged_sum ((f + g),TD)) - (J1 + J2)).| <= epsilon

          proof

            let TD be tagged_division of I;

            assume TD is jauge -fine;

            then

             A8: TD is jauge1 -fine & TD is jauge2 -fine by Th23, Th08;

            ( len ( tagged_volume (f,TD))) = ( len TD) & ( len ( tagged_volume (g,TD))) = ( len TD) by Def4;

            then

            reconsider R1 = ( tagged_volume (f,TD)), R2 = ( tagged_volume (g,TD)) as Element of (( len TD) -tuples_on REAL ) by FINSEQ_2: 92;

            ( tagged_sum ((f + g),TD)) = ( Sum (( tagged_volume (f,TD)) + ( tagged_volume (g,TD)))) by Th34

            .= (( Sum R1) + ( Sum R2)) by RVSUM_1: 89

            .= (( tagged_sum (f,TD)) + ( tagged_sum (g,TD)));

            then (( tagged_sum ((f + g),TD)) - (J1 + J2)) = ((( tagged_sum (f,TD)) - J1) + (( tagged_sum (g,TD)) - J2));

            then |.(( tagged_sum ((f + g),TD)) - (J1 + J2)).| <= ( |.(( tagged_sum (f,TD)) - J1).| + |.(( tagged_sum (g,TD)) - J2).|) by COMPLEX1: 56;

            then |.(( tagged_sum ((f + g),TD)) - (J1 + J2)).| <= ((epsilon / 2) + |.(( tagged_sum (g,TD)) - J2).|) by A8, A6, Lm01;

            then |.(( tagged_sum ((f + g),TD)) - (J1 + J2)).| <= ((epsilon / 2) + (epsilon / 2)) by A8, A7, Lm01;

            hence thesis;

          end;

          hence thesis;

        end;

        hence thesis;

      end;

      then

       A9: (f + g) is HK-integrable;

      

      then ( HK-integral (f + g)) = (J1 + J2) by A4, DEFCC

      .= (( HK-integral f) + ( HK-integral g)) by A1, DEFCC, A3;

      hence thesis by A9;

    end;

    theorem :: COUSIN2:40

    

     Th36: for f be Function of I, REAL st f is constant holds (f is HK-integrable & ex r be Real st f = (r (#) ( chi (I,I))) & ( HK-integral f) = (r * ( vol I)))

    proof

      let f be Function of I, REAL ;

      assume f is constant;

      then

      consider r be Real such that

       A1: f = (r (#) ( chi (I,I))) by Th16;

      reconsider g = ( chi (I,I)) as Function of I, REAL by Th11;

      

       A2: g is HK-integrable & ( HK-integral g) = ( vol I) by Th30;

      hence f is HK-integrable by A1, Th35;

      take r;

      thus thesis by A1, A2, Th35;

    end;

    begin

    registration

      let I be non empty closed_interval Subset of REAL ;

      cluster integrable for Function of I, REAL ;

      existence

      proof

        reconsider f = ( chi (I,I)) as PartFunc of I, REAL by Th11;

        f is integrable by INTEGRA4: 2;

        hence thesis;

      end;

    end

    registration

      let X be non empty set;

      cluster bounded for Function of X, REAL ;

      existence

      proof

        reconsider f = ( chi (X,X)) as PartFunc of X, REAL by Th11;

        f is bounded by Th14;

        hence thesis;

      end;

    end

    theorem :: COUSIN2:41

    

     Th37: for f be bounded Function of I, REAL holds |.(( upper_bound ( rng f)) - ( lower_bound ( rng f))).| = 0 iff f is constant

    proof

      let f be bounded Function of I, REAL ;

      

       A1: ( rng f) is real-bounded by INTEGRA1: 15;

      hereby

        assume |.(( upper_bound ( rng f)) - ( lower_bound ( rng f))).| = 0 ;

        then (( upper_bound ( rng f)) - ( lower_bound ( rng f))) = 0 ;

        then ex r be Real st ( rng f) = {r} by A1, Th10;

        hence f is constant;

      end;

      assume f is constant;

      then

      consider y be Element of REAL such that

       A2: ( rng f) = {y} by FUNCT_2: 111;

      ( upper_bound ( rng f)) = y & ( lower_bound ( rng f)) = y by A2, SEQ_4: 9;

      hence |.(( upper_bound ( rng f)) - ( lower_bound ( rng f))).| = 0 ;

    end;

    registration

      let I be non empty closed_interval Subset of REAL ;

      cluster bounded for integrable Function of I, REAL ;

      existence

      proof

        reconsider f = ( chi (I,I)) as PartFunc of I, REAL by Th11;

        reconsider f as integrable Function of I, REAL by INTEGRA4: 2;

        f is bounded by Th14;

        hence thesis;

      end;

    end

    theorem :: COUSIN2:42

    for f be PartFunc of I, REAL st f is upper_integrable holds ex r be Real st for D be Division of I holds r < ( upper_sum (f,D))

    proof

      let f be PartFunc of I, REAL ;

      assume f is upper_integrable;

      then ( rng ( upper_sum_set f)) is bounded_below by INTEGRA1:def 12;

      then

      consider r be Real such that

       A1: for y be object st y in ( dom ( upper_sum_set f)) holds r < (( upper_sum_set f) . y) by INTEGRA1: 12, SEQ_2:def 2;

      

       A2: ( dom ( upper_sum_set f)) = ( divs I) by FUNCT_2:def 1;

      take r;

      let D be Division of I;

      D in ( divs I) by INTEGRA1:def 3;

      then r < (( upper_sum_set f) . D) by A1, A2;

      hence thesis by INTEGRA1:def 10;

    end;

    theorem :: COUSIN2:43

    for f be PartFunc of I, REAL st f is lower_integrable holds ex r be Real st for D be Division of I holds ( lower_sum (f,D)) < r

    proof

      let f be PartFunc of I, REAL ;

      assume f is lower_integrable;

      then ( rng ( lower_sum_set f)) is bounded_above by INTEGRA1:def 13;

      then

      consider r be Real such that

       A1: for y be object st y in ( dom ( lower_sum_set f)) holds (( lower_sum_set f) . y) < r by INTEGRA1: 14, SEQ_2:def 1;

      

       A2: ( dom ( lower_sum_set f)) = ( divs I) by FUNCT_2:def 1;

      take r;

      let D be Division of I;

      D in ( divs I) by INTEGRA1:def 3;

      then (( lower_sum_set f) . D) < r by A1, A2;

      hence thesis by INTEGRA1:def 11;

    end;

    theorem :: COUSIN2:44

    

     Th38: for f be Function of I, REAL holds for D,D1 be Division of I st (D . 1) = ( lower_bound I) & D1 = (D /^ 1) holds ( upper_sum (f,D1)) = ( upper_sum (f,D)) & ( lower_sum (f,D1)) = ( lower_sum (f,D))

    proof

      let f be Function of I, REAL ;

      let D,D1 be Division of I;

      assume that

       A1: (D . 1) = ( lower_bound I) and

       A2: D1 = (D /^ 1);

      D = ( <*(D /. 1)*> ^ (D /^ 1)) by FINSEQ_5: 29;

      then

       A4: D = ( <*(D . 1)*> ^ (D /^ 1)) by FINSEQ_5: 6, PARTFUN1:def 6;

      

       A5: (( upper_volume (f,D)) . 1) = 0

      proof

        ( divset (D,1)) = [.(D . 1), (D . 1).] by A1, COUSIN: 50;

        then ( lower_bound ( divset (D,1))) = (D . 1) & ( upper_bound ( divset (D,1))) = (D . 1) by JORDAN5A: 19;

        

        then

         A6: ( vol ( divset (D,1))) = ((D . 1) - (D . 1)) by INTEGRA1:def 5

        .= 0 ;

        1 in ( dom D) by FINSEQ_5: 6;

        

        then (( upper_volume (f,D)) . 1) = (( upper_bound ( rng (f | ( divset (D,1))))) * ( vol ( divset (D,1)))) by INTEGRA1:def 6

        .= 0 by A6;

        hence thesis;

      end;

       0 < ( len ( upper_volume (f,D)));

      

      then ( Sum ( upper_volume (f,D))) = ((( upper_volume (f,D)) . 1) + ( Sum (( upper_volume (f,D)) /^ 1))) by IRRAT_1: 17

      .= ( Sum ( upper_volume (f,D1))) by A4, A1, A2, INTEGRA3: 13, A5

      .= ( upper_sum (f,D1)) by INTEGRA1:def 8;

      hence ( upper_sum (f,D1)) = ( upper_sum (f,D)) by INTEGRA1:def 8;

      

       A7: (( lower_volume (f,D)) . 1) = 0

      proof

        ( divset (D,1)) = [.(D . 1), (D . 1).] by A1, COUSIN: 50;

        then ( lower_bound ( divset (D,1))) = (D . 1) & ( upper_bound ( divset (D,1))) = (D . 1) by JORDAN5A: 19;

        

        then

         A8: ( vol ( divset (D,1))) = ((D . 1) - (D . 1)) by INTEGRA1:def 5

        .= 0 ;

        1 in ( dom D) by FINSEQ_5: 6;

        

        then (( lower_volume (f,D)) . 1) = (( lower_bound ( rng (f | ( divset (D,1))))) * ( vol ( divset (D,1)))) by INTEGRA1:def 7

        .= 0 by A8;

        hence thesis;

      end;

       0 < ( len ( lower_volume (f,D)));

      

      then ( Sum ( lower_volume (f,D))) = ((( lower_volume (f,D)) . 1) + ( Sum (( lower_volume (f,D)) /^ 1))) by IRRAT_1: 17

      .= ( Sum ( lower_volume (f,D1))) by A4, A1, A2, INTEGRA3: 13, A7

      .= ( lower_sum (f,D1)) by INTEGRA1:def 9;

      hence thesis by INTEGRA1:def 9;

    end;

    reserve f for bounded integrable Function of I, REAL ;

    theorem :: COUSIN2:45

    

     Th39: for i be Nat st i in ( dom TD) holds (( lower_volume (f,( division_of TD))) . i) <= (( tagged_volume (f,TD)) . i) <= (( upper_volume (f,( division_of TD))) . i)

    proof

      let i be Nat;

      assume

       A1: i in ( dom TD);

      set a = (( lower_volume (f,( division_of TD))) . i), b = (( tagged_volume (f,TD)) . i), c = (( upper_volume (f,( division_of TD))) . i);

      reconsider D = ( division_of TD) as Division of I;

      set x = (( tagged_of TD) . i);

      consider D9 be Division of I, T9 be Element of ( set_of_tagged_Division D9) such that

       A2: ( tagged_of TD) = T9 & TD = [D9, T9] by Def2;

      

       A3: D = D9 & x = (T9 . i) by A2, Th20;

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

       A4: T9 = s & ( dom s) = ( dom D9) & for i be Nat st i in ( dom s) holds (s . i) in ( divset (D9,i)) by COUSIN:def 2;

      ( divset (D,i)) c= I by A1, INTEGRA1: 8;

      then x in I by A1, A3, A4;

      then

       A5: x in ( dom f) by FUNCT_2:def 1;

      then

      reconsider y = (f . x) as Element of REAL by PARTFUN1: 4;

      (f /. x) in ( rng (f | ( divset (D,i)))) by A1, A3, A4, A5, PARTFUN2: 18;

      then

       W1: (f . x) in ( rng (f | ( divset (D,i)))) by A5, PARTFUN1:def 6;

      ( rng f) is bounded_below by INTEGRA1: 11;

      then ( rng (f | ( divset (D,i)))) is bounded_below by RELAT_1: 70, XXREAL_2: 44;

      then

       W3: ( lower_bound ( rng (f | ( divset (D,i))))) <= (f . (( tagged_of TD) . i)) by SEQ_4:def 2, W1;

       0 <= ( vol ( divset (D,i))) by INTEGRA1: 9;

      then (( lower_bound ( rng (f | ( divset (D,i))))) * ( vol ( divset (D,i)))) <= ((f . (( tagged_of TD) . i)) * ( vol ( divset (( division_of TD),i)))) by XREAL_1: 64, W3;

      then (( lower_volume (f,D)) . i) <= ((f . (( tagged_of TD) . i)) * ( vol ( divset (( division_of TD),i)))) by A1, INTEGRA1:def 7;

      hence a <= b by A1, Def4;

      (f /. x) in ( rng (f | ( divset (D,i)))) by A1, A3, A4, A5, PARTFUN2: 18;

      then

       T2: (f . x) in ( rng (f | ( divset (D,i)))) by A5, PARTFUN1:def 6;

      ( rng f) is bounded_above by INTEGRA1: 13;

      then ( rng (f | ( divset (D,i)))) is bounded_above by RELAT_1: 70, XXREAL_2: 43;

      then

       W1: (f . (( tagged_of TD) . i)) <= ( upper_bound ( rng (f | ( divset (D,i))))) by SEQ_4:def 1, T2;

       0 <= ( vol ( divset (D,i))) by INTEGRA1: 9;

      then ((f . (( tagged_of TD) . i)) * ( vol ( divset (( division_of TD),i)))) <= (( upper_bound ( rng (f | ( divset (D,i))))) * ( vol ( divset (D,i)))) by W1, XREAL_1: 64;

      then ((f . (( tagged_of TD) . i)) * ( vol ( divset (( division_of TD),i)))) <= (( upper_volume (f,D)) . i) by A1, INTEGRA1:def 6;

      hence b <= c by A1, Def4;

    end;

    theorem :: COUSIN2:46

    

     Th40: ( Sum ( lower_volume (f,( division_of TD)))) <= ( Sum ( tagged_volume (f,TD))) <= ( Sum ( upper_volume (f,( division_of TD))))

    proof

      

       A1: ( len ( tagged_volume (f,TD))) = ( len TD) by Def4

      .= ( len ( lower_volume (f,( division_of TD)))) by INTEGRA1:def 7;

      ( dom TD) = ( Seg ( len ( division_of TD))) by FINSEQ_1:def 3

      .= ( Seg ( len ( lower_volume (f,( division_of TD))))) by INTEGRA1:def 7

      .= ( dom ( lower_volume (f,( division_of TD)))) by FINSEQ_1:def 3;

      then for i be Element of NAT st i in ( dom ( lower_volume (f,( division_of TD)))) holds (( lower_volume (f,( division_of TD))) . i) <= (( tagged_volume (f,TD)) . i) by Th39;

      hence ( Sum ( lower_volume (f,( division_of TD)))) <= ( Sum ( tagged_volume (f,TD))) by INTEGRA5: 3, A1;

      

       B1: ( len ( tagged_volume (f,TD))) = ( len TD) by Def4

      .= ( len ( upper_volume (f,( division_of TD)))) by INTEGRA1:def 6;

      ( dom TD) = ( Seg ( len TD)) by FINSEQ_1:def 3

      .= ( Seg ( len ( tagged_volume (f,TD)))) by Def4

      .= ( dom ( tagged_volume (f,TD))) by FINSEQ_1:def 3;

      then for i be Element of NAT st i in ( dom ( tagged_volume (f,TD))) holds (( tagged_volume (f,TD)) . i) <= (( upper_volume (f,( division_of TD))) . i) by Th39;

      hence ( Sum ( tagged_volume (f,TD))) <= ( Sum ( upper_volume (f,( division_of TD)))) by INTEGRA5: 3, B1;

    end;

    theorem :: COUSIN2:47

    

     Th41: for epsilon be Real st I is non trivial & 0 < epsilon holds ex D be Division of I st (D . 1) <> ( lower_bound I) & ( upper_sum (f,D)) < (( integral f) + (epsilon / 2)) & (( integral f) - (epsilon / 2)) < ( lower_sum (f,D)) & (( upper_sum (f,D)) - ( lower_sum (f,D))) < epsilon

    proof

      let epsilon be Real;

      assume that

       A1: I is non trivial and

       A4: 0 < epsilon;

      set J = ( integral f);

      

       A6: ( rng ( lower_sum_set f)) is bounded_above by INTEGRA1:def 13, INTEGRA1:def 16;

      

       A7: ( lower_integral f) = ( upper_integral f) by INTEGRA1:def 16;

      

       A8: ( lower_integral f) = ( upper_bound ( rng ( lower_sum_set f))) by INTEGRA1:def 15;

      set X = ( rng ( lower_sum_set f));

      set e = (epsilon / 2);

      consider ru be Real such that

       A10: ru in X and

       A11: (( upper_bound X) - e) < ru by A4, A6, SEQ_4:def 1;

      consider x1 be object such that

       A13: x1 in ( dom ( lower_sum_set f)) and

       A14: ru = (( lower_sum_set f) . x1) by A10, FUNCT_1:def 3;

      reconsider x1 as Division of I by A13, INTEGRA1:def 3;

      ru = ( lower_sum (f,x1)) by A14, INTEGRA1:def 11;

      then

       A15: (J - e) < ( lower_sum (f,x1)) by A8, A7, INTEGRA1:def 17, A11;

      

       A16: ( rng ( upper_sum_set f)) is bounded_below by INTEGRA1:def 12, INTEGRA1:def 16;

      

       A17: ( upper_integral f) = ( lower_bound ( rng ( upper_sum_set f))) by INTEGRA1:def 14;

      set X2 = ( rng ( upper_sum_set f));

      consider rl be Real such that

       A18: rl in X2 and

       A19: rl < (( lower_bound X2) + e) by A4, A16, SEQ_4:def 2;

      consider x2 be object such that

       A20: x2 in ( dom ( upper_sum_set f)) and

       A21: rl = (( upper_sum_set f) . x2) by A18, FUNCT_1:def 3;

      reconsider x2 as Division of I by A20, INTEGRA1:def 3;

      rl = ( upper_sum (f,x2)) by A21, INTEGRA1:def 10;

      then

       A22: ( upper_sum (f,x2)) < (J + e) by A17, INTEGRA1:def 17, A19;

      consider x3 be Division of I such that

       A23: x1 <= x3 and

       A24: x2 <= x3 by INTEGRA1: 47;

      per cases ;

        suppose

         A25: (x3 . 1) = ( lower_bound I);

        

         A26: 2 <= ( len x3)

        proof

          assume

           A27: ( len x3) < 2;

          

           A28: ( upper_bound I) = (x3 . ( len x3)) by INTEGRA1:def 2

          .= (x3 . 1) by A27, NAT_1: 23;

          I = [.(x3 . 1), (x3 . 1).] by A25, A28, INTEGRA1: 4;

          then I = {(x3 . 1)} by XXREAL_1: 17;

          hence thesis by A1;

        end;

        then

        reconsider x4 = (x3 /^ 1) as Division of I by COUSIN: 65;

        take x4;

        now

          thus

           A29: (x4 . 1) <> ( lower_bound I)

          proof

            assume

             A30: (x4 . 1) = ( lower_bound I);

            

             A31: 1 <= ( len x3) by A26, XXREAL_0: 2;

            then ( len (x3 /^ 1)) = (( len x3) - 1) by RFINSEQ:def 1;

            then (2 - 1) <= ((( len (x3 /^ 1)) + 1) - 1) by A26, XREAL_1: 9;

            then 1 in ( dom (x3 /^ 1)) by FINSEQ_3: 25;

            then

             A32: (x4 . 1) = (x3 . (1 + 1)) by A31, RFINSEQ:def 1;

            1 <= ( len x3) & 2 <= ( len x3) by A26, XXREAL_0: 2;

            then 1 in ( dom x3) & 2 in ( dom x3) by FINSEQ_3: 25;

            hence thesis by A32, A25, A30, VALUED_0:def 13;

          end;

          

           A33: ( upper_sum (f,x4)) = ( upper_sum (f,x3)) & ( lower_sum (f,x4)) = ( lower_sum (f,x3)) by A25, Th38;

          (f | I) is bounded_above & (f | I) is bounded_below;

          then

           A34: ( upper_sum (f,x4)) <= ( upper_sum (f,x2)) & ( lower_sum (f,x1)) <= ( lower_sum (f,x4)) by A33, A23, A24, INTEGRA1: 45, INTEGRA1: 46;

          then ( upper_sum (f,x4)) < (J + e) & (J - e) < ( lower_sum (f,x4)) by A15, A22, XXREAL_0: 2;

          then (( upper_sum (f,x4)) - ( lower_sum (f,x4))) < (2 * e) by Lm02;

          hence thesis by A34, A15, A22, XXREAL_0: 2, A29;

        end;

        hence thesis;

      end;

        suppose

         A35: (x3 . 1) <> ( lower_bound I);

        (f | I) is bounded_above & (f | I) is bounded_below;

        then ( upper_sum (f,x3)) <= ( upper_sum (f,x2)) & ( lower_sum (f,x1)) <= ( lower_sum (f,x3)) by A23, A24, INTEGRA1: 45, INTEGRA1: 46;

        then

         A36: ( upper_sum (f,x3)) < (J + e) & (J - e) < ( lower_sum (f,x3)) by A15, A22, XXREAL_0: 2;

        then (( upper_sum (f,x3)) - ( lower_sum (f,x3))) < (2 * e) by Lm02;

        hence thesis by A36, A35;

      end;

    end;

    reserve jauge for positive-yielding Function of I, REAL ;

    theorem :: COUSIN2:48

    jauge = (r (#) ( chi (I,I))) implies 0 < r

    proof

      assume

       A1: jauge = (r (#) ( chi (I,I)));

      assume

       A2: r <= 0 ;

      set x = the Element of I;

      x in I;

      then

       A3: x in ( dom ( chi (I,I))) & x in ( dom jauge) by PARTFUN1:def 2;

      

      then (jauge . x) = (r * (( chi (I,I)) . x)) by A1, VALUED_1:def 5

      .= (r * 1) by FUNCT_3:def 3

      .= r;

      then (jauge . x) <= 0 & (jauge . x) in ( rng jauge) by A2, A3, FUNCT_1: 3;

      hence contradiction by PARTFUN3:def 1;

    end;

    reserve D for tagged_division of I;

    theorem :: COUSIN2:49

    

     Th42: jauge = (r (#) ( chi (I,I))) & D is jauge -fine implies ( delta ( division_of D)) <= r

    proof

      assume that

       A1: jauge = (r (#) ( chi (I,I))) and

       A2: D is jauge -fine;

       A3:

      now

        let i be Nat;

        assume

         A4: i in ( dom ( division_of D));

        consider D9 be Division of I, T9 be Element of ( set_of_tagged_Division D9) such that

         A5: D = [D9, T9] & for i be Nat st i in ( dom D9) holds ( vol ( divset (D9,i))) <= (jauge . (T9 . i)) by A2, COUSIN:def 4;

        

         A6: T9 = ( tagged_of D) & D9 = ( division_of D) by A5, Th20;

        then

         A7: ( vol ( divset (( division_of D),i))) <= (jauge . (( tagged_of D) . i)) by A5, A4;

        

         A8: ( dom (r (#) ( chi (I,I)))) = ( dom ( chi (I,I))) by VALUED_1:def 5

        .= I by FUNCT_3:def 3;

        i in ( Seg ( len ( division_of D))) by A4, FINSEQ_1:def 3;

        then i in ( Seg ( len ( tagged_of D))) by Th21;

        then

         A9: i in ( dom T9) by A6, FINSEQ_1:def 3;

        ( rng T9) c= I by Th22;

        then

         A10: (( tagged_of D) . i) in I by A9, A6, FUNCT_1: 3;

        now

          let x be object;

          assume

           A11: x in ( dom (r (#) ( chi (I,I))));

          

          then ((r (#) ( chi (I,I))) . x) = (r * (( chi (I,I)) . x)) by VALUED_1:def 5

          .= (r * 1) by A11, FUNCT_3:def 3

          .= r;

          hence (jauge . x) = r by A1;

        end;

        hence ( vol ( divset (( division_of D),i))) <= r by A7, A8, A10;

      end;

      reconsider g = ( chi (I,I)) as Function of I, REAL by Th11;

      

       A12: for i be Nat st i in ( dom ( division_of D)) holds (( upper_volume (g,( division_of D))) . i) <= r

      proof

        let i be Nat;

        assume

         A13: i in ( dom ( division_of D));

        then ( vol ( divset (( division_of D),i))) <= r by A3;

        hence thesis by A13, INTEGRA1: 20;

      end;

      ( delta ( division_of D)) <= r

      proof

        assume r < ( delta ( division_of D));

        then

         A14: r < ( max ( rng ( upper_volume (g,( division_of D))))) by INTEGRA3:def 1;

        ( sup ( rng ( upper_volume (g,( division_of D))))) in ( rng ( upper_volume (g,( division_of D)))) by XXREAL_2:def 6;

        then

        consider x be object such that

         A15: x in ( dom ( upper_volume (g,( division_of D)))) and

         A16: (( upper_volume (g,( division_of D))) . x) = ( sup ( rng ( upper_volume (g,( division_of D))))) by FUNCT_1:def 3;

        

         A17: ( dom ( upper_volume (g,( division_of D)))) = ( Seg ( len ( upper_volume (g,( division_of D))))) by FINSEQ_1:def 3

        .= ( Seg ( len ( division_of D))) by INTEGRA1:def 6

        .= ( dom ( division_of D)) by FINSEQ_1:def 3;

        reconsider i = x as Nat by A15;

        thus contradiction by A14, A15, A17, A16, A12;

      end;

      hence thesis;

    end;

    reserve r1,r2,s for Real,

D,D1 for Division of I,

fc for Function of I, REAL ;

    theorem :: COUSIN2:50

    

     Th43: ex i be Nat st i in ( dom D) & ( min ( rng ( upper_volume (fc,D)))) = (( upper_volume (fc,D)) . i)

    proof

      ( inf ( rng ( upper_volume (fc,D)))) in ( rng ( upper_volume (fc,D))) by XXREAL_2:def 5;

      then

      consider x be object such that

       A1: x in ( dom ( upper_volume (fc,D))) and

       A2: (( upper_volume (fc,D)) . x) = ( inf ( rng ( upper_volume (fc,D)))) by FUNCT_1:def 3;

      

       A3: ( dom ( upper_volume (fc,D))) = ( Seg ( len ( upper_volume (fc,D)))) by FINSEQ_1:def 3

      .= ( Seg ( len D)) by INTEGRA1:def 6

      .= ( dom D) by FINSEQ_1:def 3;

      reconsider i = x as Nat by A1;

      take i;

      thus thesis by A2, A3, A1;

    end;

    theorem :: COUSIN2:51

    

     Th44: for f be Function of I, REAL holds for epsilon be Real st fc = ( chi (I,I)) & r1 = ( min ( rng ( upper_volume (fc,D1)))) & r2 = (epsilon / ((2 * ( len D1)) * |.(( upper_bound ( rng f)) - ( lower_bound ( rng f))).|)) & 0 < r1 & 0 < r2 & s = (( min (r1,r2)) / 2) & jauge = (s (#) fc) & TD is jauge -fine holds ( delta ( division_of TD)) < ( min ( rng ( upper_volume (fc,D1)))) & ( delta ( division_of TD)) < (epsilon / ((2 * ( len D1)) * |.(( upper_bound ( rng f)) - ( lower_bound ( rng f))).|))

    proof

      let f be Function of I, REAL ;

      let epsilon be Real;

      assume that

       A1: fc = ( chi (I,I)) and

       A2: r1 = ( min ( rng ( upper_volume (fc,D1)))) and

       A3: r2 = (epsilon / ((2 * ( len D1)) * |.(( upper_bound ( rng f)) - ( lower_bound ( rng f))).|)) and

       A4: 0 < r1 and

       A5: 0 < r2 and

       A6: s = (( min (r1,r2)) / 2) and

       A7: jauge = (s (#) fc) and

       A8: TD is jauge -fine;

      

       A9: ( delta ( division_of TD)) <= (( min (r1,r2)) / 2) by A1, A6, A7, A8, Th42;

      (( min (r1,r2)) / 2) < (( min (r1,r2)) / 1) by A4, A5, XREAL_1: 76;

      then ( delta ( division_of TD)) < ( min (r1,r2)) by A9, XXREAL_0: 2;

      hence thesis by A2, A3, XXREAL_0: 23;

    end;

    theorem :: COUSIN2:52

    

     Th45: for p be FinSequence of REAL st (for i be Nat st i in ( dom p) holds r <= (p . i)) & ex i0 be Nat st i0 in ( dom p) & (p . i0) = r holds r = ( inf ( rng p))

    proof

      let p be FinSequence of REAL ;

      assume that

       A1: for i be Nat st i in ( dom p) holds r <= (p . i) and

       A2: ex i0 be Nat st i0 in ( dom p) & (p . i0) = r;

      set X = ( rng p);

      consider i0 be Nat such that

       A3: i0 in ( dom p) and

       A4: (p . i0) = r by A2;

      reconsider X as non empty bounded_below real-membered set by A3, A4, FUNCT_1:def 3;

      

       A5: for a be Real st a in X holds r <= a

      proof

        let a be Real;

        assume a in X;

        then ex i be object st i in ( dom p) & (p . i) = a by FUNCT_1:def 3;

        hence thesis by A1;

      end;

      for s be Real st 0 < s holds ex a be Real st a in X & a < (r + s)

      proof

        let s be Real;

        assume

         A6: 0 < s;

        consider i0 be Nat such that

         A7: i0 in ( dom p) and

         A8: (p . i0) = r by A2;

        reconsider a = (p . i0) as Real;

        take a;

        thus a in X by A7, FUNCT_1:def 3;

        (r + 0 ) < (r + s) by A6, XREAL_1: 8;

        hence a < (r + s) by A8;

      end;

      then r = ( lower_bound X) by A5, SEQ_4:def 2;

      hence thesis;

    end;

    theorem :: COUSIN2:53

    

     Th46: fc = ( chi (I,I)) implies 0 <= ( min ( rng ( upper_volume (fc,D)))) & ( 0 = ( min ( rng ( upper_volume (fc,D)))) iff ( divset (D,1)) = [.(D . 1), (D . 1).])

    proof

      assume

       A1: fc = ( chi (I,I));

      consider i0 be Nat such that

       A2: i0 in ( dom D) and

       A3: ( min ( rng ( upper_volume (fc,D)))) = (( upper_volume (fc,D)) . i0) by Th43;

      ( min ( rng ( upper_volume (fc,D)))) = ( vol ( divset (D,i0))) by A1, A2, A3, INTEGRA1: 20;

      hence 0 <= ( min ( rng ( upper_volume (fc,D)))) by INTEGRA1: 9;

      thus 0 = ( min ( rng ( upper_volume (fc,D)))) iff ( divset (D,1)) = [.(D . 1), (D . 1).]

      proof

        hereby

          assume 0 = ( min ( rng ( upper_volume (fc,D))));

          then

           A4: ( vol ( divset (D,i0))) = 0 by A3, A1, A2, INTEGRA1: 20;

          ( rng D) <> {} ;

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

          then (D . 1) in I by INTEGRA1: 6;

          then (D . 1) in [.( lower_bound I), ( upper_bound I).] by INTEGRA1: 4;

          then

           A5: ( lower_bound I) <= (D . 1) by XXREAL_1: 1;

          now

            1 <= i0 <= ( len D) by A2, FINSEQ_3: 25;

            per cases by XXREAL_0: 1;

              suppose i0 = 1;

              then ( divset (D,i0)) = [.( lower_bound I), (D . 1).] by COUSIN: 50;

              then ( lower_bound ( divset (D,i0))) = ( lower_bound I) & ( upper_bound ( divset (D,i0))) = (D . 1) by A5, JORDAN5A: 19;

              then ( vol ( divset (D,i0))) = ((D . 1) - ( lower_bound I)) by INTEGRA1:def 5;

              hence ( divset (D,1)) = [.(D . 1), (D . 1).] by A4, COUSIN: 50;

            end;

              suppose

               A6: 1 < i0;

               A7:

              now

                thus i0 in ( dom D) by A2;

                thus (i0 - 1) in ( dom D) by A6, A2, CGAMES_1: 20;

                (i0 - 1) < (i0 - 0 ) by XREAL_1: 15;

                hence (i0 - 1) < i0;

              end;

              then

               A8: (D . (i0 - 1)) < (D . i0) by VALUED_0:def 13;

              ( divset (D,i0)) = [.(D . (i0 - 1)), (D . i0).] by A6, A2, COUSIN: 50;

              then ( lower_bound ( divset (D,i0))) = (D . (i0 - 1)) & ( upper_bound ( divset (D,i0))) = (D . i0) by A8, JORDAN5A: 19;

              then ( vol ( divset (D,i0))) = ((D . i0) - (D . (i0 - 1))) by INTEGRA1:def 5;

              hence ( divset (D,1)) = [.(D . 1), (D . 1).] by A4, A7, VALUED_0:def 13;

            end;

          end;

          hence ( divset (D,1)) = [.(D . 1), (D . 1).];

        end;

        assume

         A9: ( divset (D,1)) = [.(D . 1), (D . 1).];

        

         A10: ( vol ( divset (D,1))) = (( upper_bound ( divset (D,1))) - ( lower_bound ( divset (D,1)))) by INTEGRA1:def 5

        .= ((D . 1) - ( lower_bound ( divset (D,1)))) by A9, JORDAN5A: 19

        .= ((D . 1) - (D . 1)) by A9, JORDAN5A: 19

        .= 0 ;

        ( rng D) <> {} ;

        then

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

        then

         A12: (( upper_volume (fc,D)) . 1) = 0 by A1, A10, INTEGRA1: 20;

        1 in ( Seg ( len D)) by A11, FINSEQ_1:def 3;

        then 1 in ( Seg ( len ( upper_volume (fc,D)))) by INTEGRA1:def 6;

        then

         A13: 1 in ( dom ( upper_volume (fc,D))) by FINSEQ_1:def 3;

        now

          let i be Nat;

          assume i in ( dom ( upper_volume (fc,D)));

          then i in ( Seg ( len ( upper_volume (fc,D)))) by FINSEQ_1:def 3;

          then i in ( Seg ( len D)) by INTEGRA1:def 6;

          then i in ( dom D) by FINSEQ_1:def 3;

          then (( upper_volume (fc,D)) . i) = ( vol ( divset (D,i))) by A1, INTEGRA1: 20;

          hence 0 <= (( upper_volume (fc,D)) . i) by INTEGRA1: 9;

        end;

        hence 0 = ( min ( rng ( upper_volume (fc,D)))) by A13, A12, Th45;

      end;

    end;

    theorem :: COUSIN2:54

    

     Th47: ( divset (D,1)) = [.(D . 1), (D . 1).] implies (D . 1) = ( lower_bound I)

    proof

      assume ( divset (D,1)) = [.(D . 1), (D . 1).];

      then

       A1: ( lower_bound ( divset (D,1))) = (D . 1) & ( upper_bound ( divset (D,1))) = (D . 1) by JORDAN5A: 19;

      

       A2: ( divset (D,1)) = [.( lower_bound I), (D . 1).] by COUSIN: 50;

      ( rng D) <> {} ;

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

      then (D . 1) in I by INTEGRA1: 6;

      then (D . 1) in [.( lower_bound I), ( upper_bound I).] by INTEGRA1: 4;

      then ( lower_bound I) <= (D . 1) <= ( upper_bound I) by XXREAL_1: 1;

      hence thesis by A1, A2, JORDAN5A: 19;

    end;

    theorem :: COUSIN2:55

    

     Th48: for f be bounded integrable Function of I, REAL holds f is HK-integrable & ( HK-integral f) = ( integral f)

    proof

      let f be bounded integrable Function of I, REAL ;

      per cases ;

        suppose

         A1: f is constant;

        then

        consider r be Real such that

         A2: f = (r (#) ( chi (I,I))) and

         A3: ( HK-integral f) = (r * ( vol I)) by Th36;

        reconsider g = ( chi (I,I)) as Function of I, REAL by Th11;

        

         A4: (g | I) is bounded by Th14;

        g is integrable by INTEGRA4: 2;

        then ( integral f) = (r * ( integral g)) by A2, A4, INTEGRA2: 31;

        hence thesis by A1, Th36, A3, INTEGRA4: 2;

      end;

        suppose

         A5: f is non constant;

        per cases ;

          suppose I is trivial;

          then f is HK-integrable & ( HK-integral f) = 0 & ( vol I) = 0 by Th25, Th27;

          hence thesis by INTEGRA4: 6;

        end;

          suppose

           A6: I is non trivial;

          set J = ( integral f);

           A7:

          now

            let epsilon be Real;

            assume

             A8: epsilon > 0 ;

            consider D be Division of I such that

             A9: (D . 1) <> ( lower_bound I) and

             A10: ( upper_sum (f,D)) < (( integral f) + (epsilon / 2)) and

             A11: (( integral f) - (epsilon / 2)) < ( lower_sum (f,D)) and (( upper_sum (f,D)) - ( lower_sum (f,D))) < epsilon by A6, A8, Th41;

            reconsider fc = ( chi (I,I)) as Function of I, REAL by Th11;

             0 < ( min ( rng ( upper_volume (fc,D))))

            proof

              assume not 0 < ( min ( rng ( upper_volume (fc,D))));

              then 0 = ( min ( rng ( upper_volume (fc,D)))) by Th46;

              then ( divset (D,1)) = [.(D . 1), (D . 1).] by Th46;

              hence contradiction by A9, Th47;

            end;

            then

            reconsider r1 = ( min ( rng ( upper_volume (fc,D)))) as positive Real;

             |.(( upper_bound ( rng f)) - ( lower_bound ( rng f))).| <> 0 by A5, Th37;

            then

            reconsider r2 = (epsilon / ((2 * ( len D)) * |.(( upper_bound ( rng f)) - ( lower_bound ( rng f))).|)) as positive Real by A8;

            reconsider s = (( min (r1,r2)) / 2) as positive Real;

            ( chi (I,I)) is positive-yielding by Th17;

            then

            reconsider jauge = (s (#) fc) as positive-yielding Function of I, REAL ;

            take jauge;

            thus for TD be tagged_division of I st TD is jauge -fine holds |.(( tagged_sum (f,TD)) - ( integral f)).| <= epsilon

            proof

              let TD be tagged_division of I;

              assume

               A12: TD is jauge -fine;

              ( Sum ( lower_volume (f,( division_of TD)))) <= ( Sum ( tagged_volume (f,TD))) <= ( Sum ( upper_volume (f,( division_of TD)))) by Th40;

              then

               A13: ( lower_sum (f,( division_of TD))) <= ( tagged_sum (f,TD)) <= ( upper_sum (f,( division_of TD))) by INTEGRA1:def 8, INTEGRA1:def 9;

              

               A14: (f | I) is bounded & ( delta ( division_of TD)) < ( min ( rng ( upper_volume (fc,D)))) by A12, Th44;

              then

              consider D9 be Division of I such that

               A15: D <= D9 and

               A16: ( division_of TD) <= D9 and

               A17: ( rng D9) = (( rng ( division_of TD)) \/ ( rng D)) and

               A18: (( upper_sum (f,( division_of TD))) - ( upper_sum (f,D9))) <= ((( len D) * (( upper_bound ( rng f)) - ( lower_bound ( rng f)))) * ( delta ( division_of TD))) by INTEGRA3: 24;

              consider D9B be Division of I such that D <= D9B and ( division_of TD) <= D9B and

               A19: ( rng D9B) = (( rng ( division_of TD)) \/ ( rng D)) and

               A20: (( lower_sum (f,D9B)) - ( lower_sum (f,( division_of TD)))) <= ((( len D) * (( upper_bound ( rng f)) - ( lower_bound ( rng f)))) * ( delta ( division_of TD))) by A14, INTEGRA3: 22;

              (f | I) is bounded_above;

              then

               A21: ( upper_sum (f,D9)) <= ( upper_sum (f,( division_of TD))) & ( upper_sum (f,D9)) <= ( upper_sum (f,D)) by A16, A15, INTEGRA1: 45;

              (f | I) is bounded_below;

              then

               A22: ( lower_sum (f,( division_of TD))) <= ( lower_sum (f,D9)) & ( lower_sum (f,D)) <= ( lower_sum (f,D9)) by A16, A15, INTEGRA1: 46;

              

               A23: J = ( upper_integral f) by INTEGRA1:def 17;

              then

               A24: J = ( lower_integral f) by INTEGRA1:def 16;

              then

               A25: ( lower_sum (f,( division_of TD))) <= J by Th18, INTEGRA1:def 16;

              

               A26: (J - (epsilon / 2)) < ( lower_sum (f,D9)) <= J by A22, A11, XXREAL_0: 2, Th18, INTEGRA1:def 16, A24;

              

               A27: J <= ( upper_sum (f,( division_of TD))) by A23, Th19, INTEGRA1:def 16;

              

               A28: J <= ( upper_sum (f,D9)) < (J + (epsilon / 2)) by A21, A10, XXREAL_0: 2, A23, INTEGRA1:def 16, Th19;

              now

                thus (( upper_sum (f,( division_of TD))) - ( upper_sum (f,D9))) <= ((( len D) * (( upper_bound ( rng f)) - ( lower_bound ( rng f)))) * ( delta ( division_of TD))) by A18;

                thus 0 <= ( len D);

                ( lower_bound ( rng f)) <= ( upper_bound ( rng f)) by INTEGRA1: 15, SEQ_4: 11;

                hence 0 <= (( upper_bound ( rng f)) - ( lower_bound ( rng f))) by XREAL_1: 48;

                thus 0 <= ( delta ( division_of TD)) by INTEGRA3: 9;

                thus ( delta ( division_of TD)) < (epsilon / ((2 * ( len D)) * |.(( upper_bound ( rng f)) - ( lower_bound ( rng f))).|)) by A12, Th44;

              end;

              then

               A29: (( upper_sum (f,( division_of TD))) - ( upper_sum (f,D9))) <= (epsilon / 2) by Th07;

              

               A30: (( lower_sum (f,D9)) - ( lower_sum (f,( division_of TD)))) <= (epsilon / 2)

              proof

                

                 A31: (( lower_sum (f,D9)) - ( lower_sum (f,( division_of TD)))) <= ((( len D) * (( upper_bound ( rng f)) - ( lower_bound ( rng f)))) * ( delta ( division_of TD))) by A20, A17, A19, INTEGRA3: 6;

                ( lower_bound ( rng f)) <= ( upper_bound ( rng f)) by INTEGRA1: 15, SEQ_4: 11;

                then

                 A32: 0 <= (( upper_bound ( rng f)) - ( lower_bound ( rng f))) by XREAL_1: 48;

                 0 <= ( delta ( division_of TD)) by INTEGRA3: 9;

                hence thesis by A31, A32, Th07, A12, Th44;

              end;

              

               A33: |.(( lower_sum (f,( division_of TD))) - J).| <= epsilon

              proof

                ((J - (epsilon / 2)) - ( lower_sum (f,( division_of TD)))) <= (( lower_sum (f,D9)) - ( lower_sum (f,( division_of TD)))) by A26, XREAL_1: 9;

                then ((J - (epsilon / 2)) - ( lower_sum (f,( division_of TD)))) <= (epsilon / 2) by A30, XXREAL_0: 2;

                then (((J - ( lower_sum (f,( division_of TD)))) - (epsilon / 2)) + (epsilon / 2)) <= ((epsilon / 2) + (epsilon / 2)) by XREAL_1: 6;

                hence thesis by Th01, A25;

              end;

               |.(( upper_sum (f,( division_of TD))) - J).| <= epsilon

              proof

                (( upper_sum (f,( division_of TD))) - (J + (epsilon / 2))) < (( upper_sum (f,( division_of TD))) - ( upper_sum (f,D9))) by A28, XREAL_1: 15;

                then (( upper_sum (f,( division_of TD))) - (J + (epsilon / 2))) < (epsilon / 2) by A29, XXREAL_0: 2;

                then (((( upper_sum (f,( division_of TD))) - J) - (epsilon / 2)) + (epsilon / 2)) < ((epsilon / 2) + (epsilon / 2)) by XREAL_1: 8;

                hence thesis by A27, Th02;

              end;

              hence thesis by A13, A33, Th03;

            end;

          end;

          hence f is HK-integrable;

          hence thesis by A7, DEFCC;

        end;

      end;

    end;

    registration

      let I be non empty closed_interval Subset of REAL ;

      cluster bounded integrable -> HK-integrable for Function of I, REAL ;

      coherence by Th48;

    end