integra4.miz



    begin

    reserve i,j,k,n,n1,n2,m for Nat;

    reserve a,r,x,y for Real;

    reserve A for non empty closed_interval Subset of REAL ;

    reserve C for non empty set;

    reserve X for set;

    theorem :: INTEGRA4:1

    

     Th1: for D be Division of A st ( vol A) = 0 holds ( len D) = 1

    proof

      let D be Division of A;

      assume that

       A1: ( vol A) = 0 and

       A2: ( len D) <> 1;

      ( rng D) <> {} ;

      then

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

      then

       A4: 1 <= ( len D) by FINSEQ_3: 25;

      then

       A5: ( len D) in ( dom D) by FINSEQ_3: 25;

      (D . 1) in A by A3, INTEGRA1: 6;

      then

       A6: ( lower_bound A) <= (D . 1) by INTEGRA2: 1;

      1 < ( len D) by A2, A4, XXREAL_0: 1;

      then

       A7: (D . 1) < (D . ( len D)) by A3, A5, SEQM_3:def 1;

      (( upper_bound A) - ( lower_bound A)) = 0 by A1, INTEGRA1:def 5;

      hence contradiction by A7, A6, INTEGRA1:def 2;

    end;

    theorem :: INTEGRA4:2

    

     Th2: ( chi (A,A)) is integrable & ( integral ( chi (A,A))) = ( vol A)

    proof

      (( divs A) /\ ( dom ( upper_sum_set ( chi (A,A))))) = (( divs A) /\ ( divs A)) by FUNCT_2:def 1;

      then

       A1: ( divs A) meets ( dom ( upper_sum_set ( chi (A,A)))) by XBOOLE_0:def 7;

      reconsider vA = ( vol A) as Element of REAL by XREAL_0:def 1;

      

       A2: for D1 be Element of ( divs A) st D1 in (( divs A) /\ ( dom ( upper_sum_set ( chi (A,A))))) holds (( upper_sum_set ( chi (A,A))) /. D1) = vA

      proof

        let D1 be Element of ( divs A);

        reconsider D2 = D1 as Division of A by INTEGRA1:def 3;

        assume D1 in (( divs A) /\ ( dom ( upper_sum_set ( chi (A,A)))));

        (( upper_sum_set ( chi (A,A))) /. D1) = (( upper_sum_set ( chi (A,A))) . D1)

        .= ( upper_sum (( chi (A,A)),D2)) by INTEGRA1:def 10

        .= ( Sum ( upper_volume (( chi (A,A)),D2))) by INTEGRA1:def 8;

        hence thesis by INTEGRA1: 24;

      end;

      then (( upper_sum_set ( chi (A,A))) | ( divs A)) is constant by PARTFUN2: 35;

      then

      consider x be Element of REAL such that

       A3: ( rng (( upper_sum_set ( chi (A,A))) | ( divs A))) = {x} by A1, PARTFUN2: 37;

      

       A4: ( chi (A,A)) is upper_integrable by A3, INTEGRA1:def 12;

      ( vol A) in ( rng ( upper_sum_set ( chi (A,A))))

      proof

        set D1 = the Element of ( divs A);

        D1 in ( divs A);

        then

         A5: D1 in ( dom ( upper_sum_set ( chi (A,A)))) by FUNCT_2:def 1;

        then

         A6: (( upper_sum_set ( chi (A,A))) . D1) in ( rng ( upper_sum_set ( chi (A,A)))) by FUNCT_1:def 3;

        

         A7: (( upper_sum_set ( chi (A,A))) . D1) = (( upper_sum_set ( chi (A,A))) /. D1);

        D1 in (( divs A) /\ ( dom ( upper_sum_set ( chi (A,A))))) by A5, XBOOLE_0:def 4;

        hence thesis by A2, A6, A7;

      end;

      then

       A8: x = ( vol A) by A3, TARSKI:def 1;

      ( rng ( upper_sum_set ( chi (A,A)))) = {x} by A3;

      then ( lower_bound ( rng ( upper_sum_set ( chi (A,A))))) = ( vol A) by A8, SEQ_4: 9;

      then

       A9: ( upper_integral ( chi (A,A))) = ( vol A) by INTEGRA1:def 14;

      (( divs A) /\ ( dom ( lower_sum_set ( chi (A,A))))) = (( divs A) /\ ( divs A)) by FUNCT_2:def 1;

      then

       A10: ( divs A) meets ( dom ( lower_sum_set ( chi (A,A)))) by XBOOLE_0:def 7;

      reconsider vA = ( vol A) as Element of REAL by XREAL_0:def 1;

      

       A11: for D1 be Element of ( divs A) st D1 in (( divs A) /\ ( dom ( lower_sum_set ( chi (A,A))))) holds (( lower_sum_set ( chi (A,A))) /. D1) = vA

      proof

        let D1 be Element of ( divs A);

        reconsider D2 = D1 as Division of A by INTEGRA1:def 3;

        assume D1 in (( divs A) /\ ( dom ( lower_sum_set ( chi (A,A)))));

        (( lower_sum_set ( chi (A,A))) /. D1) = (( lower_sum_set ( chi (A,A))) . D1)

        .= ( lower_sum (( chi (A,A)),D2)) by INTEGRA1:def 11

        .= ( Sum ( lower_volume (( chi (A,A)),D2))) by INTEGRA1:def 9;

        hence thesis by INTEGRA1: 23;

      end;

      then (( lower_sum_set ( chi (A,A))) | ( divs A)) is constant by PARTFUN2: 35;

      then

      consider x be Element of REAL such that

       A12: ( rng (( lower_sum_set ( chi (A,A))) | ( divs A))) = {x} by A10, PARTFUN2: 37;

      ( vol A) in ( rng ( lower_sum_set ( chi (A,A))))

      proof

        set D1 = the Element of ( divs A);

        D1 in ( divs A);

        then

         A13: D1 in ( dom ( lower_sum_set ( chi (A,A)))) by FUNCT_2:def 1;

        then

         A14: (( lower_sum_set ( chi (A,A))) . D1) in ( rng ( lower_sum_set ( chi (A,A)))) by FUNCT_1:def 3;

        

         A15: (( lower_sum_set ( chi (A,A))) . D1) = (( lower_sum_set ( chi (A,A))) /. D1);

        D1 in (( divs A) /\ ( dom ( lower_sum_set ( chi (A,A))))) by A13, XBOOLE_0:def 4;

        hence thesis by A11, A14, A15;

      end;

      then

       A16: x = ( vol A) by A12, TARSKI:def 1;

      ( rng ( lower_sum_set ( chi (A,A)))) = {x} by A12;

      then ( upper_bound ( rng ( lower_sum_set ( chi (A,A))))) = ( vol A) by A16, SEQ_4: 9;

      then

       A17: ( lower_integral ( chi (A,A))) = ( vol A) by INTEGRA1:def 15;

      ( chi (A,A)) is lower_integrable by A12, INTEGRA1:def 13;

      hence thesis by A4, A9, A17, INTEGRA1:def 16, INTEGRA1:def 17;

    end;

    theorem :: INTEGRA4:3

    

     Th3: for f be PartFunc of A, REAL , r holds f is total & ( rng f) = {r} iff f = (r (#) ( chi (A,A)))

    proof

      let f be PartFunc of A, REAL ;

      let r;

      

       A1: f = (r (#) ( chi (A,A))) implies f is total & ( rng f) = {r}

      proof

        assume

         A2: f = (r (#) ( chi (A,A)));

        

         A3: ( chi (A,A)) is total by RFUNCT_1: 62;

        hence f is total by A2;

        

         A4: ( dom f) = A by A2, A3, PARTFUN1:def 2;

        for x be object st x in {r} holds x in ( rng f)

        proof

          let x be object;

          assume x in {r};

          then

           A5: x = r by TARSKI:def 1;

          consider a be Element of REAL such that

           A6: a in ( dom f) by A4, SUBSET_1: 4;

          (( chi (A,A)) . a) = 1 by A6, RFUNCT_1: 63;

          then (f . a) = (r * 1) by A2, A6, VALUED_1:def 5;

          hence thesis by A5, A6, FUNCT_1:def 3;

        end;

        then

         A7: {r} c= ( rng f) by TARSKI:def 3;

        for x be object st x in ( rng f) holds x in {r}

        proof

          let x be object;

          assume x in ( rng f);

          then

          consider a be Element of A such that

           A8: a in ( dom f) and

           A9: (f . a) = x by PARTFUN1: 3;

          (( chi (A,A)) . a) = 1 by RFUNCT_1: 63;

          

          then x = (r * 1) by A2, A8, A9, VALUED_1:def 5

          .= r;

          hence thesis by TARSKI:def 1;

        end;

        then ( rng f) c= {r} by TARSKI:def 3;

        hence thesis by A7, XBOOLE_0:def 10;

      end;

      f is total & ( rng f) = {r} implies f = (r (#) ( chi (A,A)))

      proof

        reconsider g = (r (#) ( chi (A,A))) as PartFunc of A, REAL ;

        assume

         A10: f is total;

        

         A11: ( chi (A,A)) is total by RFUNCT_1: 62;

        

         A12: ( dom g) = ( dom ( chi (A,A))) by VALUED_1:def 5

        .= A by A11, PARTFUN1:def 2;

        assume

         A13: ( rng f) = {r};

        

         A14: for x be Element of A st x in ( dom f) holds (f /. x) = (g /. x)

        proof

          let x be Element of A;

          assume

           A15: x in ( dom f);

          then (f /. x) = (f . x) by PARTFUN1:def 6;

          then

           A16: (f /. x) in ( rng f) by A15, FUNCT_1:def 3;

          (g /. x) = (g . x) by A12, PARTFUN1:def 6

          .= (r * (( chi (A,A)) . x)) by A12, VALUED_1:def 5

          .= (r * 1) by RFUNCT_1: 63

          .= r;

          hence thesis by A13, A16, TARSKI:def 1;

        end;

        ( dom f) = ( dom g) by A10, A12, PARTFUN1:def 2;

        hence thesis by A14, PARTFUN2: 1;

      end;

      hence thesis by A1;

    end;

    theorem :: INTEGRA4:4

    

     Th4: for f be Function of A, REAL , r st ( rng f) = {r} holds f is integrable & ( integral f) = (r * ( vol A))

    proof

      let f be Function of A, REAL ;

      let r;

      

       A1: ( chi (A,A)) is Function of A, REAL by FUNCT_2: 68, RFUNCT_1: 62;

      

       A2: ( integral ( chi (A,A))) = ( vol A) by Th2;

      assume ( rng f) = {r};

      then

       A3: f = (r (#) ( chi (A,A))) by Th3;

      

       A4: ( rng ( chi (A,A))) is real-bounded by INTEGRA1: 17;

      then

       A5: (( chi (A,A)) | A) is bounded_above by INTEGRA1: 14;

      

       A6: (( chi (A,A)) | A) is bounded_below by A4, INTEGRA1: 12;

      ( chi (A,A)) is integrable by Th2;

      hence thesis by A3, A2, A1, A5, A6, INTEGRA2: 31;

    end;

    theorem :: INTEGRA4:5

    

     Th5: for r holds ex f be Function of A, REAL st ( rng f) = {r} & (f | A) is bounded

    proof

      let r;

      (r (#) ( chi (A,A))) is total by Th3;

      then

      reconsider f = (r (#) ( chi (A,A))) as Function of A, REAL ;

      

       A1: ( rng f) = {r} by Th3;

      then

       A2: (f | A) is bounded_below by INTEGRA1: 12;

      (f | A) is bounded_above by A1, INTEGRA1: 14;

      hence thesis by A1, A2;

    end;

    

     Lm1: 0 in REAL by XREAL_0:def 1;

    

     Lm2: for f be PartFunc of A, REAL , D be Element of ( divs A) st ( vol A) = 0 holds f is upper_integrable & ( upper_integral f) = 0

    proof

      let f be PartFunc of A, REAL ;

      let D be Element of ( divs A);

      (( divs A) /\ ( dom ( upper_sum_set f))) = (( divs A) /\ ( divs A)) by FUNCT_2:def 1;

      then

       A1: ( divs A) meets ( dom ( upper_sum_set f)) by XBOOLE_0:def 7;

      assume

       A2: ( vol A) = 0 ;

      

       A3: for D1 be Element of ( divs A) st D1 in (( divs A) /\ ( dom ( upper_sum_set f))) holds (( upper_sum_set f) /. D1) = 0

      proof

        let D1 be Element of ( divs A);

        reconsider D2 = D1 as Division of A by INTEGRA1:def 3;

        

         A4: ( len ( upper_volume (f,D2))) = ( len D2) by INTEGRA1:def 6

        .= 1 by A2, Th1;

        

         A5: ( len D2) = 1 by A2, Th1;

        then 1 in ( Seg ( len D1)) by FINSEQ_1: 1;

        then

         A6: 1 in ( dom D1) by FINSEQ_1:def 3;

        ( rng D2) <> {} ;

        then

         A7: 1 in ( dom D2) by FINSEQ_3: 32;

        

        then

         A8: ( upper_bound ( divset (D2,( len D2)))) = (D2 . ( len D2)) by A5, INTEGRA1:def 4

        .= ( upper_bound A) by INTEGRA1:def 2;

        ( divset (D2,1)) = [.( lower_bound ( divset (D2,( len D2)))), ( upper_bound ( divset (D2,( len D2)))).] by A5, INTEGRA1: 4

        .= [.( lower_bound A), ( upper_bound A).] by A5, A7, A8, INTEGRA1:def 4;

        then ( divset (D2,1)) = A by INTEGRA1: 4;

        

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

        .= 0 by A2;

        then

         A9: ( upper_volume (f,D2)) = <* 0 qua Real*> by A4, FINSEQ_1: 40;

        assume D1 in (( divs A) /\ ( dom ( upper_sum_set f)));

        (( upper_sum_set f) /. D1) = (( upper_sum_set f) . D1)

        .= ( upper_sum (f,D2)) by INTEGRA1:def 10

        .= ( Sum ( upper_volume (f,D2))) by INTEGRA1:def 8;

        hence thesis by A9, FINSOP_1: 11, Lm1;

      end;

      then (( upper_sum_set f) | ( divs A)) is constant by PARTFUN2: 35, Lm1;

      then

      consider x be Element of REAL such that

       A10: ( rng (( upper_sum_set f) | ( divs A))) = {x} by A1, PARTFUN2: 37;

      thus f is upper_integrable by A10, INTEGRA1:def 12;

       0 in ( rng ( upper_sum_set f))

      proof

        set D1 = the Element of ( divs A);

        D1 in ( divs A);

        then

         A11: D1 in ( dom ( upper_sum_set f)) by FUNCT_2:def 1;

        then

         A12: (( upper_sum_set f) . D1) in ( rng ( upper_sum_set f)) by FUNCT_1:def 3;

        

         A13: (( upper_sum_set f) . D1) = (( upper_sum_set f) /. D1);

        D1 in (( divs A) /\ ( dom ( upper_sum_set f))) by A11, XBOOLE_0:def 4;

        hence thesis by A3, A12, A13;

      end;

      then

       A14: x = 0 by A10, TARSKI:def 1;

      ( rng ( upper_sum_set f)) = {x} by A10;

      then ( lower_bound ( rng ( upper_sum_set f))) = 0 by A14, SEQ_4: 9;

      hence thesis by INTEGRA1:def 14;

    end;

    

     Lm3: for f be PartFunc of A, REAL , D be Element of ( divs A) st ( vol A) = 0 holds f is lower_integrable & ( lower_integral f) = 0

    proof

      let f be PartFunc of A, REAL ;

      let D be Element of ( divs A);

      (( divs A) /\ ( dom ( lower_sum_set f))) = (( divs A) /\ ( divs A)) by FUNCT_2:def 1;

      then

       A1: ( divs A) meets ( dom ( lower_sum_set f)) by XBOOLE_0:def 7;

      assume

       A2: ( vol A) = 0 ;

      

       A3: for D1 be Element of ( divs A) st D1 in (( divs A) /\ ( dom ( lower_sum_set f))) holds (( lower_sum_set f) /. D1) = ( In ( 0 , REAL ))

      proof

        let D1 be Element of ( divs A);

        reconsider D2 = D1 as Division of A by INTEGRA1:def 3;

        

         A4: ( len ( lower_volume (f,D2))) = ( len D2) by INTEGRA1:def 7

        .= 1 by A2, Th1;

        

         A5: ( len D2) = 1 by A2, Th1;

        then 1 in ( Seg ( len D2)) by FINSEQ_1: 1;

        then

         A6: 1 in ( dom D2) by FINSEQ_1:def 3;

        ( rng D2) <> {} ;

        then

         A7: 1 in ( dom D2) by FINSEQ_3: 32;

        

        then

         A8: ( upper_bound ( divset (D2,( len D2)))) = (D2 . ( len D2)) by A5, INTEGRA1:def 4

        .= ( upper_bound A) by INTEGRA1:def 2;

        ( divset (D2,1)) = [.( lower_bound ( divset (D2,( len D2)))), ( upper_bound ( divset (D2,( len D2)))).] by A5, INTEGRA1: 4

        .= [.( lower_bound A), ( upper_bound A).] by A5, A7, A8, INTEGRA1:def 4;

        then ( divset (D2,1)) = A by INTEGRA1: 4;

        

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

        .= 0 by A2;

        then

         A9: ( lower_volume (f,D2)) = <*( In ( 0 , REAL ))*> by A4, FINSEQ_1: 40;

        assume D1 in (( divs A) /\ ( dom ( lower_sum_set f)));

        (( lower_sum_set f) /. D1) = (( lower_sum_set f) . D1)

        .= ( lower_sum (f,D2)) by INTEGRA1:def 11

        .= ( Sum ( lower_volume (f,D2))) by INTEGRA1:def 9;

        hence thesis by A9, FINSOP_1: 11;

      end;

      then (( lower_sum_set f) | ( divs A)) is constant by PARTFUN2: 35;

      then

      consider x be Element of REAL such that

       A10: ( rng (( lower_sum_set f) | ( divs A))) = {x} by A1, PARTFUN2: 37;

      thus f is lower_integrable by A10, INTEGRA1:def 13;

       0 in ( rng ( lower_sum_set f))

      proof

        set D1 = the Element of ( divs A);

        D1 in ( divs A);

        then

         A11: D1 in ( dom ( lower_sum_set f)) by FUNCT_2:def 1;

        then

         A12: (( lower_sum_set f) . D1) in ( rng ( lower_sum_set f)) by FUNCT_1:def 3;

        

         A13: (( lower_sum_set f) . D1) = (( lower_sum_set f) /. D1);

        D1 in (( divs A) /\ ( dom ( lower_sum_set f))) by A11, XBOOLE_0:def 4;

        hence thesis by A3, A12, A13;

      end;

      then

       A14: x = 0 by A10, TARSKI:def 1;

      ( rng ( lower_sum_set f)) = {x} by A10;

      then ( upper_bound ( rng ( lower_sum_set f))) = 0 by A14, SEQ_4: 9;

      hence thesis by INTEGRA1:def 15;

    end;

    theorem :: INTEGRA4:6

    

     Th6: for f be PartFunc of A, REAL st ( vol A) = 0 holds f is integrable & ( integral f) = 0

    proof

      let f be PartFunc of A, REAL ;

      assume

       A1: ( vol A) = 0 ;

      then

       A2: ( upper_integral f) = 0 by Lm2;

      

       A3: ( lower_integral f) = 0 by A1, Lm3;

      

       A4: f is lower_integrable by A1, Lm3;

      f is upper_integrable by A1, Lm2;

      hence thesis by A2, A4, A3, INTEGRA1:def 16, INTEGRA1:def 17;

    end;

    theorem :: INTEGRA4:7

    for f be Function of A, REAL st (f | A) is bounded & f is integrable holds ex a st ( lower_bound ( rng f)) <= a & a <= ( upper_bound ( rng f)) & ( integral f) = (a * ( vol A))

    proof

      let f be Function of A, REAL ;

      consider g be Function of A, REAL such that

       A1: ( rng g) = {( lower_bound ( rng f))} and

       A2: (g | A) is bounded by Th5;

      consider h be Function of A, REAL such that

       A3: ( rng h) = {( upper_bound ( rng f))} and

       A4: (h | A) is bounded by Th5;

      

       A5: ( integral g) = (( lower_bound ( rng f)) * ( vol A)) by A1, Th4;

      assume

       A6: (f | A) is bounded;

      

       A7: for x st x in ( dom f) holds ( lower_bound ( rng f)) <= (f . x) & (f . x) <= ( upper_bound ( rng f))

      proof

        let x;

        assume x in ( dom f);

        then

         A8: (f . x) in ( rng f) by FUNCT_1:def 3;

        

         A9: ( rng f) is bounded_below by A6, INTEGRA1: 11;

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

        hence thesis by A9, A8, SEQ_4:def 1, SEQ_4:def 2;

      end;

      

       A10: for x st x in A holds (f . x) <= (h . x)

      proof

        let x;

        assume

         A11: x in A;

        ( dom h) = A by FUNCT_2:def 1;

        then

         A12: (h . x) in ( rng h) by A11, FUNCT_1:def 3;

        ( dom f) = A by FUNCT_2:def 1;

        then (f . x) <= ( upper_bound ( rng f)) by A7, A11;

        hence thesis by A3, A12, TARSKI:def 1;

      end;

      

       A13: for x st x in A holds (g . x) <= (f . x)

      proof

        let x;

        assume

         A14: x in A;

        ( dom g) = A by FUNCT_2:def 1;

        then

         A15: (g . x) in ( rng g) by A14, FUNCT_1:def 3;

        ( dom f) = A by FUNCT_2:def 1;

        then ( lower_bound ( rng f)) <= (f . x) by A7, A14;

        hence thesis by A1, A15, TARSKI:def 1;

      end;

      assume

       A16: f is integrable;

      

       A17: ( integral h) = (( upper_bound ( rng f)) * ( vol A)) by A3, Th4;

      

       A18: h is integrable by A3, Th4;

      

       A19: g is integrable by A1, Th4;

      now

        per cases ;

          suppose

           A20: ( vol A) <> 0 ;

          reconsider a = (( integral f) / ( vol A)) as Real;

          

           A21: ( integral f) = (a * ( vol A)) by A20, XCMPLX_1: 87;

          

           A22: ( vol A) >= 0 by INTEGRA1: 9;

          then

           A23: (( integral f) / ( vol A)) <= ( upper_bound ( rng f)) by A6, A16, A4, A18, A17, A10, A20, INTEGRA2: 34, XREAL_1: 79;

          ( lower_bound ( rng f)) <= (( integral f) / ( vol A)) by A6, A16, A2, A19, A5, A13, A20, A22, INTEGRA2: 34, XREAL_1: 77;

          hence thesis by A23, A21;

        end;

          suppose

           A24: ( vol A) = 0 ;

          

           A25: ( lower_bound ( rng f)) <= ( upper_bound ( rng f))

          proof

            ( dom f) = A by FUNCT_2:def 1;

            then

            consider x be Element of REAL such that

             A26: x in ( dom f) by SUBSET_1: 4;

            

             A27: (f . x) <= ( upper_bound ( rng f)) by A7, A26;

            ( lower_bound ( rng f)) <= (f . x) by A7, A26;

            hence thesis by A27, XXREAL_0: 2;

          end;

          ( integral f) = (( lower_bound ( rng f)) * ( vol A)) by A24, Th6;

          hence thesis by A25;

        end;

      end;

      hence thesis;

    end;

    begin

    theorem :: INTEGRA4:8

    

     Th8: for f be Function of A, REAL , T be DivSequence of A st (f | A) is bounded & ( delta T) is convergent & ( lim ( delta T)) = 0 holds ( lower_sum (f,T)) is convergent & ( lim ( lower_sum (f,T))) = ( lower_integral f)

    proof

      let f be Function of A, REAL ;

      let T be DivSequence of A;

      assume

       A1: (f | A) is bounded;

      assume

       A2: ( delta T) is convergent;

      assume

       A3: ( lim ( delta T)) = 0 ;

      now

        per cases ;

          suppose

           A4: ( vol A) <> 0 ;

          for n be Nat holds (( delta T) . n) <> 0

          proof

            let n be Nat;

            reconsider nn = n as Element of NAT by ORDINAL1:def 12;

            reconsider mm = ( rng ( upper_volume (( chi (A,A)),(T . nn)))) as non empty finite Subset of REAL ;

            reconsider D = (T . nn) as Division of A;

            assume (( delta T) . n) = 0 ;

            then ( delta (T . nn)) = 0 by INTEGRA3:def 2;

            then

             A5: ( max mm) = 0 by INTEGRA3:def 1;

            

             A6: for k be Element of NAT st k in ( dom D) holds ( vol ( divset (D,k))) = 0

            proof

              let k be Element of NAT ;

              assume

               A7: k in ( dom D);

              then k in ( Seg ( len D)) by FINSEQ_1:def 3;

              then k in ( Seg ( len ( upper_volume (( chi (A,A)),D)))) by INTEGRA1:def 6;

              then k in ( dom ( upper_volume (( chi (A,A)),D))) by FINSEQ_1:def 3;

              then (( upper_volume (( chi (A,A)),D)) . k) in ( rng ( upper_volume (( chi (A,A)),D))) by FUNCT_1:def 3;

              then (( upper_volume (( chi (A,A)),D)) . k) <= 0 by A5, XXREAL_2:def 8;

              then ( vol ( divset (D,k))) <= 0 by A7, INTEGRA1: 20;

              hence thesis by INTEGRA1: 9;

            end;

            

             A8: for j be Nat holds 1 <= j & j <= ( len ( upper_volume (( chi (A,A)),D))) implies (( upper_volume (( chi (A,A)),D)) . j) = ((( len D) |-> 0 qua Real) . j)

            proof

              let j be Nat;

              assume that

               A9: 1 <= j and

               A10: j <= ( len ( upper_volume (( chi (A,A)),D)));

              j in ( Seg ( len ( upper_volume (( chi (A,A)),D)))) by A9, A10, FINSEQ_1: 1;

              then

               A11: j in ( Seg ( len D)) by INTEGRA1:def 6;

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

              then

               A12: (( upper_volume (( chi (A,A)),D)) . j) = ( vol ( divset (D,j))) by INTEGRA1: 20;

              j in ( dom D) by A11, FINSEQ_1:def 3;

              then (( upper_volume (( chi (A,A)),D)) . j) = 0 by A6, A12;

              hence thesis by A11, FUNCOP_1: 7;

            end;

            ( len ( upper_volume (( chi (A,A)),D))) = ( len D) by INTEGRA1:def 6;

            then ( len ( upper_volume (( chi (A,A)),D))) = ( len (( len D) |-> 0 qua Real)) by CARD_1:def 7;

            then ( upper_volume (( chi (A,A)),D)) = (( len D) |-> 0 qua Real) by A8, FINSEQ_1: 14;

            then ( Sum ( upper_volume (( chi (A,A)),D))) = 0 by RVSUM_1: 81;

            hence contradiction by A4, INTEGRA1: 24;

          end;

          then ( delta T) is non-zero by SEQ_1: 5;

          then ( delta T) is 0 -convergent non-zero by A2, A3, FDIFF_1:def 1;

          hence thesis by A1, A4, INTEGRA3: 25;

        end;

          suppose

           A13: ( vol A) = 0 ;

          

           A14: for n be Nat holds (( lower_sum (f,T)) . n) = ( In ( 0 , REAL ))

          proof

            let n be Nat;

            reconsider nn = n as Element of NAT by ORDINAL1:def 12;

            reconsider D = (T . nn) as Division of A;

            

             A15: ( len D) = 1 by A13, Th1;

            then

             A16: ( len ( lower_volume (f,D))) = 1 by INTEGRA1:def 7;

            ( rng D) <> {} ;

            then

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

            

            then

             A18: ( upper_bound ( divset (D,( len D)))) = (D . ( len D)) by A15, INTEGRA1:def 4

            .= ( upper_bound A) by INTEGRA1:def 2;

            1 in ( Seg ( len D)) by A15, FINSEQ_1: 1;

            then

             A19: 1 in ( dom D) by FINSEQ_1:def 3;

            ( divset (D,1)) = [.( lower_bound ( divset (D,( len D)))), ( upper_bound ( divset (D,( len D)))).] by A15, INTEGRA1: 4

            .= [.( lower_bound A), ( upper_bound A).] by A15, A17, A18, INTEGRA1:def 4;

            then ( divset (D,1)) = A by INTEGRA1: 4;

            

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

            .= 0 by A13;

            then ( lower_volume (f,D)) = <* 0 qua Real*> by A16, FINSEQ_1: 40;

            then ( Sum ( lower_volume (f,D))) = ( In ( 0 , REAL )) by FINSOP_1: 11;

            then ( lower_sum (f,D)) = 0 by INTEGRA1:def 9;

            hence thesis by INTEGRA2:def 3;

          end;

          then

           A20: ( lower_sum (f,T)) is constant by VALUED_0:def 18;

          hence ( lower_sum (f,T)) is convergent;

          (( lower_sum (f,T)) . 1) = 0 by A14;

          then ( lim ( lower_sum (f,T))) = 0 by A20, SEQ_4: 25;

          hence ( lim ( lower_sum (f,T))) = ( lower_integral f) by A13, Lm3;

        end;

      end;

      hence thesis;

    end;

    theorem :: INTEGRA4:9

    

     Th9: for f be Function of A, REAL , T be DivSequence of A st (f | A) is bounded & ( delta T) is convergent & ( lim ( delta T)) = 0 holds ( upper_sum (f,T)) is convergent & ( lim ( upper_sum (f,T))) = ( upper_integral f)

    proof

      let f be Function of A, REAL ;

      let T be DivSequence of A;

      assume

       A1: (f | A) is bounded;

      assume

       A2: ( delta T) is convergent;

      assume

       A3: ( lim ( delta T)) = 0 ;

      now

        per cases ;

          suppose

           A4: ( vol A) <> 0 ;

          for n be Nat holds (( delta T) . n) <> 0

          proof

            let n be Nat;

            reconsider nn = n as Element of NAT by ORDINAL1:def 12;

            reconsider D = (T . nn) as Division of A;

            assume (( delta T) . n) = 0 ;

            then ( delta (T . nn)) = 0 by INTEGRA3:def 2;

            then

             A5: ( max ( rng ( upper_volume (( chi (A,A)),(T . nn))))) = 0 by INTEGRA3:def 1;

            

             A6: for k be Element of NAT st k in ( dom D) holds ( vol ( divset (D,k))) = 0

            proof

              let k be Element of NAT ;

              assume

               A7: k in ( dom D);

              then k in ( Seg ( len D)) by FINSEQ_1:def 3;

              then k in ( Seg ( len ( upper_volume (( chi (A,A)),D)))) by INTEGRA1:def 6;

              then k in ( dom ( upper_volume (( chi (A,A)),D))) by FINSEQ_1:def 3;

              then (( upper_volume (( chi (A,A)),D)) . k) in ( rng ( upper_volume (( chi (A,A)),D))) by FUNCT_1:def 3;

              then (( upper_volume (( chi (A,A)),D)) . k) <= 0 by A5, XXREAL_2:def 8;

              then ( vol ( divset (D,k))) <= 0 by A7, INTEGRA1: 20;

              hence thesis by INTEGRA1: 9;

            end;

            

             A8: for j be Nat holds 1 <= j & j <= ( len ( upper_volume (( chi (A,A)),D))) implies (( upper_volume (( chi (A,A)),D)) . j) = ((( len D) |-> 0 qua Real) . j)

            proof

              let j be Nat;

              assume that

               A9: 1 <= j and

               A10: j <= ( len ( upper_volume (( chi (A,A)),D)));

              j in ( Seg ( len ( upper_volume (( chi (A,A)),D)))) by A9, A10, FINSEQ_1: 1;

              then

               A11: j in ( Seg ( len D)) by INTEGRA1:def 6;

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

              then

               A12: (( upper_volume (( chi (A,A)),D)) . j) = ( vol ( divset (D,j))) by INTEGRA1: 20;

              j in ( dom D) by A11, FINSEQ_1:def 3;

              then (( upper_volume (( chi (A,A)),D)) . j) = 0 by A6, A12;

              hence thesis by A11, FUNCOP_1: 7;

            end;

            ( len ( upper_volume (( chi (A,A)),D))) = ( len D) by INTEGRA1:def 6;

            then ( len ( upper_volume (( chi (A,A)),D))) = ( len (( len D) |-> 0 qua Real)) by CARD_1:def 7;

            then ( upper_volume (( chi (A,A)),D)) = (( len D) |-> 0 qua Real) by A8, FINSEQ_1: 14;

            then ( Sum ( upper_volume (( chi (A,A)),D))) = 0 by RVSUM_1: 81;

            hence contradiction by A4, INTEGRA1: 24;

          end;

          then ( delta T) is non-zero by SEQ_1: 5;

          then ( delta T) is 0 -convergent non-zero by A2, A3, FDIFF_1:def 1;

          hence thesis by A1, A4, INTEGRA3: 26;

        end;

          suppose

           A13: ( vol A) = 0 ;

          

           A14: for n be Nat holds (( upper_sum (f,T)) . n) = ( In ( 0 , REAL ))

          proof

            let n be Nat;

            reconsider nn = n as Element of NAT by ORDINAL1:def 12;

            reconsider D = (T . nn) as Division of A;

            

             A15: ( len D) = 1 by A13, Th1;

            then

             A16: ( len ( upper_volume (f,D))) = 1 by INTEGRA1:def 6;

            ( rng D) <> {} ;

            then

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

            

            then

             A18: ( upper_bound ( divset (D,( len D)))) = (D . ( len D)) by A15, INTEGRA1:def 4

            .= ( upper_bound A) by INTEGRA1:def 2;

            1 in ( Seg ( len D)) by A15, FINSEQ_1: 1;

            then

             A19: 1 in ( dom D) by FINSEQ_1:def 3;

            ( divset (D,1)) = [.( lower_bound ( divset (D,( len D)))), ( upper_bound ( divset (D,( len D)))).] by A15, INTEGRA1: 4

            .= [.( lower_bound A), ( upper_bound A).] by A15, A17, A18, INTEGRA1:def 4;

            then ( divset (D,1)) = A by INTEGRA1: 4;

            

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

            .= 0 by A13;

            then ( upper_volume (f,D)) = <* 0 qua Real*> by A16, FINSEQ_1: 40;

            then ( Sum ( upper_volume (f,D))) = ( In ( 0 , REAL )) by FINSOP_1: 11;

            then ( upper_sum (f,D)) = 0 by INTEGRA1:def 8;

            hence thesis by INTEGRA2:def 2;

          end;

          then

           A20: ( upper_sum (f,T)) is constant by VALUED_0:def 18;

          hence ( upper_sum (f,T)) is convergent;

          (( upper_sum (f,T)) . 1) = 0 by A14;

          then ( lim ( upper_sum (f,T))) = 0 by A20, SEQ_4: 25;

          hence ( lim ( upper_sum (f,T))) = ( upper_integral f) by A13, Lm2;

        end;

      end;

      hence thesis;

    end;

    theorem :: INTEGRA4:10

    

     Th10: for f be Function of A, REAL st (f | A) is bounded holds f is upper_integrable & f is lower_integrable

    proof

      let f be Function of A, REAL ;

      assume

       A1: (f | A) is bounded;

      (( lower_bound ( rng f)) * ( vol A)) is LowerBound of ( rng ( upper_sum_set f))

      proof

        let r be ExtReal;

        assume r in ( rng ( upper_sum_set f));

        then

        consider D be Element of ( divs A) such that D in ( dom ( upper_sum_set f)) and

         A2: (( upper_sum_set f) . D) = r by PARTFUN1: 3;

        reconsider D as Division of A by INTEGRA1:def 3;

        r = ( upper_sum (f,D)) by A2, INTEGRA1:def 10;

        then

         A3: ( lower_sum (f,D)) <= r by A1, INTEGRA1: 28;

        (( lower_bound ( rng f)) * ( vol A)) <= ( lower_sum (f,D)) by A1, INTEGRA1: 25;

        hence thesis by A3, XXREAL_0: 2;

      end;

      then ( rng ( upper_sum_set f)) is bounded_below;

      hence f is upper_integrable by INTEGRA1:def 12;

      (( upper_bound ( rng f)) * ( vol A)) is UpperBound of ( rng ( lower_sum_set f))

      proof

        let r be ExtReal;

        assume r in ( rng ( lower_sum_set f));

        then

        consider D be Element of ( divs A) such that D in ( dom ( lower_sum_set f)) and

         A4: (( lower_sum_set f) . D) = r by PARTFUN1: 3;

        reconsider D as Division of A by INTEGRA1:def 3;

        r = ( lower_sum (f,D)) by A4, INTEGRA1:def 11;

        then

         A5: ( upper_sum (f,D)) >= r by A1, INTEGRA1: 28;

        (( upper_bound ( rng f)) * ( vol A)) >= ( upper_sum (f,D)) by A1, INTEGRA1: 27;

        hence thesis by A5, XXREAL_0: 2;

      end;

      then ( rng ( lower_sum_set f)) is bounded_above;

      hence thesis by INTEGRA1:def 13;

    end;

    definition

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

      :: INTEGRA4:def1

      pred IT divide_into_equal n means ( len IT) = n & for i st i in ( dom IT) holds (IT . i) = (( lower_bound A) + ((( vol A) / ( len IT)) * i));

    end

    

     Lm4: for n st n > 0 & ( vol A) > 0 holds ex D be Division of A st ( len D) = n & for i st i in ( dom D) holds (D . i) = (( lower_bound A) + ((( vol A) / n) * i))

    proof

      let n;

      assume that

       A1: n > 0 and

       A2: ( vol A) > 0 ;

      deffunc F( Nat) = ( In ((( lower_bound A) + ((( vol A) / n) * $1)), REAL ));

      consider D be FinSequence of REAL such that

       A3: ( len D) = n & for i be Nat st i in ( dom D) holds (D . i) = F(i) from FINSEQ_2:sch 1;

      

       A4: for i,j be Nat st i in ( dom D) & j in ( dom D) & i < j holds (D . i) < (D . j)

      proof

        let i,j be Nat;

        assume that

         A5: i in ( dom D) and

         A6: j in ( dom D) and

         A7: i < j;

        (( vol A) / n) > 0 by A1, A2, XREAL_1: 139;

        then ((( vol A) / n) * i) < ((( vol A) / n) * j) by A7, XREAL_1: 68;

        then F(i) < (( lower_bound A) + ((( vol A) / n) * j)) by XREAL_1: 6;

        then (D . i) < F(j) by A3, A5;

        hence thesis by A3, A6;

      end;

      

       A8: ( dom D) = ( Seg n) by A3, FINSEQ_1:def 3;

      reconsider D as non empty increasing FinSequence of REAL by A1, A3, A4, SEQM_3:def 1;

      (D . ( len D)) = F(n) by A3, A8, FINSEQ_1: 3;

      then

       A9: (D . ( len D)) = (( lower_bound A) + ( vol A)) by A1, XCMPLX_1: 87;

      for x1 be object st x1 in ( rng D) holds x1 in A

      proof

        let x1 be object;

        

         A10: (( lower_bound A) + ( vol A)) = (( lower_bound A) + (( upper_bound A) - ( lower_bound A))) by INTEGRA1:def 5

        .= ( upper_bound A);

        assume

         A11: x1 in ( rng D);

        then

        reconsider x1 as Real;

        consider i be Element of NAT such that

         A12: i in ( dom D) and

         A13: (D . i) = x1 by A11, PARTFUN1: 3;

        

         A14: 1 <= i by A12, FINSEQ_3: 25;

        i <= ( len D) by A12, FINSEQ_3: 25;

        then ((( vol A) / n) * i) <= ((( vol A) / n) * n) by A2, A3, XREAL_1: 64;

        then ((( vol A) / n) * i) <= ( vol A) by A1, XCMPLX_1: 87;

        then

         A15: (( lower_bound A) + ((( vol A) / n) * i)) <= (( lower_bound A) + ( vol A)) by XREAL_1: 6;

        (( vol A) / n) > 0 by A1, A2, XREAL_1: 139;

        then

         A16: ( lower_bound A) <= (( lower_bound A) + ((( vol A) / n) * i)) by A14, XREAL_1: 29, XREAL_1: 129;

        x1 = F(i) by A3, A12, A13;

        hence thesis by A16, A15, A10, INTEGRA2: 1;

      end;

      then

       A17: ( rng D) c= A by TARSKI:def 3;

      ( vol A) = (( upper_bound A) - ( lower_bound A)) by INTEGRA1:def 5;

      then

      reconsider D as Division of A by A17, A9, INTEGRA1:def 2;

      take D;

      thus ( len D) = n by A3;

      let i;

      assume i in ( dom D);

      then (D . i) = F(i) by A3;

      hence thesis;

    end;

    

     Lm5: ( vol A) > 0 implies ex T be DivSequence of A st ( delta T) is convergent & ( lim ( delta T)) = 0

    proof

      defpred P[ set, set] means ex n be Nat, e be Division of A st n = $1 & e = $2 & e divide_into_equal (n + 1);

      assume

       A1: ( vol A) > 0 ;

      

       A2: for n be Element of NAT holds ex D be Element of ( divs A) st P[n, D]

      proof

        let n be Element of NAT ;

        consider D be Division of A such that

         A3: ( len D) = (n + 1) and

         A4: for i st i in ( dom D) holds (D . i) = (( lower_bound A) + ((( vol A) / (n + 1)) * i)) by A1, Lm4;

        

         A5: D is Element of ( divs A) by INTEGRA1:def 3;

        D divide_into_equal (n + 1) by A3, A4;

        hence thesis by A5;

      end;

      consider T be sequence of ( divs A) such that

       A6: for n be Element of NAT holds P[n, (T . n)] from FUNCT_2:sch 3( A2);

      reconsider T as DivSequence of A;

      

       A7: for i be Element of NAT holds (( delta T) . i) = (( vol A) / (i + 1))

      proof

        let i be Element of NAT ;

        (( delta T) . i) = ( delta (T . i)) by INTEGRA3:def 2;

        then

         A8: (( delta T) . i) = ( max ( rng ( upper_volume (( chi (A,A)),(T . i))))) by INTEGRA3:def 1;

        for x1 be object st x1 in ( rng ( upper_volume (( chi (A,A)),(T . i)))) holds x1 in {(( vol A) / (i + 1))}

        proof

          reconsider D = (T . i) as Division of A;

          let x1 be object;

          assume x1 in ( rng ( upper_volume (( chi (A,A)),(T . i))));

          then

          consider k be Element of NAT such that

           A9: k in ( dom ( upper_volume (( chi (A,A)),(T . i)))) and

           A10: (( upper_volume (( chi (A,A)),(T . i))) . k) = x1 by PARTFUN1: 3;

          

           A11: ex n be Nat, e be Division of A st n = i & e = D & e divide_into_equal (n + 1) by A6;

          k in ( Seg ( len ( upper_volume (( chi (A,A)),(T . i))))) by A9, FINSEQ_1:def 3;

          then

           A12: k in ( Seg ( len D)) by INTEGRA1:def 6;

          

           A13: (( upper_bound ( divset (D,k))) - ( lower_bound ( divset (D,k)))) = (( vol A) / (i + 1))

          proof

            

             A14: 1 <= k by A9, FINSEQ_3: 25;

            now

              per cases by A14, XXREAL_0: 1;

                suppose

                 A15: k = 1;

                

                 A16: 1 in ( dom D) by A12, A15, FINSEQ_1:def 3;

                then ( upper_bound ( divset (D,k))) = (D . 1) by A15, INTEGRA1:def 4;

                then ( upper_bound ( divset (D,k))) = (( lower_bound A) + ((( vol A) / (i + 1)) * 1)) by A11, A16;

                

                then (( upper_bound ( divset (D,k))) - ( lower_bound ( divset (D,k)))) = ((( lower_bound A) + (( vol A) / (i + 1))) - ( lower_bound A)) by A15, A16, INTEGRA1:def 4

                .= ((( vol A) / (i + 1)) - (( lower_bound A) - ( lower_bound A)));

                hence thesis;

              end;

                suppose

                 A17: k > 1;

                

                 A18: k in ( dom D) by A12, FINSEQ_1:def 3;

                then

                 A19: ( lower_bound ( divset (D,k))) = (D . (k - 1)) by A17, INTEGRA1:def 4;

                (k - 1) in ( dom D) by A17, A18, INTEGRA1: 7;

                then

                 A20: (D . (k - 1)) = (( lower_bound A) + ((( vol A) / ( len D)) * (k - 1))) by A11;

                

                 A21: ( upper_bound ( divset (D,k))) = (D . k) by A17, A18, INTEGRA1:def 4;

                (D . k) = (( lower_bound A) + ((( vol A) / ( len D)) * k)) by A11, A18;

                hence thesis by A11, A19, A21, A20;

              end;

            end;

            hence thesis;

          end;

          k in ( dom D) by A12, FINSEQ_1:def 3;

          then x1 = ( vol ( divset (D,k))) by A10, INTEGRA1: 20;

          then x1 = (( upper_bound ( divset (D,k))) - ( lower_bound ( divset (D,k)))) by INTEGRA1:def 5;

          hence thesis by A13, TARSKI:def 1;

        end;

        then

         A22: ( rng ( upper_volume (( chi (A,A)),(T . i)))) c= {(( vol A) / (i + 1))} by TARSKI:def 3;

        for x1 be object st x1 in {(( vol A) / (i + 1))} holds x1 in ( rng ( upper_volume (( chi (A,A)),(T . i))))

        proof

          reconsider D = (T . i) as Division of A;

          let x1 be object;

          

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

          

           A24: ex n be Nat, e be Division of A st n = i & e = D & e divide_into_equal (n + 1) by A6;

          ( rng D) <> {} ;

          then

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

          then ( upper_bound ( divset (D,1))) = (D . 1) by INTEGRA1:def 4;

          then ( upper_bound ( divset (D,1))) = (( lower_bound A) + ((( vol A) / ( len D)) * 1)) by A25, A24;

          

          then

           A26: ( vol ( divset (D,1))) = ((( lower_bound A) + (( vol A) / ( len D))) - ( lower_bound A)) by A25, A23, INTEGRA1:def 4

          .= (( vol A) / ( len D));

          assume x1 in {(( vol A) / (i + 1))};

          then

           A27: x1 = (( vol A) / (i + 1)) by TARSKI:def 1;

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

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

          then 1 in ( dom ( upper_volume (( chi (A,A)),D))) by FINSEQ_1:def 3;

          then

           A28: (( upper_volume (( chi (A,A)),D)) . 1) in ( rng ( upper_volume (( chi (A,A)),D))) by FUNCT_1:def 3;

          (( upper_volume (( chi (A,A)),D)) . 1) = ( vol ( divset (D,1))) by A25, INTEGRA1: 20;

          hence thesis by A27, A28, A24, A26;

        end;

        then {(( vol A) / (i + 1))} c= ( rng ( upper_volume (( chi (A,A)),(T . i)))) by TARSKI:def 3;

        then ( rng ( upper_volume (( chi (A,A)),(T . i)))) = {(( vol A) / (i + 1))} by A22, XBOOLE_0:def 10;

        then (( delta T) . i) in {(( vol A) / (i + 1))} by A8, XXREAL_2:def 8;

        hence thesis by TARSKI:def 1;

      end;

      

       A29: for a st 0 < a holds ex i st |.((( delta T) . i) - 0 ).| < a

      proof

        let a;

        

         A30: ( vol A) >= 0 by INTEGRA1: 9;

        reconsider i1 = ( [\(( vol A) / a)/] + 1) as Integer;

        assume

         A31: 0 < a;

        then ( [\(( vol A) / a)/] + 1) > 0 by A30, INT_1: 29;

        then

        reconsider i1 as Element of NAT by INT_1: 3;

        i1 < (i1 + 1) by NAT_1: 13;

        then (( vol A) / a) < (1 * (i1 + 1)) by INT_1: 29, XXREAL_0: 2;

        then

         A32: (( vol A) / (i1 + 1)) < (1 * a) by A31, XREAL_1: 113;

        

         A33: (( delta T) . i1) = (( vol A) / (i1 + 1)) by A7;

        ((( vol A) / (i1 + 1)) - 0 ) = |.((( vol A) / (i1 + 1)) - 0 ).| by A30, ABSVALUE:def 1;

        hence thesis by A32, A33;

      end;

      

       A34: for i be Nat holds (( delta T) . i) >= 0

      proof

        let i be Nat;

        reconsider ii = i as Element of NAT by ORDINAL1:def 12;

        (( delta T) . i) = ( delta (T . ii)) by INTEGRA3:def 2;

        hence thesis by INTEGRA3: 9;

      end;

      

       A35: for i,j be Nat st i <= j holds (( delta T) . i) >= (( delta T) . j)

      proof

        let i,j be Nat;

        assume i <= j;

        then

         A36: (i + 1) <= (j + 1) by XREAL_1: 6;

        

         A37: i in NAT & j in NAT by ORDINAL1:def 12;

        ( vol A) >= 0 by INTEGRA1: 9;

        then (( vol A) / (i + 1)) >= (( vol A) / (j + 1)) by A36, XREAL_1: 118;

        then (( delta T) . i) >= (( vol A) / (j + 1)) by A7, A37;

        hence thesis by A7, A37;

      end;

      

       A38: for a be Real st 0 < a holds ex i be Nat st for j be Nat st i <= j holds |.((( delta T) . j) - 0 ).| < a

      proof

        let a be Real;

        assume

         A39: 0 < a;

        consider i such that

         A40: |.((( delta T) . i) - 0 ).| < a by A29, A39;

        (( delta T) . i) >= 0 by A34;

        then

         A41: (( delta T) . i) < a by A40, ABSVALUE:def 1;

        for j be Nat st i <= j holds |.((( delta T) . j) - 0 ).| < a

        proof

          let j be Nat;

          assume i <= j;

          then (( delta T) . j) <= (( delta T) . i) by A35;

          then

           A42: (( delta T) . j) < a by A41, XXREAL_0: 2;

          (( delta T) . j) >= 0 by A34;

          hence thesis by A42, ABSVALUE:def 1;

        end;

        hence thesis;

      end;

      then

       A43: ( delta T) is convergent by SEQ_2:def 6;

      then ( lim ( delta T)) = 0 by A38, SEQ_2:def 7;

      hence thesis by A43;

    end;

    

     Lm6: ( vol A) = 0 implies ex T be DivSequence of A st ( delta T) is convergent & ( lim ( delta T)) = 0

    proof

      set T = the DivSequence of A;

      assume

       A1: ( vol A) = 0 ;

      

       A2: for i be Nat holds (( delta T) . i) = ( In ( 0 , REAL ))

      proof

        let i be Nat;

        reconsider ii = i as Element of NAT by ORDINAL1:def 12;

        reconsider D = (T . ii) as Division of A;

        

         A3: (( delta T) . i) = ( delta D) by INTEGRA3:def 2

        .= ( max ( rng ( upper_volume (( chi (A,A)),D)))) by INTEGRA3:def 1;

        

         A4: ( len D) = 1

        proof

          assume ( len D) <> 1;

          then ( len D) is non trivial by NAT_2:def 1;

          then

           A5: ( len D) >= 2 by NAT_2: 29;

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

          then

           A6: 1 in ( dom D) by FINSEQ_3: 25;

          then

           A7: (D . 1) in A by INTEGRA1: 6;

          then

           A8: ( lower_bound A) <= (D . 1) by INTEGRA2: 1;

          

           A9: 2 in ( dom D) by A5, FINSEQ_3: 25;

          then (D . 2) in A by INTEGRA1: 6;

          then

           A10: (D . 2) <= ( upper_bound A) by INTEGRA2: 1;

          

           A11: (D . 1) <= ( upper_bound A) by A7, INTEGRA2: 1;

          

           A12: (( upper_bound A) - ( lower_bound A)) = 0 by A1, INTEGRA1:def 5;

          (D . 1) < (D . 2) by A6, A9, SEQM_3:def 1;

          hence contradiction by A8, A11, A10, A12, XXREAL_0: 1;

        end;

        for x1 be object st x1 in { 0 } holds x1 in ( rng ( upper_volume (( chi (A,A)),D)))

        proof

          let x1 be object;

          

           A13: 1 in ( Seg ( len D)) by A4, FINSEQ_1: 3;

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

          then

           A14: (( upper_volume (( chi (A,A)),D)) . 1) = ( vol ( divset (D,1))) by INTEGRA1: 20;

          1 in ( Seg ( len ( upper_volume (( chi (A,A)),D)))) by A13, INTEGRA1:def 6;

          then 1 in ( dom ( upper_volume (( chi (A,A)),D))) by FINSEQ_1:def 3;

          then

           A15: (( upper_volume (( chi (A,A)),D)) . 1) in ( rng ( upper_volume (( chi (A,A)),D))) by FUNCT_1:def 3;

          

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

          then ( upper_bound ( divset (D,1))) = (D . ( len D)) by A4, INTEGRA1:def 4;

          then

           A17: ( upper_bound ( divset (D,1))) = ( upper_bound A) by INTEGRA1:def 2;

          ( lower_bound ( divset (D,1))) = ( lower_bound A) by A16, INTEGRA1:def 4;

          

          then

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

          .= 0 by A1, INTEGRA1:def 5;

          assume x1 in { 0 };

          hence thesis by A15, A14, A18, TARSKI:def 1;

        end;

        then

         A19: { 0 } c= ( rng ( upper_volume (( chi (A,A)),D))) by TARSKI:def 3;

        for x1 be object st x1 in ( rng ( upper_volume (( chi (A,A)),D))) holds x1 in { 0 }

        proof

          let x1 be object;

          assume

           A20: x1 in ( rng ( upper_volume (( chi (A,A)),D)));

          then

          consider k be Element of NAT such that

           A21: k in ( dom ( upper_volume (( chi (A,A)),D))) and

           A22: (( upper_volume (( chi (A,A)),D)) . k) = x1 by PARTFUN1: 3;

          reconsider x1 as Real by A20;

          k in ( Seg ( len ( upper_volume (( chi (A,A)),D)))) by A21, FINSEQ_1:def 3;

          then

           A23: k in ( Seg ( len D)) by INTEGRA1:def 6;

          then

           A24: k in ( dom D) by FINSEQ_1:def 3;

          k in ( dom D) by A23, FINSEQ_1:def 3;

          then

           A25: x1 = ( vol ( divset (D,k))) by A22, INTEGRA1: 20;

          then x1 >= 0 by INTEGRA1: 9;

          then x1 = 0 by A1, A25, A24, INTEGRA1: 8, INTEGRA2: 38;

          hence thesis by TARSKI:def 1;

        end;

        then ( rng ( upper_volume (( chi (A,A)),D))) c= { 0 } by TARSKI:def 3;

        then ( rng ( upper_volume (( chi (A,A)),D))) = { 0 } by A19, XBOOLE_0:def 10;

        then (( delta T) . i) in { 0 } by A3, XXREAL_2:def 8;

        hence thesis by TARSKI:def 1;

      end;

      then

       A26: ( delta T) is constant by VALUED_0:def 18;

      (( delta T) . 1) = 0 by A2;

      then ( lim ( delta T)) = 0 by A26, SEQ_4: 25;

      hence thesis by A26;

    end;

    theorem :: INTEGRA4:11

    

     Th11: ex T be DivSequence of A st ( delta T) is convergent & ( lim ( delta T)) = 0

    proof

      now

        per cases ;

          suppose

           A1: ( vol A) <> 0 ;

          ( vol A) >= 0 by INTEGRA1: 9;

          hence thesis by A1, Lm5;

        end;

          suppose ( vol A) = 0 ;

          hence thesis by Lm6;

        end;

      end;

      hence thesis;

    end;

    theorem :: INTEGRA4:12

    

     Th12: for f be Function of A, REAL st (f | A) is bounded holds f is integrable iff for T be DivSequence of A st ( delta T) is convergent & ( lim ( delta T)) = 0 holds (( lim ( upper_sum (f,T))) - ( lim ( lower_sum (f,T)))) = 0

    proof

      let f be Function of A, REAL ;

      assume

       A1: (f | A) is bounded;

      

       A2: f is integrable implies for T be DivSequence of A st ( delta T) is convergent & ( lim ( delta T)) = 0 holds (( lim ( upper_sum (f,T))) - ( lim ( lower_sum (f,T)))) = 0

      proof

        assume

         A3: f is integrable;

        for T be DivSequence of A st ( delta T) is convergent & ( lim ( delta T)) = 0 holds (( lim ( upper_sum (f,T))) - ( lim ( lower_sum (f,T)))) = 0

        proof

          

           A4: ( upper_integral f) = ( lower_integral f) by A3, INTEGRA1:def 16;

          let T be DivSequence of A;

          assume that

           A5: ( delta T) is convergent and

           A6: ( lim ( delta T)) = 0 ;

          

           A7: ( lim ( lower_sum (f,T))) = ( lower_integral f) by A1, A5, A6, Th8;

          ( lim ( upper_sum (f,T))) = ( upper_integral f) by A1, A5, A6, Th9;

          hence thesis by A7, A4;

        end;

        hence thesis;

      end;

      (for T be DivSequence of A st ( delta T) is convergent & ( lim ( delta T)) = 0 holds (( lim ( upper_sum (f,T))) - ( lim ( lower_sum (f,T)))) = 0 ) implies f is integrable

      proof

        consider T be DivSequence of A such that

         A8: ( delta T) is convergent and

         A9: ( lim ( delta T)) = 0 by Th11;

        assume for T be DivSequence of A st ( delta T) is convergent & ( lim ( delta T)) = 0 holds (( lim ( upper_sum (f,T))) - ( lim ( lower_sum (f,T)))) = 0 ;

        then (( lim ( upper_sum (f,T))) - ( lim ( lower_sum (f,T)))) = 0 by A8, A9;

        then (( upper_integral f) - ( lim ( lower_sum (f,T)))) = 0 by A1, A8, A9, Th9;

        then

         A10: (( upper_integral f) - ( lower_integral f)) = 0 by A1, A8, A9, Th8;

        

         A11: f is lower_integrable by A1, Th10;

        f is upper_integrable by A1, Th10;

        hence thesis by A11, A10, INTEGRA1:def 16;

      end;

      hence thesis by A2;

    end;

    theorem :: INTEGRA4:13

    

     Th13: for f be Function of C, REAL holds ( max+ f) is total & ( max- f) is total

    proof

      let f be Function of C, REAL ;

      

       A1: ( dom f) = C by FUNCT_2:def 1;

      then

       A2: ( dom ( max- f)) = C by RFUNCT_3:def 11;

      ( dom ( max+ f)) = C by A1, RFUNCT_3:def 10;

      hence thesis by A2, PARTFUN1:def 2;

    end;

    theorem :: INTEGRA4:14

    

     Th14: for f be PartFunc of C, REAL st (f | X) is bounded_above holds (( max+ f) | X) is bounded_above

    proof

      let f be PartFunc of C, REAL ;

      assume (f | X) is bounded_above;

      then

      consider b be Real such that

       A1: for c be object st c in (X /\ ( dom f)) holds (f . c) <= b by RFUNCT_1: 70;

      

       A2: ( dom ( max+ f)) = ( dom f) by RFUNCT_3:def 10;

      ex r st for c be object st c in (X /\ ( dom ( max+ f))) holds (( max+ f) . c) <= r

      proof

        now

          per cases ;

            suppose

             A3: b < 0 ;

            for c be object st c in (X /\ ( dom ( max+ f))) holds (( max+ f) . c) <= 0

            proof

              let c be object;

              assume c in (X /\ ( dom ( max+ f)));

              then

               A4: c in (X /\ ( dom f)) by RFUNCT_3:def 10;

              then (f . c) <= b by A1;

              then ( max ((f . c), 0 )) = 0 by A3, XXREAL_0:def 10;

              then

               A5: ( max+ (f . c)) = 0 by RFUNCT_3:def 1;

              c in ( dom f) by A4, XBOOLE_0:def 4;

              hence thesis by A2, A5, RFUNCT_3:def 10;

            end;

            hence thesis;

          end;

            suppose

             A6: b >= 0 ;

            for c be object st c in (X /\ ( dom ( max+ f))) holds (( max+ f) . c) <= b

            proof

              let c be object;

              assume c in (X /\ ( dom ( max+ f)));

              then

               A7: c in (X /\ ( dom f)) by RFUNCT_3:def 10;

              then (f . c) <= b by A1;

              then ( max ((f . c), 0 )) <= b by A6, XXREAL_0: 28;

              then

               A8: ( max+ (f . c)) <= b by RFUNCT_3:def 1;

              c in ( dom f) by A7, XBOOLE_0:def 4;

              hence thesis by A2, A8, RFUNCT_3:def 10;

            end;

            then

            consider r be Real such that r = b and

             A9: for c be object st c in (X /\ ( dom ( max+ f))) holds (( max+ f) . c) <= r;

            thus thesis by A9;

          end;

        end;

        hence thesis;

      end;

      hence thesis by RFUNCT_1: 70;

    end;

    theorem :: INTEGRA4:15

    

     Th15: for f be PartFunc of C, REAL holds (( max+ f) | X) is bounded_below

    proof

      let f be PartFunc of C, REAL ;

      for c be object st c in (X /\ ( dom ( max+ f))) holds (( max+ f) . c) >= 0 by RFUNCT_3: 37;

      hence thesis by RFUNCT_1: 71;

    end;

    theorem :: INTEGRA4:16

    

     Th16: for f be PartFunc of C, REAL st (f | X) is bounded_below holds (( max- f) | X) is bounded_above

    proof

      let f be PartFunc of C, REAL ;

      assume (f | X) is bounded_below;

      then

      consider b be Real such that

       A1: for c be object st c in (X /\ ( dom f)) holds (f . c) >= b by RFUNCT_1: 71;

      

       A2: ( dom ( max- f)) = ( dom f) by RFUNCT_3:def 11;

      ex r st for c be object st c in (X /\ ( dom ( max- f))) holds (( max- f) . c) <= r

      proof

        now

          per cases ;

            suppose

             A3: b > 0 ;

            for c be object st c in (X /\ ( dom ( max- f))) holds (( max- f) . c) <= 0

            proof

              let c be object;

              assume c in (X /\ ( dom ( max- f)));

              then

               A4: c in (X /\ ( dom f)) by RFUNCT_3:def 11;

              then (f . c) >= b by A1;

              then ( max (( - (f . c)), 0 )) = 0 by A3, XXREAL_0:def 10;

              then

               A5: ( max- (f . c)) = 0 by RFUNCT_3:def 2;

              c in ( dom f) by A4, XBOOLE_0:def 4;

              hence thesis by A2, A5, RFUNCT_3:def 11;

            end;

            hence thesis;

          end;

            suppose

             A6: b <= 0 ;

            for c be object st c in (X /\ ( dom ( max- f))) holds (( max- f) . c) <= ( - b)

            proof

              let c be object;

              assume c in (X /\ ( dom ( max- f)));

              then

               A7: c in (X /\ ( dom f)) by RFUNCT_3:def 11;

              then (f . c) >= b by A1;

              then ( - (f . c)) <= ( - b) by XREAL_1: 24;

              then ( max (( - (f . c)), 0 )) <= ( - b) by A6, XXREAL_0: 28;

              then

               A8: ( max- (f . c)) <= ( - b) by RFUNCT_3:def 2;

              c in ( dom f) by A7, XBOOLE_0:def 4;

              hence thesis by A2, A8, RFUNCT_3:def 11;

            end;

            then

            consider r be Real such that r = ( - b) and

             A9: for c be object st c in (X /\ ( dom ( max- f))) holds (( max- f) . c) <= r;

            thus thesis by A9;

          end;

        end;

        hence thesis;

      end;

      hence thesis by RFUNCT_1: 70;

    end;

    theorem :: INTEGRA4:17

    

     Th17: for f be PartFunc of C, REAL holds (( max- f) | X) is bounded_below

    proof

      let f be PartFunc of C, REAL ;

      for c be object st c in (X /\ ( dom ( max- f))) holds (( max- f) . c) >= 0 by RFUNCT_3: 40;

      hence thesis by RFUNCT_1: 71;

    end;

    theorem :: INTEGRA4:18

    

     Th18: for f be PartFunc of A, REAL st (f | A) is bounded_above holds ( rng (f | X)) is bounded_above

    proof

      let f be PartFunc of A, REAL ;

      assume (f | A) is bounded_above;

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

      hence thesis by RELAT_1: 70, XXREAL_2: 43;

    end;

    theorem :: INTEGRA4:19

    

     Th19: for f be PartFunc of A, REAL st (f | A) is bounded_below holds ( rng (f | X)) is bounded_below

    proof

      let f be PartFunc of A, REAL ;

      assume (f | A) is bounded_below;

      then ( rng f) is bounded_below by INTEGRA1: 11;

      hence thesis by RELAT_1: 70, XXREAL_2: 44;

    end;

    theorem :: INTEGRA4:20

    

     Th20: for f be Function of A, REAL st (f | A) is bounded & f is integrable holds ( max+ f) is integrable

    proof

      let f be Function of A, REAL ;

      assume that

       A1: (f | A) is bounded and

       A2: f is integrable;

      

       A3: ( max+ f) is total by Th13;

      

       A4: (( max+ f) | A) is bounded_below by Th15;

      

       A5: (( max+ f) | A) is bounded_above by A1, Th14;

      for T be DivSequence of A st ( delta T) is convergent & ( lim ( delta T)) = 0 holds (( lim ( upper_sum (( max+ f),T))) - ( lim ( lower_sum (( max+ f),T)))) = 0

      proof

        let T be DivSequence of A;

        assume that

         A6: ( delta T) is convergent and

         A7: ( lim ( delta T)) = 0 ;

        

         A8: ( lower_sum (f,T)) is convergent by A1, A6, A7, Th8;

        

         A9: ( upper_sum (f,T)) is convergent by A1, A6, A7, Th9;

        then

         A10: (( upper_sum (f,T)) - ( lower_sum (f,T))) is convergent by A8;

        reconsider osc1 = (( upper_sum (( max+ f),T)) - ( lower_sum (( max+ f),T))) as Real_Sequence;

        reconsider osc = (( upper_sum (f,T)) - ( lower_sum (f,T))) as Real_Sequence;

        (( lim ( upper_sum (f,T))) - ( lim ( lower_sum (f,T)))) = 0 by A1, A2, A6, A7, Th12;

        then

         A11: ( lim (( upper_sum (f,T)) - ( lower_sum (f,T)))) = 0 by A9, A8, SEQ_2: 12;

        

         A12: for a be Real st 0 < a holds ex n be Nat st for m be Nat st n <= m holds |.((osc1 . m) - 0 ).| < a

        proof

          let a be Real;

          assume 0 < a;

          then

          consider n be Nat such that

           A13: for m be Nat st n <= m holds |.((osc . m) - 0 ).| < a by A10, A11, SEQ_2:def 7;

          take n;

          let m be Nat;

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

          reconsider D = (T . mm) as Division of A;

          ( len ( upper_volume (f,D))) = ( len D) by INTEGRA1:def 6;

          then

          reconsider UV = ( upper_volume (f,D)) as Element of (( len D) -tuples_on REAL ) by FINSEQ_2: 133;

          ( len ( lower_volume (f,D))) = ( len D) by INTEGRA1:def 7;

          then

          reconsider LV = ( lower_volume (f,D)) as Element of (( len D) -tuples_on REAL ) by FINSEQ_2: 133;

          ( len ( upper_volume (( max+ f),D))) = ( len D) by INTEGRA1:def 6;

          then

          reconsider UV1 = ( upper_volume (( max+ f),D)) as Element of (( len D) -tuples_on REAL ) by FINSEQ_2: 133;

          ( len ( lower_volume (( max+ f),D))) = ( len D) by INTEGRA1:def 7;

          then

          reconsider LV1 = ( lower_volume (( max+ f),D)) as Element of (( len D) -tuples_on REAL ) by FINSEQ_2: 133;

          reconsider F = (UV1 - LV1) as FinSequence of REAL ;

          (osc1 . m) = ((( upper_sum (( max+ f),T)) . m) + (( - ( lower_sum (( max+ f),T))) . m)) by SEQ_1: 7

          .= ((( upper_sum (( max+ f),T)) . m) + ( - (( lower_sum (( max+ f),T)) . m))) by SEQ_1: 10

          .= ((( upper_sum (( max+ f),T)) . m) - (( lower_sum (( max+ f),T)) . m))

          .= (( upper_sum (( max+ f),(T . mm))) - (( lower_sum (( max+ f),T)) . m)) by INTEGRA2:def 2

          .= (( upper_sum (( max+ f),(T . mm))) - ( lower_sum (( max+ f),(T . mm)))) by INTEGRA2:def 3

          .= (( Sum ( upper_volume (( max+ f),D))) - ( lower_sum (( max+ f),(T . mm)))) by INTEGRA1:def 8

          .= (( Sum ( upper_volume (( max+ f),D))) - ( Sum ( lower_volume (( max+ f),D)))) by INTEGRA1:def 9;

          then

           A14: (osc1 . m) = ( Sum (UV1 - LV1)) by RVSUM_1: 90;

          

           A15: for j be Nat st j in ( Seg ( len D)) holds ((UV1 - LV1) . j) <= ((UV - LV) . j)

          proof

            let j be Nat;

            set x = ((UV1 - LV1) . j), y = ((UV - LV) . j);

            assume

             A16: j in ( Seg ( len D));

            then

             A17: j in ( dom D) by FINSEQ_1:def 3;

            then

             A18: (LV1 . j) = (( lower_bound ( rng (( max+ f) | ( divset (D,j))))) * ( vol ( divset (D,j)))) by INTEGRA1:def 7;

            

             A19: ( rng (f | ( divset (D,j)))) is real-bounded & ex r st r in ( rng (f | ( divset (D,j))))

            proof

              

               A20: ( rng f) is bounded_below by A1, INTEGRA1: 11;

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

              hence ( rng (f | ( divset (D,j)))) is real-bounded by A20, RELAT_1: 70, XXREAL_2: 45;

              consider r be Element of REAL such that

               A21: r in ( divset (D,j)) by SUBSET_1: 4;

              j in ( dom D) by A16, FINSEQ_1:def 3;

              then ( divset (D,j)) c= A by INTEGRA1: 8;

              then r in A by A21;

              then r in ( dom f) by FUNCT_2:def 1;

              then (f . r) in ( rng (f | ( divset (D,j)))) by A21, FUNCT_1: 50;

              hence thesis;

            end;

            

             A22: (( upper_bound ( rng (f | ( divset (D,j))))) - ( lower_bound ( rng (f | ( divset (D,j)))))) >= (( upper_bound ( rng (( max+ f) | ( divset (D,j))))) - ( lower_bound ( rng (( max+ f) | ( divset (D,j))))))

            proof

              set m1 = ( lower_bound ( rng (( max+ f) | ( divset (D,j)))));

              set M1 = ( upper_bound ( rng (( max+ f) | ( divset (D,j)))));

              set m = ( lower_bound ( rng (f | ( divset (D,j)))));

              set M = ( upper_bound ( rng (f | ( divset (D,j)))));

              

               A23: ( dom f) = ( dom ( max+ f)) by RFUNCT_3:def 10;

              

               A24: j in ( dom D) by A16, FINSEQ_1:def 3;

              

               A25: ( rng (f | ( divset (D,j)))) is bounded_above by A1, Th18;

              ( dom (f | ( divset (D,j)))) = (( dom f) /\ ( divset (D,j))) by RELAT_1: 61;

              then ( dom (f | ( divset (D,j)))) = (A /\ ( divset (D,j))) by FUNCT_2:def 1;

              then ( dom (f | ( divset (D,j)))) <> {} by A24, INTEGRA1: 8, XBOOLE_1: 28;

              then

               A26: ( rng (f | ( divset (D,j)))) <> {} by RELAT_1: 42;

              ( dom f) = A by FUNCT_2:def 1;

              then ( dom (( max+ f) | ( divset (D,j)))) = (A /\ ( divset (D,j))) by A23, RELAT_1: 61;

              then ( dom (( max+ f) | ( divset (D,j)))) <> {} by A24, INTEGRA1: 8, XBOOLE_1: 28;

              then

               A27: ( rng (( max+ f) | ( divset (D,j)))) <> {} by RELAT_1: 42;

              (( max+ f) | A) is bounded_below by Th15;

              then

               A28: ( rng (( max+ f) | ( divset (D,j)))) is bounded_below by Th19;

              

               A29: ( rng (f | ( divset (D,j)))) is bounded_below by A1, Th19;

              (( max+ f) | A) is bounded_above by A1, Th14;

              then

               A30: ( rng (( max+ f) | ( divset (D,j)))) is bounded_above by Th18;

              now

                per cases by A19, SEQ_4: 11;

                  suppose

                   A31: M > 0 & m >= 0 ;

                  

                   A32: for r be Real st r in ( rng (( max+ f) | ( divset (D,j)))) holds r <= M

                  proof

                    let r be Real;

                    assume r in ( rng (( max+ f) | ( divset (D,j))));

                    then

                    consider x be Element of A such that

                     A33: x in ( dom (( max+ f) | ( divset (D,j)))) and

                     A34: r = ((( max+ f) | ( divset (D,j))) . x) by PARTFUN1: 3;

                    

                     A35: r = (( max+ (f | ( divset (D,j)))) . x) by A34, RFUNCT_3: 44;

                    

                     A36: x in ( dom ( max+ (f | ( divset (D,j))))) by A33, RFUNCT_3: 44;

                    then

                     A37: x in ( dom (f | ( divset (D,j)))) by RFUNCT_3:def 10;

                    now

                      per cases by A35, RFUNCT_3: 37;

                        suppose r = 0 ;

                        hence thesis by A31;

                      end;

                        suppose

                         A38: r > 0 ;

                        r = ( max+ ((f | ( divset (D,j))) . x)) by A35, A36, RFUNCT_3:def 10;

                        then r = ( max (((f | ( divset (D,j))) . x), 0 )) by RFUNCT_3:def 1;

                        then r = ((f | ( divset (D,j))) . x) by A38, XXREAL_0:def 10;

                        then r in ( rng (f | ( divset (D,j)))) by A37, FUNCT_1:def 3;

                        hence thesis by A25, SEQ_4:def 1;

                      end;

                    end;

                    hence thesis;

                  end;

                  

                   A39: for s be Real st 0 < s holds ex r be Real st r in ( rng (( max+ f) | ( divset (D,j)))) & r < (m + s)

                  proof

                    let s be Real;

                    assume 0 < s;

                    then

                    consider r be Real such that

                     A40: r in ( rng (f | ( divset (D,j)))) and

                     A41: r < (m + s) by A26, A29, SEQ_4:def 2;

                    reconsider r as Real;

                    r in ( rng (( max+ f) | ( divset (D,j))))

                    proof

                      

                       A42: r >= m by A29, A40, SEQ_4:def 2;

                      consider x be Element of A such that

                       A43: x in ( dom (f | ( divset (D,j)))) and

                       A44: r = ((f | ( divset (D,j))) . x) by A40, PARTFUN1: 3;

                      

                       A45: x in ( dom ( max+ (f | ( divset (D,j))))) by A43, RFUNCT_3:def 10;

                      

                      then (( max+ (f | ( divset (D,j)))) . x) = ( max+ r) by A44, RFUNCT_3:def 10

                      .= ( max (r, 0 )) by RFUNCT_3:def 1

                      .= r by A31, A42, XXREAL_0:def 10;

                      then r in ( rng ( max+ (f | ( divset (D,j))))) by A45, FUNCT_1:def 3;

                      hence thesis by RFUNCT_3: 44;

                    end;

                    hence thesis by A41;

                  end;

                  

                   A46: for r be Real st r in ( rng (( max+ f) | ( divset (D,j)))) holds m <= r

                  proof

                    let r be Real;

                    assume r in ( rng (( max+ f) | ( divset (D,j))));

                    then

                    consider x be Element of A such that

                     A47: x in ( dom (( max+ f) | ( divset (D,j)))) and

                     A48: r = ((( max+ f) | ( divset (D,j))) . x) by PARTFUN1: 3;

                    

                     A49: x in ( dom ( max+ (f | ( divset (D,j))))) by A47, RFUNCT_3: 44;

                    x in ( dom ( max+ (f | ( divset (D,j))))) by A47, RFUNCT_3: 44;

                    then x in ( dom (f | ( divset (D,j)))) by RFUNCT_3:def 10;

                    then ((f | ( divset (D,j))) . x) in ( rng (f | ( divset (D,j)))) by FUNCT_1:def 3;

                    then

                     A50: ((f | ( divset (D,j))) . x) >= m by A29, SEQ_4:def 2;

                    r = (( max+ (f | ( divset (D,j)))) . x) by A48, RFUNCT_3: 44

                    .= ( max+ ((f | ( divset (D,j))) . x)) by A49, RFUNCT_3:def 10

                    .= ( max (((f | ( divset (D,j))) . x), 0 )) by RFUNCT_3:def 1;

                    hence thesis by A31, A50, XXREAL_0:def 10;

                  end;

                  for s be Real st 0 < s holds ex r be Real st r in ( rng (( max+ f) | ( divset (D,j)))) & (M - s) < r

                  proof

                    let s be Real;

                    assume 0 < s;

                    then

                    consider r be Real such that

                     A51: r in ( rng (f | ( divset (D,j)))) and

                     A52: (M - s) < r by A26, A25, SEQ_4:def 1;

                    r in ( rng (( max+ f) | ( divset (D,j))))

                    proof

                      reconsider r1 = r as Real;

                      consider x be Element of A such that

                       A53: x in ( dom (f | ( divset (D,j)))) and

                       A54: r = ((f | ( divset (D,j))) . x) by A51, PARTFUN1: 3;

                      

                       A55: r >= m by A29, A51, SEQ_4:def 2;

                      

                       A56: x in ( dom ( max+ (f | ( divset (D,j))))) by A53, RFUNCT_3:def 10;

                      

                      then (( max+ (f | ( divset (D,j)))) . x) = ( max+ r1) by A54, RFUNCT_3:def 10

                      .= ( max (r, 0 )) by RFUNCT_3:def 1

                      .= r by A31, A55, XXREAL_0:def 10;

                      then r in ( rng ( max+ (f | ( divset (D,j))))) by A56, FUNCT_1:def 3;

                      hence thesis by RFUNCT_3: 44;

                    end;

                    hence thesis by A52;

                  end;

                  then M1 = M by A27, A30, A32, SEQ_4:def 1;

                  hence thesis by A27, A28, A46, A39, SEQ_4:def 2;

                end;

                  suppose

                   A57: M > 0 & m <= 0 ;

                  

                   A58: for s be Real st 0 < s holds ex r be Real st r in ( rng (( max+ f) | ( divset (D,j)))) & r < ( 0 + s)

                  proof

                    let s be Real;

                    assume

                     A59: s > 0 ;

                    then

                    consider r be Real such that

                     A60: r in ( rng (f | ( divset (D,j)))) and

                     A61: r < (m + s) by A26, A29, SEQ_4:def 2;

                    consider x be Element of A such that

                     A62: x in ( dom (f | ( divset (D,j)))) and

                     A63: r = ((f | ( divset (D,j))) . x) by A60, PARTFUN1: 3;

                    

                     A64: x in ( dom ( max+ (f | ( divset (D,j))))) by A62, RFUNCT_3:def 10;

                    

                    then

                     A65: (( max+ (f | ( divset (D,j)))) . x) = ( max+ ((f | ( divset (D,j))) . x)) by RFUNCT_3:def 10

                    .= ( max (((f | ( divset (D,j))) . x), 0 )) by RFUNCT_3:def 1;

                    (( max+ (f | ( divset (D,j)))) . x) in ( rng ( max+ (f | ( divset (D,j))))) by A64, FUNCT_1:def 3;

                    then

                     A66: (( max+ (f | ( divset (D,j)))) . x) in ( rng (( max+ f) | ( divset (D,j)))) by RFUNCT_3: 44;

                    

                     A67: (r - s) < m by A61, XREAL_1: 19;

                    now

                      per cases ;

                        suppose r < 0 ;

                        then 0 in ( rng (( max+ f) | ( divset (D,j)))) by A63, A66, A65, XXREAL_0:def 10;

                        hence ex r st r in ( rng (( max+ f) | ( divset (D,j)))) & r < ( 0 + s) by A59;

                      end;

                        suppose

                         A68: r >= 0 ;

                        

                         A69: r < ( 0 + s) by A57, A67, XREAL_1: 19;

                        r in ( rng (( max+ f) | ( divset (D,j)))) by A63, A66, A65, A68, XXREAL_0:def 10;

                        hence ex r st r in ( rng (( max+ f) | ( divset (D,j)))) & r < ( 0 + s) by A69;

                      end;

                    end;

                    hence thesis;

                  end;

                  for r be Real st r in ( rng (( max+ f) | ( divset (D,j)))) holds 0 <= r

                  proof

                    let r be Real;

                    assume r in ( rng (( max+ f) | ( divset (D,j))));

                    then r in ( rng ( max+ (f | ( divset (D,j))))) by RFUNCT_3: 44;

                    then ex x be Element of A st x in ( dom ( max+ (f | ( divset (D,j))))) & r = (( max+ (f | ( divset (D,j)))) . x) by PARTFUN1: 3;

                    hence thesis by RFUNCT_3: 37;

                  end;

                  then

                   A70: m1 = 0 by A27, A28, A58, SEQ_4:def 2;

                  for r st r in ( rng (( max+ f) | ( divset (D,j)))) holds r <= M

                  proof

                    let r;

                    assume r in ( rng (( max+ f) | ( divset (D,j))));

                    then

                    consider x be Element of A such that

                     A71: x in ( dom (( max+ f) | ( divset (D,j)))) and

                     A72: r = ((( max+ f) | ( divset (D,j))) . x) by PARTFUN1: 3;

                    

                     A73: r = (( max+ (f | ( divset (D,j)))) . x) by A72, RFUNCT_3: 44;

                    

                     A74: x in ( dom ( max+ (f | ( divset (D,j))))) by A71, RFUNCT_3: 44;

                    then

                     A75: x in ( dom (f | ( divset (D,j)))) by RFUNCT_3:def 10;

                    now

                      per cases by A73, RFUNCT_3: 37;

                        suppose r = 0 ;

                        hence thesis by A57;

                      end;

                        suppose

                         A76: r > 0 ;

                        r = ( max+ ((f | ( divset (D,j))) . x)) by A73, A74, RFUNCT_3:def 10;

                        then r = ( max (((f | ( divset (D,j))) . x), 0 )) by RFUNCT_3:def 1;

                        then r = ((f | ( divset (D,j))) . x) by A76, XXREAL_0:def 10;

                        then r in ( rng (f | ( divset (D,j)))) by A75, FUNCT_1:def 3;

                        hence thesis by A25, SEQ_4:def 1;

                      end;

                    end;

                    hence thesis;

                  end;

                  then

                   A77: for r be Real st r in ( rng (( max+ f) | ( divset (D,j)))) holds r <= M;

                  for s be Real st 0 < s holds ex r be Real st r in ( rng (( max+ f) | ( divset (D,j)))) & (M - s) < r

                  proof

                    assume not (for s be Real st 0 < s holds ex r be Real st r in ( rng (( max+ f) | ( divset (D,j)))) & (M - s) < r);

                    then

                    consider s be Real such that

                     A78: s > 0 and

                     A79: for r be Real st r in ( rng (( max+ f) | ( divset (D,j)))) holds (M - s) >= r;

                    consider r1 be Real such that

                     A80: r1 in ( rng (f | ( divset (D,j)))) and

                     A81: (M - s) < r1 by A26, A25, A78, SEQ_4:def 1;

                    consider x be Element of A such that

                     A82: x in ( dom (f | ( divset (D,j)))) and

                     A83: r1 = ((f | ( divset (D,j))) . x) by A80, PARTFUN1: 3;

                    

                     A84: x in ( dom ( max+ (f | ( divset (D,j))))) by A82, RFUNCT_3:def 10;

                    then x in ( dom (( max+ f) | ( divset (D,j)))) by RFUNCT_3: 44;

                    then

                     A85: ((( max+ f) | ( divset (D,j))) . x) in ( rng (( max+ f) | ( divset (D,j)))) by FUNCT_1:def 3;

                    (( max+ (f | ( divset (D,j)))) . x) >= 0 by RFUNCT_3: 37;

                    then ((( max+ f) | ( divset (D,j))) . x) >= 0 by RFUNCT_3: 44;

                    then

                     A86: (M - s) >= 0 by A79, A85;

                    ((( max+ f) | ( divset (D,j))) . x) = (( max+ (f | ( divset (D,j)))) . x) by RFUNCT_3: 44

                    .= ( max+ ((f | ( divset (D,j))) . x)) by A84, RFUNCT_3:def 10

                    .= ( max (r1, 0 )) by A83, RFUNCT_3:def 1

                    .= r1 by A81, A86, XXREAL_0:def 10;

                    hence contradiction by A79, A81, A85;

                  end;

                  then M1 = M by A27, A30, A77, SEQ_4:def 1;

                  hence thesis by A57, A70, XREAL_1: 13;

                end;

                  suppose

                   A87: M <= 0 & m <= 0 ;

                  

                   A88: for s be Real st 0 < s holds ex r be Real st r in ( rng (( max+ f) | ( divset (D,j)))) & r < ( 0 + s)

                  proof

                    let s be Real;

                    assume

                     A89: s > 0 ;

                    consider r be Element of REAL such that

                     A90: r in ( rng (( max+ f) | ( divset (D,j)))) by A27, SUBSET_1: 4;

                    consider x be Element of A such that

                     A91: x in ( dom (( max+ f) | ( divset (D,j)))) and

                     A92: r = ((( max+ f) | ( divset (D,j))) . x) by A90, PARTFUN1: 3;

                    

                     A93: x in ( dom ( max+ (f | ( divset (D,j))))) by A91, RFUNCT_3: 44;

                    then x in ( dom (f | ( divset (D,j)))) by RFUNCT_3:def 10;

                    then ((f | ( divset (D,j))) . x) in ( rng (f | ( divset (D,j)))) by FUNCT_1:def 3;

                    then

                     A94: ((f | ( divset (D,j))) . x) <= M by A25, SEQ_4:def 1;

                    r = (( max+ (f | ( divset (D,j)))) . x) by A92, RFUNCT_3: 44;

                    

                    then r = ( max+ ((f | ( divset (D,j))) . x)) by A93, RFUNCT_3:def 10

                    .= ( max (((f | ( divset (D,j))) . x), 0 )) by RFUNCT_3:def 1;

                    then r = 0 by A87, A94, XXREAL_0:def 10;

                    hence thesis by A89, A90;

                  end;

                  for r be Real st r in ( rng (( max+ f) | ( divset (D,j)))) holds 0 <= r

                  proof

                    let r be Real;

                    assume r in ( rng (( max+ f) | ( divset (D,j))));

                    then

                    consider x be Element of A such that x in ( dom (( max+ f) | ( divset (D,j)))) and

                     A95: r = ((( max+ f) | ( divset (D,j))) . x) by PARTFUN1: 3;

                    r = (( max+ (f | ( divset (D,j)))) . x) by A95, RFUNCT_3: 44;

                    hence thesis by RFUNCT_3: 37;

                  end;

                  then

                   A96: m1 = 0 by A27, A28, A88, SEQ_4:def 2;

                  

                   A97: for r be Real st r in ( rng (( max+ f) | ( divset (D,j)))) holds r <= 0

                  proof

                    let r be Real;

                    assume r in ( rng (( max+ f) | ( divset (D,j))));

                    then

                    consider x be Element of A such that

                     A98: x in ( dom (( max+ f) | ( divset (D,j)))) and

                     A99: r = ((( max+ f) | ( divset (D,j))) . x) by PARTFUN1: 3;

                    

                     A100: x in ( dom ( max+ (f | ( divset (D,j))))) by A98, RFUNCT_3: 44;

                    then x in ( dom (f | ( divset (D,j)))) by RFUNCT_3:def 10;

                    then ((f | ( divset (D,j))) . x) in ( rng (f | ( divset (D,j)))) by FUNCT_1:def 3;

                    then

                     A101: ((f | ( divset (D,j))) . x) <= M by A25, SEQ_4:def 1;

                    r = (( max+ (f | ( divset (D,j)))) . x) by A99, RFUNCT_3: 44;

                    

                    then r = ( max+ ((f | ( divset (D,j))) . x)) by A100, RFUNCT_3:def 10

                    .= ( max (((f | ( divset (D,j))) . x), 0 )) by RFUNCT_3:def 1

                    .= 0 by A87, A101, XXREAL_0:def 10;

                    hence thesis;

                  end;

                  for s be Real st 0 < s holds ex r be Real st r in ( rng (( max+ f) | ( divset (D,j)))) & ( 0 - s) < r

                  proof

                    let s be Real;

                    assume

                     A102: s > 0 ;

                    consider r be Element of REAL such that

                     A103: r in ( rng (( max+ f) | ( divset (D,j)))) by A27, SUBSET_1: 4;

                    consider x be Element of A such that x in ( dom (( max+ f) | ( divset (D,j)))) and

                     A104: r = ((( max+ f) | ( divset (D,j))) . x) by A103, PARTFUN1: 3;

                    r = (( max+ (f | ( divset (D,j)))) . x) by A104, RFUNCT_3: 44;

                    then r >= 0 by RFUNCT_3: 37;

                    hence thesis by A102, A103;

                  end;

                  then M1 = 0 by A27, A30, A97, SEQ_4:def 1;

                  hence thesis by A19, A96, SEQ_4: 11, XREAL_1: 48;

                end;

              end;

              hence thesis;

            end;

            

             A105: (LV . j) = (( lower_bound ( rng (f | ( divset (D,j))))) * ( vol ( divset (D,j)))) by A17, INTEGRA1:def 7;

            (UV . j) = (( upper_bound ( rng (f | ( divset (D,j))))) * ( vol ( divset (D,j)))) by A17, INTEGRA1:def 6;

            

            then

             A106: y = ((( upper_bound ( rng (f | ( divset (D,j))))) * ( vol ( divset (D,j)))) - (( lower_bound ( rng (f | ( divset (D,j))))) * ( vol ( divset (D,j))))) by A105, RVSUM_1: 27

            .= ((( upper_bound ( rng (f | ( divset (D,j))))) - ( lower_bound ( rng (f | ( divset (D,j)))))) * ( vol ( divset (D,j))));

            (UV1 . j) = (( upper_bound ( rng (( max+ f) | ( divset (D,j))))) * ( vol ( divset (D,j)))) by A17, INTEGRA1:def 6;

            

            then

             A107: x = ((( upper_bound ( rng (( max+ f) | ( divset (D,j))))) * ( vol ( divset (D,j)))) - (( lower_bound ( rng (( max+ f) | ( divset (D,j))))) * ( vol ( divset (D,j))))) by A18, RVSUM_1: 27

            .= ((( upper_bound ( rng (( max+ f) | ( divset (D,j))))) - ( lower_bound ( rng (( max+ f) | ( divset (D,j)))))) * ( vol ( divset (D,j))));

            ( vol ( divset (D,j))) >= 0 by INTEGRA1: 9;

            hence thesis by A107, A106, A22, XREAL_1: 64;

          end;

          assume n <= m;

          then

           A108: |.((osc . m) - 0 ).| < a by A13;

          for j be Nat st j in ( dom F) holds 0 <= (F . j)

          proof

            let j be Nat;

            set r = (F . j);

            (( max+ f) | A) is bounded_below by Th15;

            then

             A109: ( rng ( max+ f)) is bounded_below by INTEGRA1: 11;

            assume that

             A110: j in ( dom F);

            j in ( Seg ( len F)) by A110, FINSEQ_1:def 3;

            then

             A111: j in ( Seg ( len D)) by CARD_1:def 7;

            then

             A112: j in ( dom D) by FINSEQ_1:def 3;

            then

             A113: (LV1 . j) = (( lower_bound ( rng (( max+ f) | ( divset (D,j))))) * ( vol ( divset (D,j)))) by INTEGRA1:def 7;

            

             A114: ex r st r in ( rng (( max+ f) | ( divset (D,j))))

            proof

              consider r be Element of REAL such that

               A115: r in ( divset (D,j)) by SUBSET_1: 4;

              j in ( dom D) by A111, FINSEQ_1:def 3;

              then ( divset (D,j)) c= A by INTEGRA1: 8;

              then r in A by A115;

              then r in ( dom f) by FUNCT_2:def 1;

              then r in (( dom f) /\ ( divset (D,j))) by A115, XBOOLE_0:def 4;

              then r in ( dom (f | ( divset (D,j)))) by RELAT_1: 61;

              then r in ( dom ( max+ (f | ( divset (D,j))))) by RFUNCT_3:def 10;

              then r in ( dom (( max+ f) | ( divset (D,j)))) by RFUNCT_3: 44;

              then ((( max+ f) | ( divset (D,j))) . r) in ( rng (( max+ f) | ( divset (D,j)))) by FUNCT_1:def 3;

              hence thesis;

            end;

            (( max+ f) | A) is bounded_above by A1, Th14;

            then ( rng ( max+ f)) is bounded_above by INTEGRA1: 13;

            then ( rng (( max+ f) | ( divset (D,j)))) is real-bounded by A109, RELAT_1: 70, XXREAL_2: 45;

            then

             A116: (( upper_bound ( rng (( max+ f) | ( divset (D,j))))) - ( lower_bound ( rng (( max+ f) | ( divset (D,j)))))) >= 0 by A114, SEQ_4: 11, XREAL_1: 48;

            (UV1 . j) = (( upper_bound ( rng (( max+ f) | ( divset (D,j))))) * ( vol ( divset (D,j)))) by A112, INTEGRA1:def 6;

            

            then

             A117: r = ((( upper_bound ( rng (( max+ f) | ( divset (D,j))))) * ( vol ( divset (D,j)))) - (( lower_bound ( rng (( max+ f) | ( divset (D,j))))) * ( vol ( divset (D,j))))) by A110, A113, VALUED_1: 13

            .= ((( upper_bound ( rng (( max+ f) | ( divset (D,j))))) - ( lower_bound ( rng (( max+ f) | ( divset (D,j)))))) * ( vol ( divset (D,j))));

            ( vol ( divset (D,j))) >= 0 by INTEGRA1: 9;

            hence thesis by A117, A116;

          end;

          then

           A118: (osc1 . m) >= 0 by A14, RVSUM_1: 84;

          then

           A119: |.((osc1 . m) - 0 ).| = (osc1 . m) by ABSVALUE:def 1;

          (osc . m) = ((( upper_sum (f,T)) . m) + (( - ( lower_sum (f,T))) . m)) by SEQ_1: 7

          .= ((( upper_sum (f,T)) . m) + ( - (( lower_sum (f,T)) . m))) by SEQ_1: 10

          .= ((( upper_sum (f,T)) . m) - (( lower_sum (f,T)) . m))

          .= (( upper_sum (f,(T . mm))) - (( lower_sum (f,T)) . m)) by INTEGRA2:def 2

          .= (( upper_sum (f,(T . mm))) - ( lower_sum (f,(T . mm)))) by INTEGRA2:def 3

          .= (( Sum ( upper_volume (f,D))) - ( lower_sum (f,(T . mm)))) by INTEGRA1:def 8

          .= (( Sum ( upper_volume (f,D))) - ( Sum ( lower_volume (f,D)))) by INTEGRA1:def 9;

          then (osc . m) = ( Sum (UV - LV)) by RVSUM_1: 90;

          then

           A120: (osc1 . m) <= (osc . m) by A14, A15, RVSUM_1: 82;

          then |.(osc . m).| = (osc . m) by A118, ABSVALUE:def 1;

          hence thesis by A108, A120, A119, XXREAL_0: 2;

        end;

        then osc1 is convergent by SEQ_2:def 6;

        then

         A121: ( lim (( upper_sum (( max+ f),T)) - ( lower_sum (( max+ f),T)))) = 0 by A12, SEQ_2:def 7;

        

         A122: ( lower_sum (( max+ f),T)) is convergent by A3, A5, A4, A6, A7, Th8;

        ( upper_sum (( max+ f),T)) is convergent by A3, A5, A4, A6, A7, Th9;

        hence thesis by A122, A121, SEQ_2: 12;

      end;

      hence thesis by A3, A5, A4, Th12;

    end;

    theorem :: INTEGRA4:21

    

     Th21: for f be PartFunc of C, REAL holds ( max- f) = ( max+ ( - f))

    proof

      let f be PartFunc of C, REAL ;

      ( dom ( max+ ( - f))) = ( dom ( - f)) by RFUNCT_3:def 10;

      then

       A1: ( dom ( max+ ( - f))) = ( dom f) by VALUED_1: 8;

      

       A2: ( dom ( max- f)) = ( dom f) by RFUNCT_3:def 11;

      for x1 be Element of C st x1 in ( dom f) holds (( max- f) . x1) = (( max+ ( - f)) . x1)

      proof

        let x1 be Element of C;

        assume

         A3: x1 in ( dom f);

        

        then

         A4: (( max+ ( - f)) . x1) = ( max+ (( - f) . x1)) by A1, RFUNCT_3:def 10

        .= ( max ((( - f) . x1), 0 )) by RFUNCT_3:def 1

        .= ( max (( - (f . x1)), 0 )) by VALUED_1: 8;

        (( max- f) . x1) = ( max- (f . x1)) by A2, A3, RFUNCT_3:def 11

        .= ( max (( - (f . x1)), 0 )) by RFUNCT_3:def 2;

        hence thesis by A4;

      end;

      hence thesis by A2, A1, PARTFUN1: 5;

    end;

    theorem :: INTEGRA4:22

    

     Th22: for f be Function of A, REAL st (f | A) is bounded & f is integrable holds ( max- f) is integrable

    proof

      let f be Function of A, REAL ;

      assume that

       A1: (f | A) is bounded and

       A2: f is integrable;

      

       A3: (( - f) | A) is bounded by A1, RFUNCT_1: 82;

      (( - 1) (#) f) is integrable by A1, A2, INTEGRA2: 31;

      then ( max+ ( - f)) is integrable by A3, Th20;

      hence thesis by Th21;

    end;

    theorem :: INTEGRA4:23

    for f be Function of A, REAL st (f | A) is bounded & f is integrable holds ( abs f) is integrable & |.( integral f).| <= ( integral ( abs f))

    proof

      let f be Function of A, REAL ;

      assume that

       A1: (f | A) is bounded and

       A2: f is integrable;

      

       A3: ( max- f) is integrable by A1, A2, Th22;

      

       A4: (( max+ f) | A) is bounded_above by A1, Th14;

      

       A5: (( max- f) | A) is bounded_above by A1, Th16;

      

       A6: ( max+ f) is total by Th13;

      

       A7: (( max- f) | A) is bounded_below by Th17;

      

       A8: (( max+ f) | A) is bounded_below by Th15;

      

       A9: ( max- f) is total by Th13;

      

       A10: ( max+ f) is integrable by A1, A2, Th20;

      then (( max+ f) + ( max- f)) is integrable by A6, A9, A4, A8, A5, A7, A3, INTEGRA1: 57;

      hence ( abs f) is integrable by RFUNCT_3: 34;

      

       A11: (( integral ( max+ f)) - ( integral ( max- f))) = ( integral (( max+ f) - ( max- f))) by A6, A9, A4, A8, A5, A7, A10, A3, INTEGRA2: 33

      .= ( integral f) by RFUNCT_3: 34;

      

       A12: (( integral ( max+ f)) + ( integral ( max- f))) = ( integral (( max+ f) + ( max- f))) by A6, A9, A4, A8, A5, A7, A10, A3, INTEGRA1: 57

      .= ( integral ( abs f)) by RFUNCT_3: 34;

      then

       A13: (( integral ( abs f)) - ( integral f)) = (2 * ( integral ( max- f))) by A11;

      for x st x in A holds (( max- f) . x) >= 0 by RFUNCT_3: 40;

      then ( integral ( max- f)) >= 0 by A9, A5, A7, INTEGRA2: 32;

      then

       A14: ( integral ( abs f)) >= ( integral f) by A13, XREAL_1: 49;

      

       A15: (( integral ( abs f)) + ( integral f)) = (2 * ( integral ( max+ f))) by A12, A11;

      for x st x in A holds (( max+ f) . x) >= 0 by RFUNCT_3: 37;

      then ( integral ( max+ f)) >= 0 by A6, A4, A8, INTEGRA2: 32;

      then ( - ( integral ( abs f))) <= ( integral f) by A15, XREAL_1: 61;

      hence thesis by A14, ABSVALUE: 5;

    end;

    theorem :: INTEGRA4:24

    

     Th24: for f be Function of A, REAL st (for x, y st x in A & y in A holds |.((f . x) - (f . y)).| <= a) holds (( upper_bound ( rng f)) - ( lower_bound ( rng f))) <= a

    proof

      let f be Function of A, REAL ;

      assume

       A1: for x, y st x in A & y in A holds |.((f . x) - (f . y)).| <= a;

      

       A2: for y be Real st y in A holds (( upper_bound ( rng f)) - a) <= (f . y)

      proof

        let y be Real;

        assume

         A3: y in A;

        for b be Real st b in ( rng f) holds b <= (a + (f . y))

        proof

          let b be Real;

          assume b in ( rng f);

          then

          consider x be Element of A such that x in ( dom f) and

           A4: b = (f . x) by PARTFUN1: 3;

           |.((f . x) - (f . y)).| <= a by A1, A3;

          then ((f . x) - (f . y)) <= a by ABSVALUE: 5;

          hence thesis by A4, XREAL_1: 20;

        end;

        then ( upper_bound ( rng f)) <= (a + (f . y)) by SEQ_4: 45;

        hence thesis by XREAL_1: 20;

      end;

      for b be Real st b in ( rng f) holds (( upper_bound ( rng f)) - a) <= b

      proof

        let b be Real;

        assume b in ( rng f);

        then ex x be Element of A st x in ( dom f) & b = (f . x) by PARTFUN1: 3;

        hence thesis by A2;

      end;

      then (( upper_bound ( rng f)) - a) <= ( lower_bound ( rng f)) by SEQ_4: 43;

      then ( upper_bound ( rng f)) <= (a + ( lower_bound ( rng f))) by XREAL_1: 20;

      hence thesis by XREAL_1: 20;

    end;

    theorem :: INTEGRA4:25

    

     Th25: for f,g be Function of A, REAL st (f | A) is bounded & a >= 0 & (for x, y st x in A & y in A holds |.((g . x) - (g . y)).| <= (a * |.((f . x) - (f . y)).|)) holds (( upper_bound ( rng g)) - ( lower_bound ( rng g))) <= (a * (( upper_bound ( rng f)) - ( lower_bound ( rng f))))

    proof

      let f,g be Function of A, REAL ;

      assume that

       A1: (f | A) is bounded and

       A2: a >= 0 and

       A3: for x, y st x in A & y in A holds |.((g . x) - (g . y)).| <= (a * |.((f . x) - (f . y)).|);

      

       A4: ( rng f) is bounded_above by A1, INTEGRA1: 13;

      

       A5: ( dom f) = A by FUNCT_2:def 1;

      

       A6: ( rng f) is bounded_below by A1, INTEGRA1: 11;

      

       A7: for x, y st x in A & y in A holds |.((f . x) - (f . y)).| <= (( upper_bound ( rng f)) - ( lower_bound ( rng f)))

      proof

        let x, y;

        assume that

         A8: x in A and

         A9: y in A;

        now

          per cases ;

            suppose (f . x) >= (f . y);

            then ((f . x) - (f . y)) >= 0 by XREAL_1: 48;

            then |.((f . x) - (f . y)).| = ((f . x) - (f . y)) by ABSVALUE:def 1;

            then

             A10: ( |.((f . x) - (f . y)).| + (f . y)) = (f . x);

            (f . y) in ( rng f) by A5, A9, FUNCT_1:def 3;

            then

             A11: ( lower_bound ( rng f)) <= (f . y) by A6, SEQ_4:def 2;

            (f . x) in ( rng f) by A5, A8, FUNCT_1:def 3;

            then (f . x) <= ( upper_bound ( rng f)) by A4, SEQ_4:def 1;

            then (f . y) <= (( upper_bound ( rng f)) - |.((f . x) - (f . y)).|) by A10, XREAL_1: 19;

            then ( lower_bound ( rng f)) <= (( upper_bound ( rng f)) - |.((f . x) - (f . y)).|) by A11, XXREAL_0: 2;

            then (( lower_bound ( rng f)) + |.((f . x) - (f . y)).|) <= ( upper_bound ( rng f)) by XREAL_1: 19;

            hence thesis by XREAL_1: 19;

          end;

            suppose (f . x) < (f . y);

            then ((f . x) - (f . y)) < 0 by XREAL_1: 49;

            

            then |.((f . x) - (f . y)).| = ( - ((f . x) - (f . y))) by ABSVALUE:def 1

            .= ((f . y) - (f . x));

            then

             A12: ( |.((f . x) - (f . y)).| + (f . x)) = (f . y);

            (f . x) in ( rng f) by A5, A8, FUNCT_1:def 3;

            then

             A13: ( lower_bound ( rng f)) <= (f . x) by A6, SEQ_4:def 2;

            (f . y) in ( rng f) by A5, A9, FUNCT_1:def 3;

            then (f . y) <= ( upper_bound ( rng f)) by A4, SEQ_4:def 1;

            then (f . x) <= (( upper_bound ( rng f)) - |.((f . x) - (f . y)).|) by A12, XREAL_1: 19;

            then ( lower_bound ( rng f)) <= (( upper_bound ( rng f)) - |.((f . x) - (f . y)).|) by A13, XXREAL_0: 2;

            then (( lower_bound ( rng f)) + |.((f . x) - (f . y)).|) <= ( upper_bound ( rng f)) by XREAL_1: 19;

            hence thesis by XREAL_1: 19;

          end;

        end;

        hence thesis;

      end;

      for x, y st x in A & y in A holds |.((g . x) - (g . y)).| <= (a * (( upper_bound ( rng f)) - ( lower_bound ( rng f))))

      proof

        let x, y;

        assume that

         A14: x in A and

         A15: y in A;

        

         A16: |.((g . x) - (g . y)).| <= (a * |.((f . x) - (f . y)).|) by A3, A14, A15;

        (a * |.((f . x) - (f . y)).|) <= (a * (( upper_bound ( rng f)) - ( lower_bound ( rng f)))) by A2, A7, A14, A15, XREAL_1: 64;

        hence thesis by A16, XXREAL_0: 2;

      end;

      hence thesis by Th24;

    end;

    theorem :: INTEGRA4:26

    

     Th26: for f,g,h be Function of A, REAL st (f | A) is bounded & (g | A) is bounded & a >= 0 & (for x, y st x in A & y in A holds |.((h . x) - (h . y)).| <= (a * ( |.((f . x) - (f . y)).| + |.((g . x) - (g . y)).|))) holds (( upper_bound ( rng h)) - ( lower_bound ( rng h))) <= (a * ((( upper_bound ( rng f)) - ( lower_bound ( rng f))) + (( upper_bound ( rng g)) - ( lower_bound ( rng g)))))

    proof

      let f,g,h be Function of A, REAL ;

      assume that

       A1: (f | A) is bounded and

       A2: (g | A) is bounded and

       A3: a >= 0 and

       A4: for x, y st x in A & y in A holds |.((h . x) - (h . y)).| <= (a * ( |.((f . x) - (f . y)).| + |.((g . x) - (g . y)).|));

      

       A5: ( rng g) is bounded_above by A2, INTEGRA1: 13;

      

       A6: ( rng f) is bounded_above by A1, INTEGRA1: 13;

      

       A7: ( dom g) = A by FUNCT_2:def 1;

      

       A8: ( rng g) is bounded_below by A2, INTEGRA1: 11;

      

       A9: for x, y st x in A & y in A holds |.((g . x) - (g . y)).| <= (( upper_bound ( rng g)) - ( lower_bound ( rng g)))

      proof

        let x, y;

        assume that

         A10: x in A and

         A11: y in A;

        now

          per cases ;

            suppose (g . x) >= (g . y);

            then ((g . x) - (g . y)) >= 0 by XREAL_1: 48;

            then |.((g . x) - (g . y)).| = ((g . x) - (g . y)) by ABSVALUE:def 1;

            then

             A12: ( |.((g . x) - (g . y)).| + (g . y)) = (g . x);

            (g . y) in ( rng g) by A7, A11, FUNCT_1:def 3;

            then

             A13: ( lower_bound ( rng g)) <= (g . y) by A8, SEQ_4:def 2;

            (g . x) in ( rng g) by A7, A10, FUNCT_1:def 3;

            then (g . x) <= ( upper_bound ( rng g)) by A5, SEQ_4:def 1;

            then (g . y) <= (( upper_bound ( rng g)) - |.((g . x) - (g . y)).|) by A12, XREAL_1: 19;

            then ( lower_bound ( rng g)) <= (( upper_bound ( rng g)) - |.((g . x) - (g . y)).|) by A13, XXREAL_0: 2;

            then (( lower_bound ( rng g)) + |.((g . x) - (g . y)).|) <= ( upper_bound ( rng g)) by XREAL_1: 19;

            hence thesis by XREAL_1: 19;

          end;

            suppose (g . x) < (g . y);

            then ((g . x) - (g . y)) < 0 by XREAL_1: 49;

            

            then |.((g . x) - (g . y)).| = ( - ((g . x) - (g . y))) by ABSVALUE:def 1

            .= ((g . y) - (g . x));

            then

             A14: ( |.((g . x) - (g . y)).| + (g . x)) = (g . y);

            (g . x) in ( rng g) by A7, A10, FUNCT_1:def 3;

            then

             A15: ( lower_bound ( rng g)) <= (g . x) by A8, SEQ_4:def 2;

            (g . y) in ( rng g) by A7, A11, FUNCT_1:def 3;

            then (g . y) <= ( upper_bound ( rng g)) by A5, SEQ_4:def 1;

            then (g . x) <= (( upper_bound ( rng g)) - |.((g . x) - (g . y)).|) by A14, XREAL_1: 19;

            then ( lower_bound ( rng g)) <= (( upper_bound ( rng g)) - |.((g . x) - (g . y)).|) by A15, XXREAL_0: 2;

            then (( lower_bound ( rng g)) + |.((g . x) - (g . y)).|) <= ( upper_bound ( rng g)) by XREAL_1: 19;

            hence thesis by XREAL_1: 19;

          end;

        end;

        hence thesis;

      end;

      

       A16: ( dom f) = A by FUNCT_2:def 1;

      

       A17: ( rng f) is bounded_below by A1, INTEGRA1: 11;

      

       A18: for x, y st x in A & y in A holds |.((f . x) - (f . y)).| <= (( upper_bound ( rng f)) - ( lower_bound ( rng f)))

      proof

        let x, y;

        assume that

         A19: x in A and

         A20: y in A;

        now

          per cases ;

            suppose (f . x) >= (f . y);

            then ((f . x) - (f . y)) >= 0 by XREAL_1: 48;

            then |.((f . x) - (f . y)).| = ((f . x) - (f . y)) by ABSVALUE:def 1;

            then

             A21: ( |.((f . x) - (f . y)).| + (f . y)) = (f . x);

            (f . y) in ( rng f) by A16, A20, FUNCT_1:def 3;

            then

             A22: ( lower_bound ( rng f)) <= (f . y) by A17, SEQ_4:def 2;

            (f . x) in ( rng f) by A16, A19, FUNCT_1:def 3;

            then (f . x) <= ( upper_bound ( rng f)) by A6, SEQ_4:def 1;

            then (f . y) <= (( upper_bound ( rng f)) - |.((f . x) - (f . y)).|) by A21, XREAL_1: 19;

            then ( lower_bound ( rng f)) <= (( upper_bound ( rng f)) - |.((f . x) - (f . y)).|) by A22, XXREAL_0: 2;

            then (( lower_bound ( rng f)) + |.((f . x) - (f . y)).|) <= ( upper_bound ( rng f)) by XREAL_1: 19;

            hence thesis by XREAL_1: 19;

          end;

            suppose (f . x) < (f . y);

            then ((f . x) - (f . y)) < 0 by XREAL_1: 49;

            

            then |.((f . x) - (f . y)).| = ( - ((f . x) - (f . y))) by ABSVALUE:def 1

            .= ((f . y) - (f . x));

            then

             A23: ( |.((f . x) - (f . y)).| + (f . x)) = (f . y);

            (f . x) in ( rng f) by A16, A19, FUNCT_1:def 3;

            then

             A24: ( lower_bound ( rng f)) <= (f . x) by A17, SEQ_4:def 2;

            (f . y) in ( rng f) by A16, A20, FUNCT_1:def 3;

            then (f . y) <= ( upper_bound ( rng f)) by A6, SEQ_4:def 1;

            then (f . x) <= (( upper_bound ( rng f)) - |.((f . x) - (f . y)).|) by A23, XREAL_1: 19;

            then ( lower_bound ( rng f)) <= (( upper_bound ( rng f)) - |.((f . x) - (f . y)).|) by A24, XXREAL_0: 2;

            then (( lower_bound ( rng f)) + |.((f . x) - (f . y)).|) <= ( upper_bound ( rng f)) by XREAL_1: 19;

            hence thesis by XREAL_1: 19;

          end;

        end;

        hence thesis;

      end;

      for x, y st x in A & y in A holds |.((h . x) - (h . y)).| <= (a * ((( upper_bound ( rng f)) - ( lower_bound ( rng f))) + (( upper_bound ( rng g)) - ( lower_bound ( rng g)))))

      proof

        let x, y;

        assume that

         A25: x in A and

         A26: y in A;

        

         A27: (a * |.((g . x) - (g . y)).|) <= (a * (( upper_bound ( rng g)) - ( lower_bound ( rng g)))) by A3, A9, A25, A26, XREAL_1: 64;

        (a * |.((f . x) - (f . y)).|) <= (a * (( upper_bound ( rng f)) - ( lower_bound ( rng f)))) by A3, A18, A25, A26, XREAL_1: 64;

        then

         A28: ((a * |.((f . x) - (f . y)).|) + (a * |.((g . x) - (g . y)).|)) <= ((a * (( upper_bound ( rng f)) - ( lower_bound ( rng f)))) + (a * (( upper_bound ( rng g)) - ( lower_bound ( rng g))))) by A27, XREAL_1: 7;

         |.((h . x) - (h . y)).| <= (a * ( |.((f . x) - (f . y)).| + |.((g . x) - (g . y)).|)) by A4, A25, A26;

        hence thesis by A28, XXREAL_0: 2;

      end;

      hence thesis by Th24;

    end;

    theorem :: INTEGRA4:27

    

     Th27: for f,g be Function of A, REAL st (f | A) is bounded & f is integrable & (g | A) is bounded & a > 0 & (for x, y st x in A & y in A holds |.((g . x) - (g . y)).| <= (a * |.((f . x) - (f . y)).|)) holds g is integrable

    proof

      let f,g be Function of A, REAL ;

      assume that

       A1: (f | A) is bounded and

       A2: f is integrable and

       A3: (g | A) is bounded and

       A4: a > 0 and

       A5: for x, y st x in A & y in A holds |.((g . x) - (g . y)).| <= (a * |.((f . x) - (f . y)).|);

      for T be DivSequence of A st ( delta T) is convergent & ( lim ( delta T)) = 0 holds (( lim ( upper_sum (g,T))) - ( lim ( lower_sum (g,T)))) = 0

      proof

        let T be DivSequence of A;

        assume that

         A6: ( delta T) is convergent and

         A7: ( lim ( delta T)) = 0 ;

        

         A8: ( lower_sum (f,T)) is convergent by A1, A6, A7, Th8;

        

         A9: ( upper_sum (f,T)) is convergent by A1, A6, A7, Th9;

        then

         A10: (( upper_sum (f,T)) - ( lower_sum (f,T))) is convergent by A8;

        reconsider osc1 = (( upper_sum (g,T)) - ( lower_sum (g,T))) as Real_Sequence;

        reconsider osc = (( upper_sum (f,T)) - ( lower_sum (f,T))) as Real_Sequence;

        (( lim ( upper_sum (f,T))) - ( lim ( lower_sum (f,T)))) = 0 by A1, A2, A6, A7, Th12;

        then

         A11: ( lim (( upper_sum (f,T)) - ( lower_sum (f,T)))) = 0 by A9, A8, SEQ_2: 12;

        

         A12: for b be Real st 0 < b holds ex n be Nat st for m be Nat st n <= m holds |.((osc1 . m) - 0 ).| < b

        proof

          let b be Real;

          assume b > 0 ;

          then (b / a) > 0 by A4, XREAL_1: 139;

          then

          consider n be Nat such that

           A13: for m be Nat st n <= m holds |.((osc . m) - 0 ).| < (b / a) by A10, A11, SEQ_2:def 7;

          take n;

          let m be Nat;

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

          reconsider D = (T . mm) as Division of A;

          ( len ( upper_volume (f,D))) = ( len D) by INTEGRA1:def 6;

          then

          reconsider UV = ( upper_volume (f,D)) as Element of (( len D) -tuples_on REAL ) by FINSEQ_2: 133;

          ( len ( lower_volume (f,D))) = ( len D) by INTEGRA1:def 7;

          then

          reconsider LV = ( lower_volume (f,D)) as Element of (( len D) -tuples_on REAL ) by FINSEQ_2: 133;

          (osc . m) = ((( upper_sum (f,T)) . m) + (( - ( lower_sum (f,T))) . m)) by SEQ_1: 7

          .= ((( upper_sum (f,T)) . m) + ( - (( lower_sum (f,T)) . m))) by SEQ_1: 10

          .= ((( upper_sum (f,T)) . m) - (( lower_sum (f,T)) . m))

          .= (( upper_sum (f,(T . mm))) - (( lower_sum (f,T)) . m)) by INTEGRA2:def 2

          .= (( upper_sum (f,(T . mm))) - ( lower_sum (f,(T . mm)))) by INTEGRA2:def 3

          .= (( Sum ( upper_volume (f,D))) - ( lower_sum (f,(T . mm)))) by INTEGRA1:def 8

          .= (( Sum ( upper_volume (f,D))) - ( Sum ( lower_volume (f,D)))) by INTEGRA1:def 9;

          then

           A14: (osc . m) = ( Sum (UV - LV)) by RVSUM_1: 90;

          assume n <= m;

          then

           A15: |.((osc . m) - 0 ).| < (b / a) by A13;

          ( len ( lower_volume (g,D))) = ( len D) by INTEGRA1:def 7;

          then

          reconsider LV1 = ( lower_volume (g,D)) as Element of (( len D) -tuples_on REAL ) by FINSEQ_2: 133;

          ( len ( upper_volume (g,D))) = ( len D) by INTEGRA1:def 6;

          then

          reconsider UV1 = ( upper_volume (g,D)) as Element of (( len D) -tuples_on REAL ) by FINSEQ_2: 133;

          reconsider F = (UV1 - LV1) as FinSequence of REAL ;

          (osc1 . m) = ((( upper_sum (g,T)) . m) + (( - ( lower_sum (g,T))) . m)) by SEQ_1: 7

          .= ((( upper_sum (g,T)) . m) + ( - (( lower_sum (g,T)) . m))) by SEQ_1: 10

          .= ((( upper_sum (g,T)) . m) - (( lower_sum (g,T)) . m))

          .= (( upper_sum (g,(T . mm))) - (( lower_sum (g,T)) . m)) by INTEGRA2:def 2

          .= (( upper_sum (g,(T . mm))) - ( lower_sum (g,(T . mm)))) by INTEGRA2:def 3

          .= (( Sum ( upper_volume (g,D))) - ( lower_sum (g,(T . mm)))) by INTEGRA1:def 8

          .= (( Sum ( upper_volume (g,D))) - ( Sum ( lower_volume (g,D)))) by INTEGRA1:def 9;

          then

           A16: (osc1 . m) = ( Sum (UV1 - LV1)) by RVSUM_1: 90;

          for j be Nat st j in ( dom F) holds 0 <= (F . j)

          proof

            let j be Nat;

            set r = (F . j);

            

             A17: ( rng g) is bounded_below by A3, INTEGRA1: 11;

            assume that

             A18: j in ( dom F);

            j in ( Seg ( len F)) by A18, FINSEQ_1:def 3;

            then

             A19: j in ( Seg ( len D)) by CARD_1:def 7;

            then

             A20: j in ( dom D) by FINSEQ_1:def 3;

            then

             A21: (LV1 . j) = (( lower_bound ( rng (g | ( divset (D,j))))) * ( vol ( divset (D,j)))) by INTEGRA1:def 7;

            

             A22: ex r st r in ( rng (g | ( divset (D,j))))

            proof

              consider r be Element of REAL such that

               A23: r in ( divset (D,j)) by SUBSET_1: 4;

              j in ( dom D) by A19, FINSEQ_1:def 3;

              then ( divset (D,j)) c= A by INTEGRA1: 8;

              then r in A by A23;

              then r in ( dom g) by FUNCT_2:def 1;

              then r in (( dom g) /\ ( divset (D,j))) by A23, XBOOLE_0:def 4;

              then r in ( dom (g | ( divset (D,j)))) by RELAT_1: 61;

              then ((g | ( divset (D,j))) . r) in ( rng (g | ( divset (D,j)))) by FUNCT_1:def 3;

              hence thesis;

            end;

            ( rng g) is bounded_above by A3, INTEGRA1: 13;

            then ( rng (g | ( divset (D,j)))) is real-bounded by A17, RELAT_1: 70, XXREAL_2: 45;

            then

             A24: (( upper_bound ( rng (g | ( divset (D,j))))) - ( lower_bound ( rng (g | ( divset (D,j)))))) >= 0 by A22, SEQ_4: 11, XREAL_1: 48;

            (UV1 . j) = (( upper_bound ( rng (g | ( divset (D,j))))) * ( vol ( divset (D,j)))) by A20, INTEGRA1:def 6;

            

            then

             A25: r = ((( upper_bound ( rng (g | ( divset (D,j))))) * ( vol ( divset (D,j)))) - (( lower_bound ( rng (g | ( divset (D,j))))) * ( vol ( divset (D,j))))) by A18, A21, VALUED_1: 13

            .= ((( upper_bound ( rng (g | ( divset (D,j))))) - ( lower_bound ( rng (g | ( divset (D,j)))))) * ( vol ( divset (D,j))));

            ( vol ( divset (D,j))) >= 0 by INTEGRA1: 9;

            hence thesis by A25, A24;

          end;

          then

           A26: (osc1 . m) >= 0 by A16, RVSUM_1: 84;

          then

           A27: |.(osc1 . m).| = (osc1 . m) by ABSVALUE:def 1;

          for j be Nat st j in ( Seg ( len D)) holds ((UV1 - LV1) . j) <= ((a * (UV - LV)) . j)

          proof

            let j be Nat;

            set x = ((UV1 - LV1) . j), y = ((a * (UV - LV)) . j);

            

             A28: y = (a * ((UV - LV) . j)) by RVSUM_1: 45;

            assume

             A29: j in ( Seg ( len D));

            then

             A30: j in ( dom D) by FINSEQ_1:def 3;

            then

             A31: (LV1 . j) = (( lower_bound ( rng (g | ( divset (D,j))))) * ( vol ( divset (D,j)))) by INTEGRA1:def 7;

            

             A32: (a * (( upper_bound ( rng (f | ( divset (D,j))))) - ( lower_bound ( rng (f | ( divset (D,j))))))) >= (( upper_bound ( rng (g | ( divset (D,j))))) - ( lower_bound ( rng (g | ( divset (D,j))))))

            proof

              

               A33: j in ( dom D) by A29, FINSEQ_1:def 3;

              then

               A34: ((f | ( divset (D,j))) | ( divset (D,j))) is bounded_below by A1, INTEGRA1: 8, INTEGRA2: 6;

              

               A35: ( dom (g | ( divset (D,j)))) = (( dom g) /\ ( divset (D,j))) by RELAT_1: 61

              .= (A /\ ( divset (D,j))) by FUNCT_2:def 1

              .= ( divset (D,j)) by A33, INTEGRA1: 8, XBOOLE_1: 28;

              then

              reconsider g1 = (g | ( divset (D,j))) as PartFunc of ( divset (D,j)), REAL by RELSET_1: 5;

              

               A36: ( dom (f | ( divset (D,j)))) = (( dom f) /\ ( divset (D,j))) by RELAT_1: 61

              .= (A /\ ( divset (D,j))) by FUNCT_2:def 1

              .= ( divset (D,j)) by A33, INTEGRA1: 8, XBOOLE_1: 28;

              then

              reconsider f1 = (f | ( divset (D,j))) as PartFunc of ( divset (D,j)), REAL by RELSET_1: 5;

              reconsider g1 as Function of ( divset (D,j)), REAL by A35, FUNCT_2:def 1;

              reconsider f1 as Function of ( divset (D,j)), REAL by A36, FUNCT_2:def 1;

              

               A37: ( divset (D,j)) c= A by A33, INTEGRA1: 8;

              

               A38: for x, y st x in ( divset (D,j)) & y in ( divset (D,j)) holds |.((g1 . x) - (g1 . y)).| <= (a * |.((f1 . x) - (f1 . y)).|)

              proof

                let x, y;

                assume that

                 A39: x in ( divset (D,j)) and

                 A40: y in ( divset (D,j));

                

                 A41: (g . y) = (g1 . y) by A35, A40, FUNCT_1: 47;

                

                 A42: (f . y) = (f1 . y) by A36, A40, FUNCT_1: 47;

                

                 A43: (f . x) = (f1 . x) by A36, A39, FUNCT_1: 47;

                (g . x) = (g1 . x) by A35, A39, FUNCT_1: 47;

                hence thesis by A5, A37, A39, A40, A41, A43, A42;

              end;

              ((f | ( divset (D,j))) | ( divset (D,j))) is bounded_above by A1, A33, INTEGRA1: 8, INTEGRA2: 5;

              then (f1 | ( divset (D,j))) is bounded by A34;

              hence thesis by A4, A38, Th25;

            end;

            ( vol ( divset (D,j))) >= 0 by INTEGRA1: 9;

            then

             A44: ((a * (( upper_bound ( rng (f | ( divset (D,j))))) - ( lower_bound ( rng (f | ( divset (D,j))))))) * ( vol ( divset (D,j)))) >= ((( upper_bound ( rng (g | ( divset (D,j))))) - ( lower_bound ( rng (g | ( divset (D,j)))))) * ( vol ( divset (D,j)))) by A32, XREAL_1: 64;

            (UV1 . j) = (( upper_bound ( rng (g | ( divset (D,j))))) * ( vol ( divset (D,j)))) by A30, INTEGRA1:def 6;

            

            then

             A45: x = ((( upper_bound ( rng (g | ( divset (D,j))))) * ( vol ( divset (D,j)))) - (( lower_bound ( rng (g | ( divset (D,j))))) * ( vol ( divset (D,j))))) by A31, RVSUM_1: 27

            .= ((( upper_bound ( rng (g | ( divset (D,j))))) - ( lower_bound ( rng (g | ( divset (D,j)))))) * ( vol ( divset (D,j))));

            

             A46: (LV . j) = (( lower_bound ( rng (f | ( divset (D,j))))) * ( vol ( divset (D,j)))) by A30, INTEGRA1:def 7;

            (UV . j) = (( upper_bound ( rng (f | ( divset (D,j))))) * ( vol ( divset (D,j)))) by A30, INTEGRA1:def 6;

            

            then y = (a * ((( upper_bound ( rng (f | ( divset (D,j))))) * ( vol ( divset (D,j)))) - (( lower_bound ( rng (f | ( divset (D,j))))) * ( vol ( divset (D,j)))))) by A46, A28, RVSUM_1: 27

            .= (a * ((( upper_bound ( rng (f | ( divset (D,j))))) - ( lower_bound ( rng (f | ( divset (D,j)))))) * ( vol ( divset (D,j)))));

            hence thesis by A45, A44;

          end;

          then (osc1 . m) <= ( Sum (a * (UV - LV))) by A16, RVSUM_1: 82;

          then

           A47: (osc1 . m) <= (a * (osc . m)) by A14, RVSUM_1: 87;

          then (osc . m) >= ( 0 / a) by A4, A26, XREAL_1: 79;

          then |.(osc . m).| = (osc . m) by ABSVALUE:def 1;

          then (a * (osc . m)) < (a * (b / a)) by A4, A15, XREAL_1: 68;

          then (a * (osc . m)) < b by A4, XCMPLX_1: 87;

          hence thesis by A47, A27, XXREAL_0: 2;

        end;

        then osc1 is convergent by SEQ_2:def 6;

        then

         A48: ( lim (( upper_sum (g,T)) - ( lower_sum (g,T)))) = 0 by A12, SEQ_2:def 7;

        

         A49: ( lower_sum (g,T)) is convergent by A3, A6, A7, Th8;

        ( upper_sum (g,T)) is convergent by A3, A6, A7, Th9;

        hence thesis by A49, A48, SEQ_2: 12;

      end;

      hence thesis by A3, Th12;

    end;

    theorem :: INTEGRA4:28

    

     Th28: for f,g,h be Function of A, REAL st (f | A) is bounded & f is integrable & (g | A) is bounded & g is integrable & (h | A) is bounded & a > 0 & (for x, y st x in A & y in A holds |.((h . x) - (h . y)).| <= (a * ( |.((f . x) - (f . y)).| + |.((g . x) - (g . y)).|))) holds h is integrable

    proof

      let f,g,h be Function of A, REAL ;

      assume that

       A1: (f | A) is bounded and

       A2: f is integrable and

       A3: (g | A) is bounded and

       A4: g is integrable and

       A5: (h | A) is bounded and

       A6: a > 0 and

       A7: for x, y st x in A & y in A holds |.((h . x) - (h . y)).| <= (a * ( |.((f . x) - (f . y)).| + |.((g . x) - (g . y)).|));

      for T be DivSequence of A st ( delta T) is convergent & ( lim ( delta T)) = 0 holds (( lim ( upper_sum (h,T))) - ( lim ( lower_sum (h,T)))) = 0

      proof

        let T be DivSequence of A;

        assume that

         A8: ( delta T) is convergent and

         A9: ( lim ( delta T)) = 0 ;

        

         A10: ( lower_sum (g,T)) is convergent by A3, A8, A9, Th8;

        

         A11: ( upper_sum (g,T)) is convergent by A3, A8, A9, Th9;

        then

         A12: (( upper_sum (g,T)) - ( lower_sum (g,T))) is convergent by A10;

        (( lim ( upper_sum (g,T))) - ( lim ( lower_sum (g,T)))) = 0 by A3, A4, A8, A9, Th12;

        then

         A13: ( lim (( upper_sum (g,T)) - ( lower_sum (g,T)))) = 0 by A11, A10, SEQ_2: 12;

        

         A14: ( lower_sum (f,T)) is convergent by A1, A8, A9, Th8;

        reconsider osc2 = (( upper_sum (h,T)) - ( lower_sum (h,T))) as Real_Sequence;

        reconsider osc1 = (( upper_sum (g,T)) - ( lower_sum (g,T))) as Real_Sequence;

        reconsider osc = (( upper_sum (f,T)) - ( lower_sum (f,T))) as Real_Sequence;

        

         A15: ( upper_sum (f,T)) is convergent by A1, A8, A9, Th9;

        (( lim ( upper_sum (f,T))) - ( lim ( lower_sum (f,T)))) = 0 by A1, A2, A8, A9, Th12;

        then

         A16: ( lim (( upper_sum (f,T)) - ( lower_sum (f,T)))) = 0 by A15, A14, SEQ_2: 12;

        

         A17: (( upper_sum (f,T)) - ( lower_sum (f,T))) is convergent by A15, A14;

        

         A18: for b be Real st 0 < b holds ex n be Nat st for m be Nat st n <= m holds |.((osc2 . m) - 0 ).| < b

        proof

          let b be Real;

          assume b > 0 ;

          then (b / a) > 0 by A6, XREAL_1: 139;

          then

           A19: ((b / a) / 2) > 0 by XREAL_1: 139;

          then

          consider n1 be Nat such that

           A20: for m be Nat st n1 <= m holds |.((osc . m) - 0 ).| < ((b / a) / 2) by A17, A16, SEQ_2:def 7;

          consider n2 be Nat such that

           A21: for m be Nat st n2 <= m holds |.((osc1 . m) - 0 ).| < ((b / a) / 2) by A12, A13, A19, SEQ_2:def 7;

          ex n st n1 <= n & n2 <= n

          proof

            take n = ( max (n1,n2));

            n is Element of NAT by ORDINAL1:def 12;

            hence thesis by XXREAL_0: 25;

          end;

          then

          consider n such that

           A22: n1 <= n and

           A23: n2 <= n;

          take n;

          let m be Nat;

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

          reconsider D = (T . mm) as Division of A;

          ( len ( upper_volume (f,D))) = ( len D) by INTEGRA1:def 6;

          then

          reconsider UV = ( upper_volume (f,D)) as Element of (( len D) -tuples_on REAL ) by FINSEQ_2: 133;

          ( len ( lower_volume (f,D))) = ( len D) by INTEGRA1:def 7;

          then

          reconsider LV = ( lower_volume (f,D)) as Element of (( len D) -tuples_on REAL ) by FINSEQ_2: 133;

          (osc . m) = ((( upper_sum (f,T)) . m) + (( - ( lower_sum (f,T))) . m)) by SEQ_1: 7

          .= ((( upper_sum (f,T)) . m) + ( - (( lower_sum (f,T)) . m))) by SEQ_1: 10

          .= ((( upper_sum (f,T)) . m) - (( lower_sum (f,T)) . m))

          .= (( upper_sum (f,(T . mm))) - (( lower_sum (f,T)) . m)) by INTEGRA2:def 2

          .= (( upper_sum (f,(T . mm))) - ( lower_sum (f,(T . mm)))) by INTEGRA2:def 3

          .= (( Sum ( upper_volume (f,D))) - ( lower_sum (f,(T . mm)))) by INTEGRA1:def 8

          .= (( Sum ( upper_volume (f,D))) - ( Sum ( lower_volume (f,D)))) by INTEGRA1:def 9;

          then

           A24: (osc . m) = ( Sum (UV - LV)) by RVSUM_1: 90;

          ( len ( lower_volume (h,D))) = ( len D) by INTEGRA1:def 7;

          then

          reconsider LV2 = ( lower_volume (h,D)) as Element of (( len D) -tuples_on REAL ) by FINSEQ_2: 133;

          ( len ( upper_volume (h,D))) = ( len D) by INTEGRA1:def 6;

          then

          reconsider UV2 = ( upper_volume (h,D)) as Element of (( len D) -tuples_on REAL ) by FINSEQ_2: 133;

          ( len ( lower_volume (g,D))) = ( len D) by INTEGRA1:def 7;

          then

          reconsider LV1 = ( lower_volume (g,D)) as Element of (( len D) -tuples_on REAL ) by FINSEQ_2: 133;

          ( len ( upper_volume (g,D))) = ( len D) by INTEGRA1:def 6;

          then

          reconsider UV1 = ( upper_volume (g,D)) as Element of (( len D) -tuples_on REAL ) by FINSEQ_2: 133;

          reconsider H = (UV - LV) as FinSequence of REAL ;

          reconsider G = (UV1 - LV1) as FinSequence of REAL ;

          reconsider F = (UV2 - LV2) as FinSequence of REAL ;

          (osc1 . m) = ((( upper_sum (g,T)) . m) + (( - ( lower_sum (g,T))) . m)) by SEQ_1: 7

          .= ((( upper_sum (g,T)) . m) + ( - (( lower_sum (g,T)) . m))) by SEQ_1: 10

          .= ((( upper_sum (g,T)) . m) - (( lower_sum (g,T)) . m))

          .= (( upper_sum (g,(T . mm))) - (( lower_sum (g,T)) . m)) by INTEGRA2:def 2

          .= (( upper_sum (g,(T . mm))) - ( lower_sum (g,(T . mm)))) by INTEGRA2:def 3

          .= (( Sum ( upper_volume (g,D))) - ( lower_sum (g,(T . mm)))) by INTEGRA1:def 8

          .= (( Sum ( upper_volume (g,D))) - ( Sum ( lower_volume (g,D)))) by INTEGRA1:def 9;

          then

           A25: (osc1 . m) = ( Sum (UV1 - LV1)) by RVSUM_1: 90;

          for j be Nat st j in ( dom G) holds 0 <= (G . j)

          proof

            let j be Nat;

            set r = (G . j);

            

             A26: ( rng g) is bounded_below by A3, INTEGRA1: 11;

            assume that

             A27: j in ( dom G);

            j in ( Seg ( len G)) by A27, FINSEQ_1:def 3;

            then

             A28: j in ( Seg ( len D)) by CARD_1:def 7;

            then

             A29: j in ( dom D) by FINSEQ_1:def 3;

            then

             A30: (LV1 . j) = (( lower_bound ( rng (g | ( divset (D,j))))) * ( vol ( divset (D,j)))) by INTEGRA1:def 7;

            

             A31: ex r st r in ( rng (g | ( divset (D,j))))

            proof

              consider r be Element of REAL such that

               A32: r in ( divset (D,j)) by SUBSET_1: 4;

              j in ( dom D) by A28, FINSEQ_1:def 3;

              then ( divset (D,j)) c= A by INTEGRA1: 8;

              then r in A by A32;

              then r in ( dom g) by FUNCT_2:def 1;

              then r in (( dom g) /\ ( divset (D,j))) by A32, XBOOLE_0:def 4;

              then r in ( dom (g | ( divset (D,j)))) by RELAT_1: 61;

              then ((g | ( divset (D,j))) . r) in ( rng (g | ( divset (D,j)))) by FUNCT_1:def 3;

              hence thesis;

            end;

            ( rng g) is bounded_above by A3, INTEGRA1: 13;

            then ( rng (g | ( divset (D,j)))) is real-bounded by A26, RELAT_1: 70, XXREAL_2: 45;

            then

             A33: (( upper_bound ( rng (g | ( divset (D,j))))) - ( lower_bound ( rng (g | ( divset (D,j)))))) >= 0 by A31, SEQ_4: 11, XREAL_1: 48;

            (UV1 . j) = (( upper_bound ( rng (g | ( divset (D,j))))) * ( vol ( divset (D,j)))) by A29, INTEGRA1:def 6;

            

            then

             A34: r = ((( upper_bound ( rng (g | ( divset (D,j))))) * ( vol ( divset (D,j)))) - (( lower_bound ( rng (g | ( divset (D,j))))) * ( vol ( divset (D,j))))) by A27, A30, VALUED_1: 13

            .= ((( upper_bound ( rng (g | ( divset (D,j))))) - ( lower_bound ( rng (g | ( divset (D,j)))))) * ( vol ( divset (D,j))));

            ( vol ( divset (D,j))) >= 0 by INTEGRA1: 9;

            hence thesis by A34, A33;

          end;

          then

           A35: (osc1 . m) >= 0 by A25, RVSUM_1: 84;

          assume

           A36: n <= m;

          then n1 <= m by A22, XXREAL_0: 2;

          then

           A37: |.((osc . m) - 0 ).| < ((b / a) / 2) by A20;

          n2 <= m by A23, A36, XXREAL_0: 2;

          then

           A38: |.((osc1 . m) - 0 ).| < ((b / a) / 2) by A21;

          for j be Nat st j in ( dom H) holds 0 <= (H . j)

          proof

            let j be Nat;

            set r = (H . j);

            

             A39: ( rng f) is bounded_below by A1, INTEGRA1: 11;

            assume that

             A40: j in ( dom H);

            j in ( Seg ( len H)) by A40, FINSEQ_1:def 3;

            then

             A41: j in ( Seg ( len D)) by CARD_1:def 7;

            then

             A42: j in ( dom D) by FINSEQ_1:def 3;

            then

             A43: (LV . j) = (( lower_bound ( rng (f | ( divset (D,j))))) * ( vol ( divset (D,j)))) by INTEGRA1:def 7;

            

             A44: ex r st r in ( rng (f | ( divset (D,j))))

            proof

              consider r be Element of REAL such that

               A45: r in ( divset (D,j)) by SUBSET_1: 4;

              j in ( dom D) by A41, FINSEQ_1:def 3;

              then ( divset (D,j)) c= A by INTEGRA1: 8;

              then r in A by A45;

              then r in ( dom f) by FUNCT_2:def 1;

              then r in (( dom f) /\ ( divset (D,j))) by A45, XBOOLE_0:def 4;

              then r in ( dom (f | ( divset (D,j)))) by RELAT_1: 61;

              then ((f | ( divset (D,j))) . r) in ( rng (f | ( divset (D,j)))) by FUNCT_1:def 3;

              hence thesis;

            end;

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

            then ( rng (f | ( divset (D,j)))) is real-bounded by A39, RELAT_1: 70, XXREAL_2: 45;

            then

             A46: (( upper_bound ( rng (f | ( divset (D,j))))) - ( lower_bound ( rng (f | ( divset (D,j)))))) >= 0 by A44, SEQ_4: 11, XREAL_1: 48;

            (UV . j) = (( upper_bound ( rng (f | ( divset (D,j))))) * ( vol ( divset (D,j)))) by A42, INTEGRA1:def 6;

            

            then

             A47: r = ((( upper_bound ( rng (f | ( divset (D,j))))) * ( vol ( divset (D,j)))) - (( lower_bound ( rng (f | ( divset (D,j))))) * ( vol ( divset (D,j))))) by A40, A43, VALUED_1: 13

            .= ((( upper_bound ( rng (f | ( divset (D,j))))) - ( lower_bound ( rng (f | ( divset (D,j)))))) * ( vol ( divset (D,j))));

            ( vol ( divset (D,j))) >= 0 by INTEGRA1: 9;

            hence thesis by A47, A46;

          end;

          then

           A48: (osc . m) >= 0 by A24, RVSUM_1: 84;

          then ((osc . m) * (osc1 . m)) >= 0 by A35;

          then ( |.(osc . m).| + |.(osc1 . m).|) = |.((osc . m) + (osc1 . m)).| by ABSVALUE: 11;

          then ( |.((osc . m) - 0 ).| + |.(osc1 . m).|) = ((osc . m) + (osc1 . m)) by A48, A35, ABSVALUE:def 1;

          then ((osc . m) + (osc1 . m)) < (((b / a) / 2) + ((b / a) / 2)) by A37, A38, XREAL_1: 8;

          then (a * ((osc . m) + (osc1 . m))) < (a * (b / a)) by A6, XREAL_1: 68;

          then

           A49: (a * ((osc . m) + (osc1 . m))) < b by A6, XCMPLX_1: 87;

          (osc2 . m) = ((( upper_sum (h,T)) . m) + (( - ( lower_sum (h,T))) . m)) by SEQ_1: 7

          .= ((( upper_sum (h,T)) . m) + ( - (( lower_sum (h,T)) . m))) by SEQ_1: 10

          .= ((( upper_sum (h,T)) . m) - (( lower_sum (h,T)) . m))

          .= (( upper_sum (h,(T . mm))) - (( lower_sum (h,T)) . m)) by INTEGRA2:def 2

          .= (( upper_sum (h,(T . mm))) - ( lower_sum (h,(T . mm)))) by INTEGRA2:def 3

          .= (( Sum ( upper_volume (h,D))) - ( lower_sum (h,(T . mm)))) by INTEGRA1:def 8

          .= (( Sum ( upper_volume (h,D))) - ( Sum ( lower_volume (h,D)))) by INTEGRA1:def 9;

          then

           A50: (osc2 . m) = ( Sum (UV2 - LV2)) by RVSUM_1: 90;

          for j be Nat st j in ( dom F) holds 0 <= (F . j)

          proof

            let j be Nat;

            set r = (F . j);

            

             A51: ( rng h) is bounded_below by A5, INTEGRA1: 11;

            assume that

             A52: j in ( dom F);

            j in ( Seg ( len F)) by A52, FINSEQ_1:def 3;

            then

             A53: j in ( Seg ( len D)) by CARD_1:def 7;

            then

             A54: j in ( dom D) by FINSEQ_1:def 3;

            then

             A55: (LV2 . j) = (( lower_bound ( rng (h | ( divset (D,j))))) * ( vol ( divset (D,j)))) by INTEGRA1:def 7;

            

             A56: ex r st r in ( rng (h | ( divset (D,j))))

            proof

              consider r be Element of REAL such that

               A57: r in ( divset (D,j)) by SUBSET_1: 4;

              j in ( dom D) by A53, FINSEQ_1:def 3;

              then ( divset (D,j)) c= A by INTEGRA1: 8;

              then r in A by A57;

              then r in ( dom h) by FUNCT_2:def 1;

              then r in (( dom h) /\ ( divset (D,j))) by A57, XBOOLE_0:def 4;

              then r in ( dom (h | ( divset (D,j)))) by RELAT_1: 61;

              then ((h | ( divset (D,j))) . r) in ( rng (h | ( divset (D,j)))) by FUNCT_1:def 3;

              hence thesis;

            end;

            ( rng h) is bounded_above by A5, INTEGRA1: 13;

            then ( rng (h | ( divset (D,j)))) is real-bounded by A51, RELAT_1: 70, XXREAL_2: 45;

            then

             A58: (( upper_bound ( rng (h | ( divset (D,j))))) - ( lower_bound ( rng (h | ( divset (D,j)))))) >= 0 by A56, SEQ_4: 11, XREAL_1: 48;

            (UV2 . j) = (( upper_bound ( rng (h | ( divset (D,j))))) * ( vol ( divset (D,j)))) by A54, INTEGRA1:def 6;

            

            then

             A59: r = ((( upper_bound ( rng (h | ( divset (D,j))))) * ( vol ( divset (D,j)))) - (( lower_bound ( rng (h | ( divset (D,j))))) * ( vol ( divset (D,j))))) by A52, A55, VALUED_1: 13

            .= ((( upper_bound ( rng (h | ( divset (D,j))))) - ( lower_bound ( rng (h | ( divset (D,j)))))) * ( vol ( divset (D,j))));

            ( vol ( divset (D,j))) >= 0 by INTEGRA1: 9;

            hence thesis by A59, A58;

          end;

          then (osc2 . m) >= 0 by A50, RVSUM_1: 84;

          then

           A60: |.(osc2 . m).| = (osc2 . m) by ABSVALUE:def 1;

          for j be Nat st j in ( Seg ( len D)) holds ((UV2 - LV2) . j) <= ((a * ((UV - LV) + (UV1 - LV1))) . j)

          proof

            let j be Nat;

            set x = ((UV2 - LV2) . j), y = ((a * ((UV - LV) + (UV1 - LV1))) . j);

            

             A61: y = (a * (((UV - LV) + (UV1 - LV1)) . j)) by RVSUM_1: 45

            .= (a * (((UV - LV) . j) + ((UV1 - LV1) . j))) by RVSUM_1: 11

            .= (a * (((UV . j) - (LV . j)) + ((UV1 - LV1) . j))) by RVSUM_1: 27

            .= (a * (((UV . j) - (LV . j)) + ((UV1 . j) - (LV1 . j)))) by RVSUM_1: 27;

            

             A62: ( vol ( divset (D,j))) >= 0 by INTEGRA1: 9;

            assume

             A63: j in ( Seg ( len D));

            then

             A64: j in ( dom D) by FINSEQ_1:def 3;

            then

             A65: (LV2 . j) = (( lower_bound ( rng (h | ( divset (D,j))))) * ( vol ( divset (D,j)))) by INTEGRA1:def 7;

            (UV2 . j) = (( upper_bound ( rng (h | ( divset (D,j))))) * ( vol ( divset (D,j)))) by A64, INTEGRA1:def 6;

            

            then

             A66: x = ((( upper_bound ( rng (h | ( divset (D,j))))) * ( vol ( divset (D,j)))) - (( lower_bound ( rng (h | ( divset (D,j))))) * ( vol ( divset (D,j))))) by A65, RVSUM_1: 27

            .= ((( upper_bound ( rng (h | ( divset (D,j))))) - ( lower_bound ( rng (h | ( divset (D,j)))))) * ( vol ( divset (D,j))));

            

             A67: (LV1 . j) = (( lower_bound ( rng (g | ( divset (D,j))))) * ( vol ( divset (D,j)))) by A64, INTEGRA1:def 7;

            

             A68: (UV1 . j) = (( upper_bound ( rng (g | ( divset (D,j))))) * ( vol ( divset (D,j)))) by A64, INTEGRA1:def 6;

            

             A69: (a * ((( upper_bound ( rng (f | ( divset (D,j))))) - ( lower_bound ( rng (f | ( divset (D,j)))))) + (( upper_bound ( rng (g | ( divset (D,j))))) - ( lower_bound ( rng (g | ( divset (D,j)))))))) >= (( upper_bound ( rng (h | ( divset (D,j))))) - ( lower_bound ( rng (h | ( divset (D,j))))))

            proof

              

               A70: j in ( dom D) by A63, FINSEQ_1:def 3;

              

               A71: ( dom (g | ( divset (D,j)))) = (( dom g) /\ ( divset (D,j))) by RELAT_1: 61

              .= (A /\ ( divset (D,j))) by FUNCT_2:def 1

              .= ( divset (D,j)) by A70, INTEGRA1: 8, XBOOLE_1: 28;

              then

              reconsider g1 = (g | ( divset (D,j))) as PartFunc of ( divset (D,j)), REAL by RELSET_1: 5;

              reconsider g1 as Function of ( divset (D,j)), REAL by A71, FUNCT_2:def 1;

              

               A72: ((g | ( divset (D,j))) | ( divset (D,j))) is bounded_below by A3, A71, INTEGRA2: 6;

              

               A73: ( dom (h | ( divset (D,j)))) = (( dom h) /\ ( divset (D,j))) by RELAT_1: 61

              .= (A /\ ( divset (D,j))) by FUNCT_2:def 1

              .= ( divset (D,j)) by A70, INTEGRA1: 8, XBOOLE_1: 28;

              then

              reconsider h1 = (h | ( divset (D,j))) as PartFunc of ( divset (D,j)), REAL by RELSET_1: 5;

              reconsider h1 as Function of ( divset (D,j)), REAL by A73, FUNCT_2:def 1;

              

               A74: ( dom (f | ( divset (D,j)))) = (( dom f) /\ ( divset (D,j))) by RELAT_1: 61

              .= (A /\ ( divset (D,j))) by FUNCT_2:def 1

              .= ( divset (D,j)) by A70, INTEGRA1: 8, XBOOLE_1: 28;

              then

              reconsider f1 = (f | ( divset (D,j))) as PartFunc of ( divset (D,j)), REAL by RELSET_1: 5;

              

               A75: ((f | ( divset (D,j))) | ( divset (D,j))) is bounded_below by A1, A74, INTEGRA2: 6;

              

               A76: for x, y st x in ( divset (D,j)) & y in ( divset (D,j)) holds |.((h1 . x) - (h1 . y)).| <= (a * ( |.((f1 . x) - (f1 . y)).| + |.((g1 . x) - (g1 . y)).|))

              proof

                let x, y;

                assume that

                 A77: x in ( divset (D,j)) and

                 A78: y in ( divset (D,j));

                

                 A79: (g . y) = (g1 . y) by A71, A78, FUNCT_1: 47;

                

                 A80: (h . y) = (h1 . y) by A73, A78, FUNCT_1: 47;

                

                 A81: (h . x) = (h1 . x) by A73, A77, FUNCT_1: 47;

                

                 A82: (f . y) = (f1 . y) by A74, A78, FUNCT_1: 47;

                

                 A83: (f . x) = (f1 . x) by A74, A77, FUNCT_1: 47;

                (g . x) = (g1 . x) by A71, A77, FUNCT_1: 47;

                hence thesis by A7, A74, A77, A78, A79, A83, A82, A81, A80;

              end;

              ((g | ( divset (D,j))) | ( divset (D,j))) is bounded_above by A3, A71, INTEGRA2: 5;

              then

               A84: (g1 | ( divset (D,j))) is bounded by A72;

              ((f | ( divset (D,j))) | ( divset (D,j))) is bounded_above by A1, A74, INTEGRA2: 5;

              then

               A85: (f1 | ( divset (D,j))) is bounded by A75;

              f1 is total by A74, PARTFUN1:def 2;

              hence thesis by A6, A85, A84, A76, Th26;

            end;

            (LV . j) = (( lower_bound ( rng (f | ( divset (D,j))))) * ( vol ( divset (D,j)))) by A64, INTEGRA1:def 7;

            

            then y = (a * (((( upper_bound ( rng (f | ( divset (D,j))))) * ( vol ( divset (D,j)))) - (( lower_bound ( rng (f | ( divset (D,j))))) * ( vol ( divset (D,j))))) + ((( upper_bound ( rng (g | ( divset (D,j))))) * ( vol ( divset (D,j)))) - (( lower_bound ( rng (g | ( divset (D,j))))) * ( vol ( divset (D,j))))))) by A64, A68, A67, A61, INTEGRA1:def 6

            .= ((a * ((( upper_bound ( rng (f | ( divset (D,j))))) - ( lower_bound ( rng (f | ( divset (D,j)))))) + (( upper_bound ( rng (g | ( divset (D,j))))) - ( lower_bound ( rng (g | ( divset (D,j)))))))) * ( vol ( divset (D,j))));

            hence thesis by A66, A69, A62, XREAL_1: 64;

          end;

          then (osc2 . m) <= ( Sum (a * ((UV - LV) + (UV1 - LV1)))) by A50, RVSUM_1: 82;

          then (osc2 . m) <= (a * ( Sum ((UV - LV) + (UV1 - LV1)))) by RVSUM_1: 87;

          then (osc2 . m) <= (a * ((osc . m) + (osc1 . m))) by A24, A25, RVSUM_1: 89;

          hence thesis by A60, A49, XXREAL_0: 2;

        end;

        then osc2 is convergent by SEQ_2:def 6;

        then

         A86: ( lim (( upper_sum (h,T)) - ( lower_sum (h,T)))) = 0 by A18, SEQ_2:def 7;

        

         A87: ( lower_sum (h,T)) is convergent by A5, A8, A9, Th8;

        ( upper_sum (h,T)) is convergent by A5, A8, A9, Th9;

        hence thesis by A87, A86, SEQ_2: 12;

      end;

      hence thesis by A5, Th12;

    end;

    theorem :: INTEGRA4:29

    for f,g be Function of A, REAL st (f | A) is bounded & f is integrable & (g | A) is bounded & g is integrable holds (f (#) g) is integrable

    proof

      let f,g be Function of A, REAL ;

      assume that

       A1: (f | A) is bounded and

       A2: f is integrable and

       A3: (g | A) is bounded and

       A4: g is integrable;

      

       A5: ((f (#) g) | (A /\ A)) is bounded by A1, A3, RFUNCT_1: 84;

      consider r2 be Real such that

       A6: for x be object st x in (A /\ ( dom g)) holds |.(g . x).| <= r2 by A3, RFUNCT_1: 73;

      

       A7: (A /\ ( dom g)) = (A /\ A) by FUNCT_2:def 1

      .= A;

      

       A8: (A /\ ( dom f)) = (A /\ A) by FUNCT_2:def 1

      .= A;

      then

      consider a be Element of REAL such that

       A9: a in (A /\ ( dom f)) by SUBSET_1: 4;

      reconsider a as Element of A by A9;

      

       A10: |.(f . a).| >= 0 by COMPLEX1: 46;

      consider r1 be Real such that

       A11: for x be object st x in (A /\ ( dom f)) holds |.(f . x).| <= r1 by A1, RFUNCT_1: 73;

      reconsider r = ( max (r1,r2)) as Real;

      

       A12: r2 <= r by XXREAL_0: 25;

      

       A13: r1 <= r by XXREAL_0: 25;

      

       A14: for x, y st x in A & y in A holds |.(((f (#) g) . x) - ((f (#) g) . y)).| <= (r * ( |.((g . x) - (g . y)).| + |.((f . x) - (f . y)).|))

      proof

        let x, y;

        assume that

         A15: x in A and

         A16: y in A;

        

         A17: ((f (#) g) . y) = ((f . y) * (g . y)) by VALUED_1: 5;

         |.(g . y).| <= r2 by A6, A7, A16;

        then

         A18: |.(g . y).| <= r by A12, XXREAL_0: 2;

        

         A19: |.((f . x) - (f . y)).| >= 0 by COMPLEX1: 46;

         |.(((f . x) - (f . y)) * (g . y)).| = ( |.((f . x) - (f . y)).| * |.(g . y).|) by COMPLEX1: 65;

        then

         A20: |.(((f . x) - (f . y)) * (g . y)).| <= (r * |.((f . x) - (f . y)).|) by A19, A18, XREAL_1: 64;

        ((f (#) g) . x) = ((f . x) * (g . x)) by VALUED_1: 5;

        then |.(((f (#) g) . x) - ((f (#) g) . y)).| = |.(((f . x) * ((g . x) - (g . y))) + (((f . x) - (f . y)) * (g . y))).| by A17;

        then

         A21: |.(((f (#) g) . x) - ((f (#) g) . y)).| <= ( |.((f . x) * ((g . x) - (g . y))).| + |.(((f . x) - (f . y)) * (g . y)).|) by COMPLEX1: 56;

         |.(f . x).| <= r1 by A11, A8, A15;

        then

         A22: |.(f . x).| <= r by A13, XXREAL_0: 2;

        

         A23: |.((g . x) - (g . y)).| >= 0 by COMPLEX1: 46;

         |.((f . x) * ((g . x) - (g . y))).| = ( |.(f . x).| * |.((g . x) - (g . y)).|) by COMPLEX1: 65;

        then |.((f . x) * ((g . x) - (g . y))).| <= (r * |.((g . x) - (g . y)).|) by A23, A22, XREAL_1: 64;

        then ( |.((f . x) * ((g . x) - (g . y))).| + |.(((f . x) - (f . y)) * (g . y)).|) <= ((r * |.((g . x) - (g . y)).|) + (r * |.((f . x) - (f . y)).|)) by A20, XREAL_1: 7;

        hence thesis by A21, XXREAL_0: 2;

      end;

      

       A24: |.(f . a).| <= r1 by A11, A9;

      now

        per cases by A24, A10, XXREAL_0: 25;

          suppose

           A25: r = 0 ;

          for x, y st x in A & y in A holds |.(((f (#) g) . x) - ((f (#) g) . y)).| <= (1 * |.((f . x) - (f . y)).|)

          proof

            let x, y;

            assume that

             A26: x in A and

             A27: y in A;

             |.(((f (#) g) . x) - ((f (#) g) . y)).| <= (r * ( |.((g . x) - (g . y)).| + |.((f . x) - (f . y)).|)) by A14, A26, A27;

            hence thesis by A25, COMPLEX1: 46;

          end;

          hence thesis by A1, A2, A5, Th27;

        end;

          suppose r > 0 ;

          hence thesis by A1, A2, A3, A4, A5, A14, Th28;

        end;

      end;

      hence thesis;

    end;

    theorem :: INTEGRA4:30

    for f be Function of A, REAL st (f | A) is bounded & f is integrable & not 0 in ( rng f) & ((f ^ ) | A) is bounded holds (f ^ ) is integrable

    proof

      let f be Function of A, REAL ;

      assume that

       A1: (f | A) is bounded and

       A2: f is integrable and

       A3: not 0 in ( rng f) and

       A4: ((f ^ ) | A) is bounded;

      consider r be Real such that

       A5: for x be object st x in (A /\ ( dom (f ^ ))) holds |.((f ^ ) . x).| <= r by A4, RFUNCT_1: 73;

      reconsider r as Real;

      (f " { 0 }) = {} by A3, FUNCT_1: 72;

      then

       A6: (f ^ ) is total by RFUNCT_1: 54;

      

       A7: for x, y st x in A & y in A holds |.(((f ^ ) . x) - ((f ^ ) . y)).| <= ((r ^2 ) * |.((f . x) - (f . y)).|)

      proof

        let x, y;

        assume that

         A8: x in A and

         A9: y in A;

        

         A10: x in ( dom (f ^ )) by A6, A8, PARTFUN1:def 2;

        then

         A11: (f . x) <> 0 by RFUNCT_1: 3;

        

         A12: y in ( dom (f ^ )) by A6, A9, PARTFUN1:def 2;

        then

         A13: (f . y) <> 0 by RFUNCT_1: 3;

         0 <= (1 / |.(f . x).|) & 0 <= (1 / |.(f . y).|) & (1 / |.(f . x).|) <= r & (1 / |.(f . y).|) <= r

        proof

          

           A14: |.(f . y).| > 0 by A13, COMPLEX1: 47;

           |.(f . x).| > 0 by A11, COMPLEX1: 47;

          hence 0 <= (1 / |.(f . x).|) & 0 <= (1 / |.(f . y).|) by A14;

          reconsider x, y as Element of A by A8, A9;

          y in (A /\ ( dom (f ^ ))) by A12, XBOOLE_0:def 4;

          then |.((f ^ ) . y).| <= r by A5;

          then |.(1 * ((f . y) " )).| <= r by A12, RFUNCT_1:def 2;

          then

           A15: |.(1 / (f . y)).| <= r by XCMPLX_0:def 9;

          x in (A /\ ( dom (f ^ ))) by A10, XBOOLE_0:def 4;

          then |.((f ^ ) . x).| <= r by A5;

          then |.(1 * ((f . x) " )).| <= r by A10, RFUNCT_1:def 2;

          then |.(1 / (f . x)).| <= r by XCMPLX_0:def 9;

          hence thesis by A15, ABSVALUE: 7;

        end;

        then

         A16: ((1 / |.(f . x).|) * (1 / |.(f . y).|)) <= (r * r) by XREAL_1: 66;

         |.((f . x) - (f . y)).| >= 0 by COMPLEX1: 46;

        then

         A17: ( |.((f . x) - (f . y)).| * ((1 / |.(f . x).|) * (1 / |.(f . y).|))) <= ( |.((f . x) - (f . y)).| * (r ^2 )) by A16, XREAL_1: 64;

        (((f ^ ) . x) - ((f ^ ) . y)) = (((f . x) " ) - ((f ^ ) . y)) by A10, RFUNCT_1:def 2

        .= (((f . x) " ) - ((f . y) " )) by A12, RFUNCT_1:def 2;

        

        then |.(((f ^ ) . x) - ((f ^ ) . y)).| = ( |.((f . x) - (f . y)).| / ( |.(f . x).| * |.(f . y).|)) by A13, A11, SEQ_2: 2

        .= (( |.((f . x) - (f . y)).| / |.(f . x).|) * (1 / |.(f . y).|)) by XCMPLX_1: 103

        .= (( |.((f . x) - (f . y)).| * (1 / |.(f . x).|)) * (1 / |.(f . y).|)) by XCMPLX_1: 99;

        hence thesis by A17;

      end;

      per cases by XREAL_1: 63;

        suppose

         A18: (r ^2 ) = 0 ;

        for x, y st x in A & y in A holds |.(((f ^ ) . x) - ((f ^ ) . y)).| <= (1 * |.((f . x) - (f . y)).|)

        proof

          let x, y;

          assume that

           A19: x in A and

           A20: y in A;

           |.(((f ^ ) . x) - ((f ^ ) . y)).| <= ( 0 * |.((f . x) - (f . y)).|) by A7, A18, A19, A20;

          hence thesis by COMPLEX1: 46;

        end;

        hence thesis by A1, A2, A4, A6, Th27;

      end;

        suppose (r ^2 ) > 0 ;

        hence thesis by A1, A2, A4, A6, A7, Th27;

      end;

    end;