integra6.miz



    begin

    reserve a,b,c,d,e,x,r for Real,

A for non empty closed_interval Subset of REAL ,

f,g for PartFunc of REAL , REAL ;

    theorem :: INTEGRA6:1

    

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

    proof

      assume that

       A1: a <= b & c <= d and

       A2: (a + c) = (b + d);

      assume not (a = b & c = d);

      then a < b or c < d by A1, XXREAL_0: 1;

      hence contradiction by A1, A2, XREAL_1: 8;

    end;

    theorem :: INTEGRA6:2

    

     Th2: a <= b implies ].(x - a), (x + a).[ c= ].(x - b), (x + b).[

    proof

      assume a <= b;

      then (x - b) <= (x - a) & (x + a) <= (x + b) by XREAL_1: 7, XREAL_1: 10;

      hence thesis by XXREAL_1: 46;

    end;

    theorem :: INTEGRA6:3

    

     Th3: for R be Relation, A,B,C be set st A c= B & A c= C holds ((R | B) | A) = ((R | C) | A)

    proof

      let R be Relation, A,B,C be set;

      assume that

       A1: A c= B and

       A2: A c= C;

      ((R | C) | A) = (R | A) by A2, RELAT_1: 74;

      hence thesis by A1, RELAT_1: 74;

    end;

    theorem :: INTEGRA6:4

    

     Th4: for A,B,C be set st A c= B & A c= C holds (( chi (B,B)) | A) = (( chi (C,C)) | A)

    proof

      let A,B,C be set;

      assume that

       A1: A c= B and

       A2: A c= C;

       A3:

      now

        

         A4: ( dom (( chi (C,C)) | A)) = (( dom ( chi (C,C))) /\ A) by RELAT_1: 61;

        assume

         A5: A is non empty;

        then C is non empty by A2, XBOOLE_1: 58, XBOOLE_1: 61;

        then ( dom (( chi (C,C)) | A)) = (C /\ A) by A4, RFUNCT_1: 61;

        then

         A6: ( dom (( chi (C,C)) | A)) = A by A2, XBOOLE_1: 28;

        

         A7: ( dom (( chi (B,B)) | A)) = (( dom ( chi (B,B))) /\ A) by RELAT_1: 61;

        B is non empty by A1, A5, XBOOLE_1: 58, XBOOLE_1: 61;

        then ( dom (( chi (B,B)) | A)) = (B /\ A) by A7, RFUNCT_1: 61;

        then

         A8: ( dom (( chi (B,B)) | A)) = A by A1, XBOOLE_1: 28;

        now

          let x be object;

          assume

           A9: x in A;

          then ((( chi (B,B)) | A) . x) = (( chi (B,B)) . x) by A8, FUNCT_1: 47;

          then ((( chi (B,B)) | A) . x) = 1 by A1, A9, RFUNCT_1: 61;

          then ((( chi (B,B)) | A) . x) = (( chi (C,C)) . x) by A2, A9, RFUNCT_1: 61;

          hence ((( chi (B,B)) | A) . x) = ((( chi (C,C)) | A) . x) by A6, A9, FUNCT_1: 47;

        end;

        hence thesis by A8, A6, FUNCT_1: 2;

      end;

      now

        assume

         A10: A is empty;

        then (( chi (B,B)) | A) = {} ;

        hence thesis by A10;

      end;

      hence thesis by A3;

    end;

    theorem :: INTEGRA6:5

    

     Th5: a <= b implies ( vol ['a, b']) = (b - a)

    proof

      assume a <= b;

      then

       A1: ['a, b'] = [.a, b.] by INTEGRA5:def 3;

      then

       A2: [.a, b.] = [.( lower_bound [.a, b.]), ( upper_bound [.a, b.]).] by INTEGRA1: 4;

      then a = ( lower_bound [.a, b.]) by A1, INTEGRA1: 5;

      hence thesis by A1, A2, INTEGRA1: 5;

    end;

    theorem :: INTEGRA6:6

    

     Th6: ( vol ['( min (a,b)), ( max (a,b))']) = |.(b - a).|

    proof

      per cases ;

        suppose

         A1: a <= b;

        then ( min (a,b)) = a & ( max (a,b)) = b by XXREAL_0:def 9, XXREAL_0:def 10;

        then

         A2: ( vol ['( min (a,b)), ( max (a,b))']) = (b - a) by Th5, XXREAL_0: 25;

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

        hence thesis by A2, ABSVALUE:def 1;

      end;

        suppose

         A3: not a <= b;

        then 0 <= (a - b) by XREAL_1: 48;

        

        then

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

        .= |.(b - a).| by COMPLEX1: 60;

        ( min (a,b)) = b & ( max (a,b)) = a by A3, XXREAL_0:def 9, XXREAL_0:def 10;

        hence thesis by A4, Th5, XXREAL_0: 17;

      end;

    end;

    begin

    

     Lm1: A c= ( dom f) implies (f || A) is Function of A, REAL

    proof

      ( rng f) c= REAL ;

      then

       A1: f is Function of ( dom f), REAL by FUNCT_2: 2;

      assume A c= ( dom f);

      hence thesis by A1, FUNCT_2: 32;

    end;

    theorem :: INTEGRA6:7

    

     Th7: A c= ( dom f) & f is_integrable_on A & (f | A) is bounded implies ( abs f) is_integrable_on A & |.( integral (f,A)).| <= ( integral (( abs f),A))

    proof

      

       A1: |.(f || A).| = (( abs f) || A) by RFUNCT_1: 46;

      assume A c= ( dom f);

      then

       A2: (f || A) is Function of A, REAL by Lm1;

      assume f is_integrable_on A & (f | A) is bounded;

      then

       A3: (f || A) is integrable & ((f || A) | A) is bounded;

      thus thesis by A3, A2, A1, INTEGRA4: 23;

    end;

    theorem :: INTEGRA6:8

    

     Th8: a <= b & ['a, b'] c= ( dom f) & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded implies |.( integral (f,a,b)).| <= ( integral (( abs f),a,b))

    proof

      assume a <= b;

      then ( integral (f,a,b)) = ( integral (f, ['a, b'])) & ( integral (( abs f),a,b)) = ( integral (( abs f), ['a, b'])) by INTEGRA5:def 4;

      hence thesis by Th7;

    end;

    theorem :: INTEGRA6:9

    

     Th9: A c= ( dom f) & f is_integrable_on A & (f | A) is bounded implies (r (#) f) is_integrable_on A & ( integral ((r (#) f),A)) = (r * ( integral (f,A)))

    proof

      assume that

       A1: A c= ( dom f) and

       A2: f is_integrable_on A & (f | A) is bounded;

      

       A3: (f || A) is integrable & ((f || A) | A) is bounded by A2;

      ( rng f) c= REAL ;

      then f is Function of ( dom f), REAL by FUNCT_2: 2;

      then

       A4: (f | A) is Function of A, REAL by A1, FUNCT_2: 32;

      (r (#) (f || A)) = ((r (#) f) | A) by RFUNCT_1: 49;

      then ((r (#) f) || A) is integrable by A3, A4, INTEGRA2: 31;

      hence (r (#) f) is_integrable_on A;

      ( integral ((r (#) f),A)) = ( integral (r (#) (f || A))) by RFUNCT_1: 49;

      hence thesis by A3, A4, INTEGRA2: 31;

    end;

    theorem :: INTEGRA6:10

    

     Th10: a <= b & ['a, b'] c= ( dom f) & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded implies ( integral ((c (#) f),a,b)) = (c * ( integral (f,a,b)))

    proof

      assume that

       A1: a <= b and

       A2: ['a, b'] c= ( dom f) & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded;

      ( integral (f,a,b)) = ( integral (f, ['a, b'])) & ( integral ((c (#) f),a,b)) = ( integral ((c (#) f), ['a, b'])) by A1, INTEGRA5:def 4;

      hence thesis by A2, Th9;

    end;

    theorem :: INTEGRA6:11

    

     Th11: A c= ( dom f) & A c= ( dom g) & f is_integrable_on A & (f | A) is bounded & g is_integrable_on A & (g | A) is bounded implies (f + g) is_integrable_on A & (f - g) is_integrable_on A & ( integral ((f + g),A)) = (( integral (f,A)) + ( integral (g,A))) & ( integral ((f - g),A)) = (( integral (f,A)) - ( integral (g,A)))

    proof

      assume that

       A1: A c= ( dom f) & A c= ( dom g) and

       A2: f is_integrable_on A and

       A3: (f | A) is bounded and

       A4: g is_integrable_on A and

       A5: (g | A) is bounded;

      

       A6: ((f || A) | A) is bounded & ((g || A) | A) is bounded by A3, A5;

      

       A7: (f || A) is Function of A, REAL & (g || A) is Function of A, REAL by A1, Lm1;

      

       A8: ((f || A) + (g || A)) = ((f + g) || A) & ((f || A) - (g || A)) = ((f - g) || A) by RFUNCT_1: 44, RFUNCT_1: 47;

      

       A9: (f || A) is integrable & (g || A) is integrable by A2, A4;

      then ((f || A) + (g || A)) is integrable & ((f || A) - (g || A)) is integrable by A6, A7, INTEGRA1: 57, INTEGRA2: 33;

      hence (f + g) is_integrable_on A & (f - g) is_integrable_on A by A8;

      thus thesis by A9, A6, A7, A8, INTEGRA1: 57, INTEGRA2: 33;

    end;

    theorem :: INTEGRA6:12

    

     Th12: a <= b & ['a, b'] c= ( dom f) & ['a, b'] c= ( dom g) & f is_integrable_on ['a, b'] & g is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & (g | ['a, b']) is bounded implies ( integral ((f + g),a,b)) = (( integral (f,a,b)) + ( integral (g,a,b))) & ( integral ((f - g),a,b)) = (( integral (f,a,b)) - ( integral (g,a,b)))

    proof

      assume that

       A1: a <= b and

       A2: ['a, b'] c= ( dom f) & ['a, b'] c= ( dom g) & f is_integrable_on ['a, b'] & g is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & (g | ['a, b']) is bounded;

      

       A3: ( integral ((f + g),a,b)) = ( integral ((f + g), ['a, b'])) & ( integral ((f - g),a,b)) = ( integral ((f - g), ['a, b'])) by A1, INTEGRA5:def 4;

      ( integral (f,a,b)) = ( integral (f, ['a, b'])) & ( integral (g,a,b)) = ( integral (g, ['a, b'])) by A1, INTEGRA5:def 4;

      hence thesis by A2, A3, Th11;

    end;

    theorem :: INTEGRA6:13

    (f | A) is bounded & (g | A) is bounded implies ((f (#) g) | A) is bounded

    proof

      assume (f | A) is bounded & (g | A) is bounded;

      then ((f (#) g) | (A /\ A)) is bounded by RFUNCT_1: 84;

      hence thesis;

    end;

    theorem :: INTEGRA6:14

    A c= ( dom f) & A c= ( dom g) & f is_integrable_on A & (f | A) is bounded & g is_integrable_on A & (g | A) is bounded implies (f (#) g) is_integrable_on A

    proof

      assume that

       A1: A c= ( dom f) & A c= ( dom g) and

       A2: f is_integrable_on A & (f | A) is bounded and

       A3: g is_integrable_on A & (g | A) is bounded;

      

       A4: (f || A) is integrable & ((f || A) | A) is bounded by A2;

      

       A5: (g || A) is integrable & ((g || A) | A) is bounded by A3;

      

       A6: ((f || A) (#) (g || A)) = ((f (#) g) || A) by INTEGRA5: 4;

      (f || A) is Function of A, REAL & (g || A) is Function of A, REAL by A1, Lm1;

      then ((f (#) g) || A) is integrable by A4, A5, A6, INTEGRA4: 29;

      hence thesis;

    end;

    theorem :: INTEGRA6:15

    

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

    proof

      let n be Nat;

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

        assume x1 in ( rng D);

        then

        consider i be Element of NAT such that

         A10: i in ( dom D) and

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

        

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

        i <= ( len D) by A10, 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

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

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

        x1 = F(i) by A3, A10, A11;

        hence thesis by A14, A13, INTEGRA2: 1;

      end;

      then ( rng D) c= A;

      then

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

      take D;

      thus ( len D) = n by A3;

      let i be Nat;

      assume i in ( dom D);

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

      hence thesis;

    end;

    begin

    theorem :: INTEGRA6:16

    

     Th16: ( vol A) > 0 implies ex T be DivSequence of A st ( delta T) is convergent & ( lim ( delta T)) = 0 & for n be Element of NAT holds ex Tn be Division of A st Tn divide_into_equal (n + 1) & (T . n) = Tn

    proof

      defpred P[ set, set] means ex n be Element of 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) & for i be Nat st i in ( dom D) holds (D . i) = (( lower_bound A) + ((( vol A) / (n + 1)) * i)) by A1, Th15;

        reconsider D1 = D as Element of ( divs A) by INTEGRA1:def 3;

        take D1;

        D divide_into_equal (n + 1) by A3, INTEGRA4:def 1;

        hence thesis;

      end;

      consider T be sequence of ( divs A) such that

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

      reconsider T as DivSequence of A;

      

       A5: for n be Element of NAT holds ex Tn be Division of A st Tn divide_into_equal (n + 1) & (T . n) = Tn

      proof

        let n be Element of NAT ;

        ex n1 be Element of NAT , Tn be Division of A st n1 = n & Tn = (T . n) & Tn divide_into_equal (n1 + 1) by A4;

        hence thesis;

      end;

      

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

      proof

        let i be Element of NAT ;

        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

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

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

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

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

          then

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

          

           A10: ex n be Element of NAT , e be Division of A st n = i & e = D & e divide_into_equal (n + 1) by A4;

          

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

          proof

             A12:

            now

              

               A13: ( len D) = (i + 1) by A10, INTEGRA4:def 1;

              assume

               A14: k = 1;

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

              then ( upper_bound ( divset (D,k))) = (( lower_bound A) + ((( vol A) / (i + 1)) * 1)) by A10, A9, A14, A13, INTEGRA4:def 1;

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

              hence thesis;

            end;

            now

              assume

               A15: k <> 1;

              then (k - 1) in ( dom D) by A9, INTEGRA1: 7;

              then

               A16: (D . (k - 1)) = (( lower_bound A) + ((( vol A) / ( len D)) * (k - 1))) by A10, INTEGRA4:def 1;

              

               A17: (D . k) = (( lower_bound A) + ((( vol A) / ( len D)) * k)) by A10, A9, INTEGRA4:def 1;

              ( lower_bound ( divset (D,k))) = (D . (k - 1)) & ( upper_bound ( divset (D,k))) = (D . k) by A9, A15, INTEGRA1:def 4;

              hence thesis by A10, A16, A17, INTEGRA4:def 1;

            end;

            hence thesis by A12;

          end;

          x1 = ( vol ( divset (D,k))) by A8, A9, INTEGRA1: 20;

          hence thesis by A11, TARSKI:def 1;

        end;

        then

         A18: ( rng ( upper_volume (( chi (A,A)),(T . i)))) c= {(( vol A) / (i + 1))};

        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;

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

          then

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

          

           A20: ex n be Element of NAT , e be Division of A st n = i & e = D & e divide_into_equal (n + 1) by A4;

          ( rng D) <> {} ;

          then

           A21: 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 A21, A20, INTEGRA4:def 1;

          then

           A22: ( vol ( divset (D,1))) = ((( lower_bound A) + (( vol A) / ( len D))) - ( lower_bound A)) by A21, INTEGRA1:def 4;

          1 in ( Seg ( len D)) by A21, 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

           A23: (( 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 A21, INTEGRA1: 20;

          hence thesis by A19, A23, A20, A22, INTEGRA4:def 1;

        end;

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

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

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

        hence thesis by TARSKI:def 1;

      end;

      

       A24: for a be Real st 0 < a holds ex i be Element of NAT st |.((( delta T) . i) - 0 ).| < a

      proof

        let a be Real;

        

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

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

        assume

         A26: 0 < a;

        then ( [\(( vol A) / a)/] + 1) > 0 by A25, 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

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

        

         A28: (( delta T) . i1) = (( vol A) / (i1 + 1)) by A6;

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

        hence thesis by A27, A28;

      end;

      

       A29: for i,j be Element of NAT st i <= j holds (( delta T) . i) >= (( delta T) . j)

      proof

        let i,j be Element of NAT ;

        assume i <= j;

        then

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

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

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

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

        hence thesis by A6;

      end;

      

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

         A32: 0 < a;

        consider i be Element of NAT such that

         A33: |.((( delta T) . i) - 0 ).| < a by A24, A32;

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

        then (( delta T) . i) >= 0 by INTEGRA3: 9;

        then

         A34: (( delta T) . i) < a by A33, ABSVALUE:def 1;

        take i;

        let j be Nat;

        reconsider jj = j as Element of NAT by ORDINAL1:def 12;

        assume i <= j;

        then (( delta T) . jj) <= (( delta T) . i) by A29;

        then

         A35: (( delta T) . j) < a by A34, XXREAL_0: 2;

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

        then (( delta T) . j) >= 0 by INTEGRA3: 9;

        hence |.((( delta T) . j) - 0 ).| < a by A35, ABSVALUE:def 1;

      end;

      then

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

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

      hence thesis by A5, A36;

    end;

    

     Lm2: a <= b & ['a, b'] c= ( dom f) & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & c in ['a, b'] & b <> c implies ( integral (f,a,b)) = (( integral (f,a,c)) + ( integral (f,c,b))) & f is_integrable_on ['a, c'] & f is_integrable_on ['c, b']

    proof

      assume that

       A1: a <= b and

       A2: ['a, b'] c= ( dom f) and

       A3: f is_integrable_on ['a, b'] and

       A4: (f | ['a, b']) is bounded and

       A5: c in ['a, b'] and

       A6: b <> c;

      

       A7: ['a, b'] = [.a, b.] by A1, INTEGRA5:def 3;

      then

       A8: c <= b by A5, XXREAL_1: 1;

      then

       A9: ['c, b'] = [.c, b.] by INTEGRA5:def 3;

      then

       A10: [.c, b.] = [.( lower_bound [.c, b.]), ( upper_bound [.c, b.]).] by INTEGRA1: 4;

      then

       A11: ( upper_bound ['c, b']) = b by A9, INTEGRA1: 5;

      set FAB = (f || ['a, b']), FAC = (f || ['a, c']), FCB = (f || ['c, b']);

      

       A12: FAB is Function of ['a, b'], REAL by A2, Lm1;

      

       A13: a <= c by A5, A7, XXREAL_1: 1;

      then

       A14: ['a, c'] = [.a, c.] by INTEGRA5:def 3;

      then

       A15: [.a, c.] = [.( lower_bound [.a, c.]), ( upper_bound [.a, c.]).] by INTEGRA1: 4;

      then

       A16: ( lower_bound ['a, c']) = a by A14, INTEGRA1: 5;

      

       A17: ['c, b'] c= ['a, b'] by A7, A13, A9, XXREAL_1: 34;

      then (f | ['c, b']) is bounded by A4, RFUNCT_1: 74;

      then

       A18: (FCB | ['c, b']) is bounded;

      

       A19: ( lower_bound ['c, b']) = c by A9, A10, INTEGRA1: 5;

      ex PS2 be DivSequence of ['c, b'] st ( delta PS2) is convergent & ( lim ( delta PS2)) = 0 & ex K be Element of NAT st for i be Element of NAT st K <= i holds ex S2i be Division of ['c, b'] st S2i = (PS2 . i) & 2 <= ( len S2i)

      proof

        c < b by A6, A8, XXREAL_0: 1;

        then ( vol ['c, b']) > 0 by A19, A11, XREAL_1: 50;

        then

        consider T be DivSequence of ['c, b'] such that

         A20: ( delta T) is convergent & ( lim ( delta T)) = 0 and

         A21: for n be Element of NAT holds ex Tn be Division of ['c, b'] st Tn divide_into_equal (n + 1) & (T . n) = Tn by Th16;

        take T;

        now

          let i be Element of NAT ;

          assume

           A22: 2 <= i;

          consider Tn be Division of ['c, b'] such that

           A23: Tn divide_into_equal (i + 1) and

           A24: (T . i) = Tn by A21;

          reconsider Tn as Division of ['c, b'];

          take Tn;

          thus Tn = (T . i) by A24;

          ( len Tn) = (i + 1) by A23, INTEGRA4:def 1;

          then i <= ( len Tn) by NAT_1: 11;

          hence 2 <= ( len Tn) by A22, XXREAL_0: 2;

        end;

        hence thesis by A20;

      end;

      then

      consider PS2 be DivSequence of ['c, b'] such that

       A25: ( delta PS2) is convergent & ( lim ( delta PS2)) = 0 and

       A26: ex K be Element of NAT st for i be Element of NAT st K <= i holds ex S2i be Division of ['c, b'] st S2i = (PS2 . i) & 2 <= ( len S2i);

      consider K be Element of NAT such that

       A27: for i be Element of NAT st K <= i holds ex S2i be Division of ['c, b'] st S2i = (PS2 . i) & 2 <= ( len S2i) by A26;

      defpred Q[ set, set] means ex n be Element of NAT , e be Division of ['c, b'] st n = $1 & e = $2 & e = (PS2 . (n + K));

      

       A28: for n be Element of NAT holds ex D be Element of ( divs ['c, b']) st Q[n, D]

      proof

        let n be Element of NAT ;

        reconsider D = (PS2 . (n + K)) as Element of ( divs ['c, b']) by INTEGRA1:def 3;

        take D;

        thus thesis;

      end;

      consider S2 be sequence of ( divs ['c, b']) such that

       A29: for n be Element of NAT holds Q[n, (S2 . n)] from FUNCT_2:sch 3( A28);

      reconsider S2 as DivSequence of ['c, b'];

      defpred P1[ Element of NAT , set] means ex S be Division of ['c, b'] st S = (S2 . $1) & $2 = (S /^ 1);

       A30:

      now

        let i be Element of NAT ;

        ex n be Element of NAT , e be Division of ['c, b'] st n = i & e = (S2 . i) & e = (PS2 . (n + K)) by A29;

        hence ex S2i be Division of ['c, b'] st S2i = (S2 . i) & 2 <= ( len S2i) by A27, NAT_1: 11;

      end;

      

       A31: for i be Element of NAT holds ex T be Element of ( divs ['c, b']) st P1[i, T]

      proof

        let i be Element of NAT ;

        consider S be Division of ['c, b'] such that

         A32: S = (S2 . i) and

         A33: 2 <= ( len S) by A30;

        set T = (S /^ 1);

        

         A34: 1 <= ( len S) by A33, XXREAL_0: 2;

        (2 - 1) <= (( len S) - 1) by A33, XREAL_1: 13;

        then

         A35: 1 <= ( len T) by A34, RFINSEQ:def 1;

        then ( len T) in ( Seg ( len T));

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

        then (T . ( len T)) = (S . (( len T) + 1)) by A34, RFINSEQ:def 1;

        then (T . ( len T)) = (S . ((( len S) - 1) + 1)) by A34, RFINSEQ:def 1;

        then

         A36: (T . ( len T)) = ( upper_bound ['c, b']) by INTEGRA1:def 2;

        ( rng S) c= ['c, b'] & ( rng T) c= ( rng S) by FINSEQ_5: 33, INTEGRA1:def 2;

        then

         A37: ( rng T) c= ['c, b'];

        T is non empty increasing by A33, A35, INTEGRA1: 34, XXREAL_0: 2;

        then T is Division of ['c, b'] by A37, A36, INTEGRA1:def 2;

        then T is Element of ( divs ['c, b']) by INTEGRA1:def 3;

        hence thesis by A32;

      end;

      consider T2 be DivSequence of ['c, b'] such that

       A38: for i be Element of NAT holds P1[i, (T2 . i)] from FUNCT_2:sch 3( A31);

      

       A39: for n be Element of NAT holds ex D be Division of ['c, b'] st D = (T2 . n) & for i be Element of NAT st i in ( dom D) holds c < (D . i)

      proof

        let n be Element of NAT ;

        reconsider D = (T2 . n) as Division of ['c, b'];

        take D;

        consider E be Division of ['c, b'] such that

         A40: E = (S2 . n) and

         A41: (T2 . n) = (E /^ 1) by A38;

        

         A42: ex E1 be Division of ['c, b'] st E1 = (S2 . n) & 2 <= ( len E1) by A30;

        then

         A43: (2 - 1) <= (( len E) - 1) by A40, XREAL_1: 13;

        

         A44: 1 <= ( len E) by A40, A42, XXREAL_0: 2;

        then 1 in ( Seg ( len E));

        then

         A45: 1 in ( dom E) by FINSEQ_1:def 3;

        then ( rng E) c= ['c, b'] & (E . 1) in ( rng E) by FUNCT_1:def 3, INTEGRA1:def 2;

        then

         A46: c <= (E . 1) by A9, XXREAL_1: 1;

        2 in ( Seg ( len E)) by A40, A42;

        then 2 in ( dom E) by FINSEQ_1:def 3;

        then

         A47: (E . 1) < (E . 2) by A45, SEQM_3:def 1;

        ( len D) = (( len E) - 1) by A41, A44, RFINSEQ:def 1;

        then 1 in ( Seg ( len D)) by A43;

        then

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

        then

         A49: (D . 1) = (E . (1 + 1)) by A41, A44, RFINSEQ:def 1;

        then

         A50: c < (D . 1) by A46, A47, XXREAL_0: 2;

        now

          let i be Element of NAT ;

          assume

           A51: i in ( dom D);

          then

           A52: 1 <= i by FINSEQ_3: 25;

          now

            assume i <> 1;

            then 1 < i by A52, XXREAL_0: 1;

            then (D . 1) < (D . i) by A48, A51, SEQM_3:def 1;

            hence c < (D . i) by A50, XXREAL_0: 2;

          end;

          hence c < (D . i) by A49, A46, A47, XXREAL_0: 2;

        end;

        hence thesis;

      end;

      set XAC = ( chi ( ['a, c'], ['a, c']));

      set XCB = ( chi ( ['c, b'], ['c, b']));

      consider T1 be DivSequence of ['a, c'] such that

       A53: ( delta T1) is convergent & ( lim ( delta T1)) = 0 by INTEGRA4: 11;

      

       A54: for n be Element of NAT holds ex D be Division of ['c, b'] st D = (T2 . n) & 1 <= ( len D)

      proof

        let n be Element of NAT ;

        reconsider D = (T2 . n) as Division of ['c, b'];

        take D;

        consider E be Division of ['c, b'] such that

         A55: E = (S2 . n) and

         A56: (T2 . n) = (E /^ 1) by A38;

        ex E1 be Division of ['c, b'] st E1 = (S2 . n) & 2 <= ( len E1) by A30;

        then 1 <= ( len E) & (2 - 1) <= (( len E) - 1) by A55, XREAL_1: 13, XXREAL_0: 2;

        hence thesis by A56, RFINSEQ:def 1;

      end;

      

       A57: ( integral (f,c,b)) = ( integral (f, ['c, b'])) by A8, INTEGRA5:def 4

      .= ( integral FCB);

      

       A58: ( integral (f,a,c)) = ( integral (f, ['a, c'])) by A13, INTEGRA5:def 4;

      defpred P2[ Element of NAT , set] means ex S1 be Division of ['a, c'], S2 be Division of ['c, b'] st S1 = (T1 . $1) & S2 = (T2 . $1) & $2 = (S1 ^ S2);

      

       A59: [.a, b.] = [.( lower_bound [.a, b.]), ( upper_bound [.a, b.]).] by A7, INTEGRA1: 4;

      then

       A60: ( upper_bound ['a, b']) = b by A7, INTEGRA1: 5;

      

       A61: for i be Element of NAT holds ex T be Element of ( divs ['a, b']) st P2[i, T]

      proof

        let i0 be Element of NAT ;

        reconsider S1 = (T1 . i0) as Division of ['a, c'];

        reconsider S2 = (T2 . i0) as Division of ['c, b'];

        set T = (S1 ^ S2);

        ex D be Division of ['c, b'] st D = (T2 . i0) & 1 <= ( len D) by A54;

        then ( len S2) in ( Seg ( len S2));

        then

         A62: ( len S2) in ( dom S2) by FINSEQ_1:def 3;

        

         A63: ( rng S1) c= ['a, c'] by INTEGRA1:def 2;

        now

          let i,j be Nat;

          assume that

           A64: i in ( dom T) and

           A65: j in ( dom T) and

           A66: i < j;

          

           A67: 1 <= i by A64, FINSEQ_3: 25;

          

           A68: j <= ( len T) by A65, FINSEQ_3: 25;

          

           A69: i <= ( len T) by A64, FINSEQ_3: 25;

           A70:

          now

            j <= (( len S1) + ( len S2)) by A68, FINSEQ_1: 22;

            then

             A71: (j - ( len S1)) <= ( len S2) by XREAL_1: 20;

            assume

             A72: j > ( len S1);

            then

             A73: (T . j) = (S2 . (j - ( len S1))) by A68, FINSEQ_1: 24;

            

             A74: (( len S1) + 1) <= j by A72, NAT_1: 13;

            then

            consider m be Nat such that

             A75: ((( len S1) + 1) + m) = j by NAT_1: 10;

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

            (1 + m) = (j - ( len S1)) by A75;

            then 1 <= (1 + m) by A74, XREAL_1: 19;

            then (1 + m) in ( Seg ( len S2)) by A75, A71;

            then

             A76: (j - ( len S1)) in ( dom S2) by A75, FINSEQ_1:def 3;

             A77:

            now

              i <= (( len S1) + ( len S2)) by A69, FINSEQ_1: 22;

              then

               A78: (i - ( len S1)) <= ( len S2) by XREAL_1: 20;

              

               A79: (i - ( len S1)) < (j - ( len S1)) by A66, XREAL_1: 14;

              assume

               A80: i > ( len S1);

              then

               A81: (( len S1) + 1) <= i by NAT_1: 13;

              then

              consider m be Nat such that

               A82: ((( len S1) + 1) + m) = i by NAT_1: 10;

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

              (1 + m) = (i - ( len S1)) by A82;

              then 1 <= (1 + m) by A81, XREAL_1: 19;

              then (1 + m) in ( Seg ( len S2)) by A82, A78;

              then

               A83: (i - ( len S1)) in ( dom S2) by A82, FINSEQ_1:def 3;

              (T . i) = (S2 . (i - ( len S1))) by A69, A80, FINSEQ_1: 24;

              hence (T . i) < (T . j) by A73, A76, A79, A83, SEQM_3:def 1;

            end;

            now

              assume i <= ( len S1);

              then

               A84: i in ( dom S1) by A67, FINSEQ_3: 25;

              then (T . i) = (S1 . i) by FINSEQ_1:def 7;

              then (T . i) in ( rng S1) by A84, FUNCT_1:def 3;

              then

               A85: (T . i) <= c by A14, A63, XXREAL_1: 1;

              ex DD be Division of ['c, b'] st DD = (T2 . i0) & for k be Element of NAT st k in ( dom DD) holds c < (DD . k) by A39;

              hence (T . i) < (T . j) by A73, A76, A85, XXREAL_0: 2;

            end;

            hence (T . i) < (T . j) by A77;

          end;

          

           A86: 1 <= j by A65, FINSEQ_3: 25;

          now

            assume

             A87: j <= ( len S1);

            then

             A88: j in ( dom S1) by A86, FINSEQ_3: 25;

            then

             A89: (T . j) = (S1 . j) by FINSEQ_1:def 7;

            i <= ( len S1) by A66, A87, XXREAL_0: 2;

            then

             A90: i in ( dom S1) by A67, FINSEQ_3: 25;

            then (T . i) = (S1 . i) by FINSEQ_1:def 7;

            hence (T . i) < (T . j) by A66, A90, A88, A89, SEQM_3:def 1;

          end;

          hence (T . i) < (T . j) by A70;

        end;

        then

         A91: T is non empty increasing FinSequence of REAL by SEQM_3:def 1;

        ( rng S2) c= ['c, b'] by INTEGRA1:def 2;

        then (( rng S1) \/ ( rng S2)) c= ( ['a, c'] \/ ['c, b']) by A63, XBOOLE_1: 13;

        then (( rng S1) \/ ( rng S2)) c= [.a, b.] by A13, A8, A14, A9, XXREAL_1: 174;

        then

         A92: ( rng T) c= ['a, b'] by A7, FINSEQ_1: 31;

        (T . ( len T)) = (T . (( len S1) + ( len S2))) by FINSEQ_1: 22

        .= (S2 . ( len S2)) by A62, FINSEQ_1:def 7

        .= ( upper_bound ['a, b']) by A60, A11, INTEGRA1:def 2;

        then T is Division of ['a, b'] by A92, A91, INTEGRA1:def 2;

        then T is Element of ( divs ['a, b']) by INTEGRA1:def 3;

        hence thesis;

      end;

      consider T be DivSequence of ['a, b'] such that

       A93: for i be Element of NAT holds P2[i, (T . i)] from FUNCT_2:sch 3( A61);

      

       A94: ( lower_bound ['a, b']) = a by A7, A59, INTEGRA1: 5;

      

       A95: for i,k be Element of NAT , S0 be Division of ['a, c'] st S0 = (T1 . i) & k in ( Seg ( len S0)) holds ( divset ((T . i),k)) = ( divset ((T1 . i),k))

      proof

        let i,k be Element of NAT , S0 be Division of ['a, c'];

        assume

         A96: S0 = (T1 . i);

        reconsider S = (T . i) as Division of ['a, b'];

        

         A97: ( divset ((T1 . i),k)) = [.( lower_bound ( divset ((T1 . i),k))), ( upper_bound ( divset ((T1 . i),k))).] by INTEGRA1: 4;

        consider S1 be Division of ['a, c'], S2 be Division of ['c, b'] such that

         A98: S1 = (T1 . i) and S2 = (T2 . i) and

         A99: (T . i) = (S1 ^ S2) by A93;

        assume

         A100: k in ( Seg ( len S0));

        then

         A101: k in ( dom S1) by A96, A98, FINSEQ_1:def 3;

        ( len S) = (( len S1) + ( len S2)) by A99, FINSEQ_1: 22;

        then ( len S1) <= ( len S) by NAT_1: 11;

        then ( Seg ( len S1)) c= ( Seg ( len S)) by FINSEQ_1: 5;

        then k in ( Seg ( len S)) by A96, A100, A98;

        then

         A102: k in ( dom S) by FINSEQ_1:def 3;

        

         A103: ( divset ((T . i),k)) = [.( lower_bound ( divset ((T . i),k))), ( upper_bound ( divset ((T . i),k))).] by INTEGRA1: 4;

         A104:

        now

          k <= ( len S1) & (k - 1) <= (k - 0 ) by A96, A100, A98, FINSEQ_1: 1, XREAL_1: 10;

          then

           A105: (k - 1) <= ( len S1) by XXREAL_0: 2;

          assume

           A106: k <> 1;

          1 <= k by A100, FINSEQ_1: 1;

          then

           A107: 1 < k by A106, XXREAL_0: 1;

          then (1 + 1) <= k by NAT_1: 13;

          then

           A108: (2 - 1) <= (k - 1) by XREAL_1: 9;

          (k - 1) is Element of NAT by A107, NAT_1: 20;

          then (k - 1) in ( Seg ( len S1)) by A105, A108;

          then

           A109: (k - 1) in ( dom S1) by FINSEQ_1:def 3;

          

          thus ( divset ((T . i),k)) = [.(S . (k - 1)), ( upper_bound ( divset ((T . i),k))).] by A102, A103, A106, INTEGRA1:def 4

          .= [.(S . (k - 1)), (S . k).] by A102, A106, INTEGRA1:def 4

          .= [.(S . (k - 1)), (S1 . k).] by A99, A101, FINSEQ_1:def 7

          .= [.(S1 . (k - 1)), (S1 . k).] by A99, A109, FINSEQ_1:def 7

          .= [.( lower_bound ( divset ((T1 . i),k))), (S1 . k).] by A98, A101, A106, INTEGRA1:def 4

          .= ( divset ((T1 . i),k)) by A98, A101, A97, A106, INTEGRA1:def 4;

        end;

        now

          assume

           A110: k = 1;

          

          hence ( divset ((T . i),k)) = [.( lower_bound ['a, b']), ( upper_bound ( divset ((T . i),k))).] by A102, A103, INTEGRA1:def 4

          .= [.( lower_bound ['a, b']), (S . k).] by A102, A110, INTEGRA1:def 4

          .= [.( lower_bound ['a, b']), (S1 . k).] by A99, A101, FINSEQ_1:def 7

          .= [.( lower_bound ( divset ((T1 . i),k))), (S1 . 1).] by A94, A16, A98, A101, A110, INTEGRA1:def 4

          .= ( divset ((T1 . i),k)) by A98, A101, A97, A110, INTEGRA1:def 4;

        end;

        hence thesis by A104;

      end;

      

       A111: ( upper_bound ['a, c']) = c by A14, A15, INTEGRA1: 5;

      

       A112: for i,k be Element of NAT , S01 be Division of ['a, c'], S02 be Division of ['c, b'] st S01 = (T1 . i) & S02 = (T2 . i) & k in ( Seg ( len S02)) holds ( divset ((T . i),(( len S01) + k))) = ( divset ((T2 . i),k))

      proof

        let i,k be Element of NAT , S01 be Division of ['a, c'], S02 be Division of ['c, b'];

        assume that

         A113: S01 = (T1 . i) and

         A114: S02 = (T2 . i);

        reconsider S = (T . i) as Division of ['a, b'];

        consider S1 be Division of ['a, c'], S2 be Division of ['c, b'] such that

         A115: S1 = (T1 . i) and

         A116: S2 = (T2 . i) and

         A117: (T . i) = (S1 ^ S2) by A93;

        assume

         A118: k in ( Seg ( len S02));

        then

         A119: k in ( dom S2) by A114, A116, FINSEQ_1:def 3;

        then

         A120: (( len S1) + k) in ( dom S) by A117, FINSEQ_1: 28;

        

         A121: ( divset ((T2 . i),k)) = [.( lower_bound ( divset ((T2 . i),k))), ( upper_bound ( divset ((T2 . i),k))).] by INTEGRA1: 4;

        

         A122: ( divset ((T . i),(( len S1) + k))) = [.( lower_bound ( divset ((T . i),(( len S1) + k)))), ( upper_bound ( divset ((T . i),(( len S1) + k)))).] by INTEGRA1: 4;

         A123:

        now

          k <= ( len S2) & (k - 1) <= (k - 0 ) by A114, A118, A116, FINSEQ_1: 1, XREAL_1: 10;

          then

           A124: (k - 1) <= ( len S2) by XXREAL_0: 2;

          assume

           A125: k <> 1;

          

           A126: 1 <= k by A118, FINSEQ_1: 1;

          then

           A127: 1 < k by A125, XXREAL_0: 1;

          then (1 + 1) <= k by NAT_1: 13;

          then

           A128: (2 - 1) <= (k - 1) by XREAL_1: 9;

          (k - 1) is Element of NAT by A127, NAT_1: 20;

          then (k - 1) in ( Seg ( len S2)) by A124, A128;

          then

           A129: (k - 1) in ( dom S2) by FINSEQ_1:def 3;

          

           A130: (1 + 0 ) < (k + ( len S1)) by A126, XREAL_1: 8;

          

          hence ( divset ((T . i),(( len S1) + k))) = [.(S . ((( len S1) + k) - 1)), ( upper_bound ( divset ((T . i),(( len S1) + k)))).] by A120, A122, INTEGRA1:def 4

          .= [.(S . ((( len S1) + k) - 1)), (S . (( len S1) + k)).] by A120, A130, INTEGRA1:def 4

          .= [.(S . (( len S1) + (k - 1))), (S2 . k).] by A117, A119, FINSEQ_1:def 7

          .= [.(S2 . (k - 1)), (S2 . k).] by A117, A129, FINSEQ_1:def 7

          .= [.( lower_bound ( divset ((T2 . i),k))), (S2 . k).] by A116, A119, A125, INTEGRA1:def 4

          .= ( divset ((T2 . i),k)) by A116, A119, A121, A125, INTEGRA1:def 4;

        end;

        now

          ( len S1) in ( Seg ( len S1)) by FINSEQ_1: 3;

          then

           A131: ( len S1) in ( dom S1) by FINSEQ_1:def 3;

          assume

           A132: k = 1;

          ( len S1) <> 0 ;

          then

           A133: (( len S1) + k) <> 1 by A132;

          

          hence ( divset ((T . i),(( len S1) + k))) = [.(S . ((( len S1) + k) - 1)), ( upper_bound ( divset ((T . i),(( len S1) + k)))).] by A120, A122, INTEGRA1:def 4

          .= [.(S1 . ( len S1)), ( upper_bound ( divset ((T . i),(( len S1) + k)))).] by A117, A132, A131, FINSEQ_1:def 7

          .= [.( upper_bound ['a, c']), ( upper_bound ( divset ((T . i),(( len S1) + k)))).] by INTEGRA1:def 2

          .= [.( lower_bound ['c, b']), (S . (( len S1) + k)).] by A19, A111, A120, A133, INTEGRA1:def 4

          .= [.( lower_bound ['c, b']), (S2 . k).] by A117, A119, FINSEQ_1:def 7

          .= [.( lower_bound ( divset ((T2 . i),k))), (S2 . 1).] by A116, A119, A132, INTEGRA1:def 4

          .= ( divset ((T2 . i),k)) by A116, A119, A121, A132, INTEGRA1:def 4;

        end;

        hence thesis by A113, A115, A123;

      end;

      set XAB = ( chi ( ['a, b'], ['a, b']));

      

       A134: for i,k be Element of NAT , S0 be Division of ['c, b'] st S0 = (T2 . i) & k in ( Seg ( len S0)) holds ( divset ((T2 . i),k)) c= ['c, b']

      proof

        let i,k be Element of NAT , S0 be Division of ['c, b'];

        assume that

         A135: S0 = (T2 . i) and

         A136: k in ( Seg ( len S0));

        k in ( dom S0) by A136, FINSEQ_1:def 3;

        hence thesis by A135, INTEGRA1: 8;

      end;

      

       A137: ['a, c'] c= ['a, b'] by A7, A8, A14, XXREAL_1: 34;

      then (f | ['a, c']) is bounded by A4, RFUNCT_1: 74;

      then

       A138: (FAC | ['a, c']) is bounded;

      

       A139: for i,k be Element of NAT , S0 be Division of ['a, c'] st S0 = (T1 . i) & k in ( Seg ( len S0)) holds ( divset ((T1 . i),k)) c= ['a, c']

      proof

        let i,k be Element of NAT , S0 be Division of ['a, c'];

        assume that

         A140: S0 = (T1 . i) and

         A141: k in ( Seg ( len S0));

        k in ( dom S0) by A141, FINSEQ_1:def 3;

        hence thesis by A140, INTEGRA1: 8;

      end;

      

       A142: for i be Element of NAT holds ( upper_volume ((f || ['a, b']),(T . i))) = (( upper_volume (FAC,(T1 . i))) ^ ( upper_volume (FCB,(T2 . i))))

      proof

        let i be Element of NAT ;

        reconsider F = ( upper_volume (FAB,(T . i))) as FinSequence of REAL ;

        reconsider F1 = ( upper_volume (FAC,(T1 . i))) as FinSequence of REAL ;

        reconsider F2 = ( upper_volume (FCB,(T2 . i))) as FinSequence of REAL ;

        reconsider S = (T . i) as Division of ['a, b'];

        consider S1 be Division of ['a, c'], S2 be Division of ['c, b'] such that

         A143: S1 = (T1 . i) and

         A144: S2 = (T2 . i) and

         A145: (T . i) = (S1 ^ S2) by A93;

        

         A146: ( len F) = ( len S) by INTEGRA1:def 6

        .= (( len S1) + ( len S2)) by A145, FINSEQ_1: 22

        .= (( len F1) + ( len S2)) by A143, INTEGRA1:def 6

        .= (( len F1) + ( len F2)) by A144, INTEGRA1:def 6;

         A147:

        now

          let k be Nat;

          assume

           A148: k in ( dom F2);

          then

           A149: k in ( Seg ( len F2)) by FINSEQ_1:def 3;

          then 1 <= k by FINSEQ_1: 1;

          then

           A150: (1 + ( len F1)) <= (k + ( len F1)) by XREAL_1: 6;

          k <= ( len F2) by A149, FINSEQ_1: 1;

          then

           A151: (( len F1) + k) <= ( len F) by A146, XREAL_1: 6;

          1 <= (1 + ( len F1)) by NAT_1: 11;

          then 1 <= (k + ( len F1)) by A150, XXREAL_0: 2;

          then (k + ( len F1)) in ( Seg ( len F)) by A151;

          then (( len F1) + k) in ( Seg ( len S)) by INTEGRA1:def 6;

          then (( len F1) + k) in ( dom S) by FINSEQ_1:def 3;

          then

           A152: (F . (( len F1) + k)) = (( upper_bound ( rng (FAB | ( divset ((T . i),(( len F1) + k)))))) * ( vol ( divset ((T . i),(( len F1) + k))))) by INTEGRA1:def 6;

          k in ( Seg ( len F2)) by A148, FINSEQ_1:def 3;

          then

           A153: k in ( Seg ( len S2)) by A144, INTEGRA1:def 6;

          then

           A154: k in ( dom S2) by FINSEQ_1:def 3;

          ( len F1) = ( len S1) by A143, INTEGRA1:def 6;

          then

           A155: ( divset ((T . i),(( len F1) + k))) = ( divset ((T2 . i),k)) by A112, A143, A144, A153;

          then

           A156: ( divset ((T . i),(( len F1) + k))) c= ['c, b'] by A134, A144, A153;

          then ( divset ((T . i),(( len F1) + k))) c= ['a, b'] by A17;

          then (F . (( len F1) + k)) = (( upper_bound ( rng (FCB | ( divset ((T2 . i),k))))) * ( vol ( divset ((T2 . i),k)))) by A152, A155, A156, Th3;

          hence (F . (( len F1) + k)) = (F2 . k) by A144, A154, INTEGRA1:def 6;

        end;

         A157:

        now

          let k be Nat;

          assume k in ( dom F1);

          then

           A158: k in ( Seg ( len F1)) by FINSEQ_1:def 3;

          then

           A159: k in ( Seg ( len S1)) by A143, INTEGRA1:def 6;

          then

           A160: k in ( dom S1) by FINSEQ_1:def 3;

          ( len F1) <= ( len F) by A146, NAT_1: 11;

          then ( Seg ( len F1)) c= ( Seg ( len F)) by FINSEQ_1: 5;

          then k in ( Seg ( len F)) by A158;

          then k in ( Seg ( len S)) by INTEGRA1:def 6;

          then k in ( dom S) by FINSEQ_1:def 3;

          then

           A161: (F . k) = (( upper_bound ( rng (FAB | ( divset ((T . i),k))))) * ( vol ( divset ((T . i),k)))) by INTEGRA1:def 6;

          

           A162: ( divset ((T . i),k)) = ( divset ((T1 . i),k)) by A95, A143, A159;

          then

           A163: ( divset ((T . i),k)) c= ['a, c'] by A139, A143, A159;

          then ( divset ((T . i),k)) c= ['a, b'] by A137;

          then (F . k) = (( upper_bound ( rng (FAC | ( divset ((T1 . i),k))))) * ( vol ( divset ((T1 . i),k)))) by A161, A162, A163, Th3;

          hence (F . k) = (F1 . k) by A143, A160, INTEGRA1:def 6;

        end;

        ( dom F) = ( Seg (( len F1) + ( len F2))) by A146, FINSEQ_1:def 3;

        hence thesis by A157, A147, FINSEQ_1:def 7;

      end;

      

       A164: for i be Element of NAT holds ( Sum ( upper_volume (FAB,(T . i)))) = (( Sum ( upper_volume (FAC,(T1 . i)))) + ( Sum ( upper_volume (FCB,(T2 . i)))))

      proof

        let i be Element of NAT ;

        ( upper_volume (FAB,(T . i))) = (( upper_volume (FAC,(T1 . i))) ^ ( upper_volume (FCB,(T2 . i)))) by A142;

        hence thesis by RVSUM_1: 75;

      end;

      now

        let i be Nat;

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

        

        thus (( upper_sum (FAB,T)) . i) = ( upper_sum (FAB,(T . ii))) by INTEGRA2:def 2

        .= (( upper_sum (FAC,(T1 . ii))) + ( Sum ( upper_volume (FCB,(T2 . ii))))) by A164

        .= ((( upper_sum (FAC,T1)) . i) + ( upper_sum (FCB,(T2 . ii)))) by INTEGRA2:def 2

        .= ((( upper_sum (FAC,T1)) . i) + (( upper_sum (FCB,T2)) . i)) by INTEGRA2:def 2;

      end;

      then

       A165: ( upper_sum (FAB,T)) = (( upper_sum (FAC,T1)) + ( upper_sum (FCB,T2))) by SEQ_1: 7;

      

       A166: FCB is Function of ['c, b'], REAL by A2, A17, Lm1, XBOOLE_1: 1;

      then

       A167: ( lower_integral FCB) <= ( upper_integral FCB) by A18, INTEGRA1: 49;

       A168:

      now

        let e be Real;

        assume 0 < e;

        then

        consider m be Nat such that

         A169: for n be Nat st m <= n holds |.((( delta PS2) . n) - 0 ).| < e by A25, SEQ_2:def 7;

        take m;

        hereby

          let n be Nat;

          

           A170: n <= (n + K) by NAT_1: 11;

          assume m <= n;

          then m <= (n + K) by A170, XXREAL_0: 2;

          then |.((( delta PS2) . (n + K)) - 0 ).| < e by A169;

          then

           A171: |.(( delta (PS2 . (n + K))) - 0 ).| < e by INTEGRA3:def 2;

          n in NAT by ORDINAL1:def 12;

          then ex k be Element of NAT , e1 be Division of ['c, b'] st k = n & e1 = (S2 . n) & e1 = (PS2 . (k + K)) by A29;

          hence |.((( delta S2) . n) - 0 ).| < e by A171, INTEGRA3:def 2;

        end;

      end;

       A172:

      now

        let e be Real;

        assume

         A173: e > 0 ;

        then

        consider m be Nat such that

         A174: for n be Nat st m <= n holds |.((( delta S2) . n) - 0 ).| < (e / 2) by A168, XREAL_1: 215;

        take m;

        

         A175: (e / 2) < e by A173, XREAL_1: 216;

        let nn be Nat;

        assume

         A176: m <= nn;

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

         |.((( delta S2) . n) - 0 ).| < (e / 2) by A174, A176;

        then 0 <= ( delta (S2 . n)) & |.( delta (S2 . n)).| < (e / 2) by INTEGRA3: 9, INTEGRA3:def 2;

        then

         A177: ( max ( rng ( upper_volume (XCB,(S2 . n))))) < (e / 2) by ABSVALUE:def 1;

        

         A178: for y be Real st y in ( rng ( upper_volume (XCB,(T2 . n)))) holds y < e

        proof

          reconsider D = (T2 . n) as Division of ['c, b'];

          let y be Real;

          assume y in ( rng ( upper_volume (XCB,(T2 . n))));

          then

          consider x be object such that

           A179: x in ( dom ( upper_volume (XCB,(T2 . n)))) and

           A180: y = (( upper_volume (XCB,(T2 . n))) . x) by FUNCT_1:def 3;

          reconsider i = x as Element of NAT by A179;

          

           A181: x in ( Seg ( len ( upper_volume (XCB,(T2 . n))))) by A179, FINSEQ_1:def 3;

          consider E1 be Division of ['c, b'] such that

           A182: E1 = (S2 . n) and

           A183: 2 <= ( len E1) by A30;

          set i1 = (i + 1);

          consider E be Division of ['c, b'] such that

           A184: E = (S2 . n) and

           A185: (T2 . n) = (E /^ 1) by A38;

          

           A186: 1 <= ( len E1) by A183, XXREAL_0: 2;

          then

           A187: ( len D) = (( len E) - 1) by A184, A185, A182, RFINSEQ:def 1;

          

           A188: ( len ( upper_volume (XCB,(T2 . n)))) = ( len D) by INTEGRA1:def 6;

          then

           A189: ( dom ( upper_volume (XCB,(T2 . n)))) = ( dom D) by FINSEQ_3: 29;

           A190:

          now

            ( len ( upper_volume (XCB,(S2 . n)))) = ( len E) by A184, INTEGRA1:def 6;

            then 2 in ( Seg ( len ( upper_volume (XCB,(S2 . n))))) by A184, A182, A183;

            then 2 in ( dom ( upper_volume (XCB,(S2 . n)))) by FINSEQ_1:def 3;

            then (( upper_volume (XCB,(S2 . n))) . 2) in ( rng ( upper_volume (XCB,(S2 . n)))) by FUNCT_1:def 3;

            then (( upper_volume (XCB,(S2 . n))) . 2) <= ( max ( rng ( upper_volume (XCB,(S2 . n))))) by XXREAL_2:def 8;

            then

             A191: (( upper_volume (XCB,(S2 . n))) . 2) < (e / 2) by A177, XXREAL_0: 2;

            assume

             A192: i = 1;

            then

             A193: 1 in ( dom D) by A181, A188, FINSEQ_1:def 3;

            ( len ( upper_volume (XCB,(S2 . n)))) = (( len D) + 1) by A184, A187, INTEGRA1:def 6;

            then ( len ( upper_volume (XCB,(S2 . n)))) = (( len ( upper_volume (XCB,(T2 . n)))) + 1) by INTEGRA1:def 6;

            then 1 in ( Seg ( len ( upper_volume (XCB,(S2 . n))))) by A181, A192, FINSEQ_2: 8;

            then 1 in ( dom ( upper_volume (XCB,(S2 . n)))) by FINSEQ_1:def 3;

            then (( upper_volume (XCB,(S2 . n))) . 1) in ( rng ( upper_volume (XCB,(S2 . n)))) by FUNCT_1:def 3;

            then (( upper_volume (XCB,(S2 . n))) . 1) <= ( max ( rng ( upper_volume (XCB,(S2 . n))))) by XXREAL_2:def 8;

            then

             A194: (( upper_volume (XCB,(S2 . n))) . 1) < (e / 2) by A177, XXREAL_0: 2;

            

             A195: 2 in ( dom E) by A184, A182, A183, FINSEQ_3: 25;

            1 in ( Seg ( len E)) by A184, A182, A186;

            then

             A196: 1 in ( dom E) by FINSEQ_1:def 3;

            ( divset ((S2 . n),1)) = [.( lower_bound ( divset ((S2 . n),1))), ( upper_bound ( divset ((S2 . n),1))).] by INTEGRA1: 4;

            then

             A197: ( divset ((S2 . n),1)) = [.( lower_bound ['c, b']), ( upper_bound ( divset ((S2 . n),1))).] by A184, A196, INTEGRA1:def 4;

            then

             A198: [.( lower_bound ['c, b']), ( upper_bound ( divset ((S2 . n),1))).] = [.( lower_bound [.( lower_bound ['c, b']), ( upper_bound ( divset ((S2 . n),1))).]), ( upper_bound [.( lower_bound ['c, b']), ( upper_bound ( divset ((S2 . n),1))).]).] by INTEGRA1: 4;

            

             A199: ( divset ((T2 . n),i)) = [.( lower_bound ( divset ((T2 . n),1))), ( upper_bound ( divset ((T2 . n),1))).] by A192, INTEGRA1: 4

            .= [.( lower_bound ['c, b']), ( upper_bound ( divset ((T2 . n),1))).] by A193, INTEGRA1:def 4

            .= [.( lower_bound ['c, b']), (D . 1).] by A193, INTEGRA1:def 4

            .= [.( lower_bound ['c, b']), (E . (1 + 1)).] by A184, A185, A182, A186, A193, RFINSEQ:def 1

            .= [.( lower_bound ['c, b']), ( upper_bound ( divset ((S2 . n),2))).] by A184, A195, INTEGRA1:def 4;

            then [.( lower_bound ['c, b']), ( upper_bound ( divset ((S2 . n),2))).] = [.( lower_bound [.( lower_bound ['c, b']), ( upper_bound ( divset ((S2 . n),2))).]), ( upper_bound [.( lower_bound ['c, b']), ( upper_bound ( divset ((S2 . n),2))).]).] by INTEGRA1: 4;

            then

             A200: ( lower_bound ['c, b']) = ( lower_bound [.( lower_bound ['c, b']), ( upper_bound ( divset ((S2 . n),2))).]) & ( upper_bound ( divset ((S2 . n),2))) = ( upper_bound [.( lower_bound ['c, b']), ( upper_bound ( divset ((S2 . n),2))).]) by A199, INTEGRA1: 5;

            y = ( vol ( divset ((T2 . n),1))) by A179, A180, A189, A192, INTEGRA1: 20;

            then y = ((( upper_bound ( divset ((S2 . n),2))) - ( upper_bound ( divset ((S2 . n),1)))) + (( upper_bound [.( lower_bound ['c, b']), ( upper_bound ( divset ((S2 . n),1))).]) - ( lower_bound ['c, b']))) by A192, A199, A200, A197;

            then

             A201: y = ((( upper_bound ( divset ((S2 . n),2))) - ( upper_bound ( divset ((S2 . n),1)))) + ( vol ( divset ((S2 . n),1)))) by A197, A198, INTEGRA1: 5;

            ( divset ((S2 . n),2)) = [.( lower_bound ( divset ((S2 . n),2))), ( upper_bound ( divset ((S2 . n),2))).] by INTEGRA1: 4;

            then ( divset ((S2 . n),2)) = [.(E . (2 - 1)), ( upper_bound ( divset ((S2 . n),2))).] by A184, A195, INTEGRA1:def 4;

            then

             A202: ( divset ((S2 . n),2)) = [.( upper_bound ( divset ((S2 . n),1))), ( upper_bound ( divset ((S2 . n),2))).] by A184, A196, INTEGRA1:def 4;

            then [.( upper_bound ( divset ((S2 . n),1))), ( upper_bound ( divset ((S2 . n),2))).] = [.( lower_bound [.( upper_bound ( divset ((S2 . n),1))), ( upper_bound ( divset ((S2 . n),2))).]), ( upper_bound [.( upper_bound ( divset ((S2 . n),1))), ( upper_bound ( divset ((S2 . n),2))).]).] by INTEGRA1: 4;

            then y = (( vol ( divset ((S2 . n),2))) + ( vol ( divset ((S2 . n),1)))) by A202, A201, INTEGRA1: 5;

            then y = ((( upper_volume (XCB,(S2 . n))) . 2) + ( vol ( divset ((S2 . n),1)))) by A184, A195, INTEGRA1: 20;

            then y = ((( upper_volume (XCB,(S2 . n))) . 2) + (( upper_volume (XCB,(S2 . n))) . 1)) by A184, A196, INTEGRA1: 20;

            then y < ((e / 2) + (e / 2)) by A191, A194, XREAL_1: 8;

            hence thesis;

          end;

          

           A203: y = (( upper_bound ( rng (XCB | ( divset ((T2 . n),i))))) * ( vol ( divset ((T2 . n),i)))) by A179, A180, A189, INTEGRA1:def 6;

          now

            ( len ( upper_volume (XCB,(S2 . n)))) = (( len D) + 1) by A184, A187, INTEGRA1:def 6;

            then ( len ( upper_volume (XCB,(S2 . n)))) = (( len ( upper_volume (XCB,(T2 . n)))) + 1) by INTEGRA1:def 6;

            then

             A204: i1 in ( Seg ( len ( upper_volume (XCB,(S2 . n))))) by A181, FINSEQ_1: 60;

            then

             A205: i1 in ( dom ( upper_volume (XCB,(S2 . n)))) by FINSEQ_1:def 3;

            

             A206: i1 in ( dom ( upper_volume (XCB,(S2 . n)))) by A204, FINSEQ_1:def 3;

            

             A207: i in ( dom D) by A181, A188, FINSEQ_1:def 3;

            ( Seg (( len D) + 1)) = ( Seg ( len E)) by A187;

            then i1 in ( Seg ( len E)) by A181, A188, FINSEQ_1: 60;

            then

             A208: i1 in ( dom E) by FINSEQ_1:def 3;

            ( len ( upper_volume (XCB,(S2 . n)))) = ( len E) by A184, INTEGRA1:def 6;

            then

             A209: ( dom ( upper_volume (XCB,(S2 . n)))) = ( dom E) by FINSEQ_3: 29;

            assume

             A210: i <> 1;

            i in ( Seg ( len D)) by A179, A188, FINSEQ_1:def 3;

            then 1 <= i by FINSEQ_1: 1;

            then

             A211: 1 < i by A210, XXREAL_0: 1;

            then

             A212: (i - 1) in ( Seg ( len D)) by A181, A188, FINSEQ_3: 12;

            then

             A213: (i - 1) in ( dom D) by FINSEQ_1:def 3;

            reconsider i9 = (i - 1) as Element of NAT by A212;

            (1 + 1) < (i + 1) by A211, XREAL_1: 8;

            then

             A214: i1 <> 1;

            ( divset ((T2 . n),i)) = [.( lower_bound ( divset ((T2 . n),i))), ( upper_bound ( divset ((T2 . n),i))).] by INTEGRA1: 4

            .= [.(D . (i - 1)), ( upper_bound ( divset ((T2 . n),i))).] by A210, A207, INTEGRA1:def 4

            .= [.(D . (i - 1)), (D . i).] by A210, A207, INTEGRA1:def 4

            .= [.(E . (i9 + 1)), (D . i).] by A184, A185, A182, A186, A213, RFINSEQ:def 1

            .= [.(E . ((i - 1) + 1)), (E . (i + 1)).] by A184, A185, A182, A186, A207, RFINSEQ:def 1

            .= [.(E . (i1 - 1)), ( upper_bound ( divset ((S2 . n),i1))).] by A184, A214, A208, INTEGRA1:def 4

            .= [.( lower_bound ( divset ((S2 . n),i1))), ( upper_bound ( divset ((S2 . n),i1))).] by A184, A214, A208, INTEGRA1:def 4

            .= ( divset ((S2 . n),i1)) by INTEGRA1: 4;

            then y = (( upper_volume (XCB,(S2 . n))) . i1) by A203, A184, A205, A209, INTEGRA1:def 6;

            then y in ( rng ( upper_volume (XCB,(S2 . n)))) by A206, FUNCT_1:def 3;

            then y <= ( max ( rng ( upper_volume (XCB,(S2 . n))))) by XXREAL_2:def 8;

            then y < (e / 2) by A177, XXREAL_0: 2;

            hence thesis by A175, XXREAL_0: 2;

          end;

          hence thesis by A190;

        end;

        ( max ( rng ( upper_volume (XCB,(T2 . n))))) in ( rng ( upper_volume (XCB,(T2 . n)))) by XXREAL_2:def 8;

        then 0 <= ( delta (T2 . n)) & ( delta (T2 . n)) < e by A178, INTEGRA3: 9;

        then |.( delta (T2 . n)).| < e by ABSVALUE:def 1;

        hence |.((( delta T2) . nn) - 0 ).| < e by INTEGRA3:def 2;

      end;

      then

       A215: ( delta T2) is convergent by SEQ_2:def 6;

      then

       A216: ( lim ( delta T2)) = 0 by A172, SEQ_2:def 7;

      then

       A217: ( upper_sum (FCB,T2)) is convergent & ( lim ( upper_sum (FCB,T2))) = ( upper_integral FCB) by A166, A18, A215, INTEGRA4: 9;

       A218:

      now

        let e be Real;

        assume

         A219: 0 < e;

        then

        consider n1 be Nat such that

         A220: for m be Nat st n1 <= m holds |.((( delta T1) . m) - 0 ).| < e by A53, SEQ_2:def 7;

        consider n2 be Nat such that

         A221: for m be Nat st n2 <= m holds |.((( delta T2) . m) - 0 ).| < e by A172, A219;

        reconsider n = ( max (n1,n2)) as Nat by TARSKI: 1;

        take n;

        let mm be Nat;

        assume

         A222: n <= mm;

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

        n2 <= n by XXREAL_0: 25;

        then n2 <= m by A222, XXREAL_0: 2;

        then |.((( delta T2) . m) - 0 ).| < e by A221;

        then

         A223: |.( delta (T2 . m)).| < e by INTEGRA3:def 2;

         0 <= ( delta (T2 . m)) by INTEGRA3: 9;

        then

         A224: ( max ( rng ( upper_volume (XCB,(T2 . m))))) < e by A223, ABSVALUE:def 1;

        n1 <= n by XXREAL_0: 25;

        then n1 <= m by A222, XXREAL_0: 2;

        then |.((( delta T1) . m) - 0 ).| < e by A220;

        then

         A225: |.( delta (T1 . m)).| < e by INTEGRA3:def 2;

         0 <= ( delta (T1 . m)) by INTEGRA3: 9;

        then

         A226: ( max ( rng ( upper_volume (XAC,(T1 . m))))) < e by A225, ABSVALUE:def 1;

        

         A227: for r be Real st r in ( rng ( upper_volume (XAB,(T . m)))) holds r < e

        proof

          reconsider Tm = (T . m) as Division of ['a, b'];

          let y be Real;

          assume y in ( rng ( upper_volume (XAB,(T . m))));

          then

          consider x be object such that

           A228: x in ( dom ( upper_volume (XAB,(T . m)))) and

           A229: y = (( upper_volume (XAB,(T . m))) . x) by FUNCT_1:def 3;

          reconsider i = x as Element of NAT by A228;

          

           A230: x in ( Seg ( len ( upper_volume (XAB,(T . m))))) by A228, FINSEQ_1:def 3;

          then

           A231: 1 <= i by FINSEQ_1: 1;

          

           A232: ( len ( upper_volume (XAB,(T . m)))) = ( len Tm) by INTEGRA1:def 6;

          then

           A233: i <= ( len Tm) by A230, FINSEQ_1: 1;

          ( dom ( upper_volume (XAB,(T . m)))) = ( dom Tm) by A232, FINSEQ_3: 29;

          then

           A234: y = (( upper_bound ( rng (XAB | ( divset ((T . m),i))))) * ( vol ( divset ((T . m),i)))) by A228, A229, INTEGRA1:def 6;

          consider S1 be Division of ['a, c'], S2 be Division of ['c, b'] such that

           A235: S1 = (T1 . m) and

           A236: S2 = (T2 . m) and

           A237: (T . m) = (S1 ^ S2) by A93;

          

           A238: ( len Tm) = (( len S1) + ( len S2)) by A237, FINSEQ_1: 22;

          per cases ;

            suppose i <= ( len S1);

            then

             A239: i in ( Seg ( len S1)) by A231;

            then

             A240: i in ( dom S1) by FINSEQ_1:def 3;

            ( len ( upper_volume (XAC,(T1 . m)))) = ( len S1) by A235, INTEGRA1:def 6;

            then

             A241: i in ( dom ( upper_volume (XAC,(T1 . m)))) by A239, FINSEQ_1:def 3;

            

             A242: ( divset ((T1 . m),i)) = ( divset ((T . m),i)) by A95, A235, A239;

            

             A243: ( divset ((T1 . m),i)) c= ['a, c'] by A139, A235, A239;

            then ( divset ((T1 . m),i)) c= ['a, b'] by A137;

            then (XAC | ( divset ((T1 . m),i))) = (XAB | ( divset ((T . m),i))) by A242, A243, Th4;

            then y = (( upper_volume (XAC,(T1 . m))) . i) by A234, A235, A240, A242, INTEGRA1:def 6;

            then y in ( rng ( upper_volume (XAC,(T1 . m)))) by A241, FUNCT_1:def 3;

            then y <= ( max ( rng ( upper_volume (XAC,(T1 . m))))) by XXREAL_2:def 8;

            hence thesis by A226, XXREAL_0: 2;

          end;

            suppose i > ( len S1);

            then

             A244: (( len S1) + 1) <= i by NAT_1: 13;

            then

            consider k be Nat such that

             A245: ((( len S1) + 1) + k) = i by NAT_1: 10;

            reconsider k as Element of NAT by ORDINAL1:def 12;

            set i1 = (1 + k);

            

             A246: (i - ( len S1)) <= ( len S2) by A238, A233, XREAL_1: 20;

            (1 + k) = (i - ( len S1)) by A245;

            then 1 <= (1 + k) by A244, XREAL_1: 19;

            then

             A247: (1 + k) in ( Seg ( len S2)) by A245, A246;

            then

             A248: (1 + k) in ( dom S2) by FINSEQ_1:def 3;

            

             A249: ( divset ((T2 . m),i1)) = ( divset ((T . m),(( len S1) + i1))) by A112, A235, A236, A247;

            

             A250: ( divset ((T2 . m),i1)) c= ['c, b'] by A134, A236, A247;

            then ( divset ((T2 . m),i1)) c= ['a, b'] by A17;

            then y = (( upper_bound ( rng (XCB | ( divset ((T2 . m),i1))))) * ( vol ( divset ((T2 . m),i1)))) by A234, A245, A249, A250, Th4;

            then

             A251: y = (( upper_volume (XCB,(T2 . m))) . i1) by A236, A248, INTEGRA1:def 6;

            ( len ( upper_volume (XCB,(T2 . m)))) = ( len S2) by A236, INTEGRA1:def 6;

            then i1 in ( dom ( upper_volume (XCB,(T2 . m)))) by A247, FINSEQ_1:def 3;

            then y in ( rng ( upper_volume (XCB,(T2 . m)))) by A251, FUNCT_1:def 3;

            then y <= ( max ( rng ( upper_volume (XCB,(T2 . m))))) by XXREAL_2:def 8;

            hence thesis by A224, XXREAL_0: 2;

          end;

        end;

        

         A252: 0 <= ( delta (T . m)) by INTEGRA3: 9;

        ( max ( rng ( upper_volume (XAB,(T . m))))) in ( rng ( upper_volume (XAB,(T . m)))) by XXREAL_2:def 8;

        then ( delta (T . m)) < e by A227;

        then |.( delta (T . m)).| < e by A252, ABSVALUE:def 1;

        hence |.((( delta T) . mm) - 0 ).| < e by INTEGRA3:def 2;

      end;

      then

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

      then

       A254: ( lim ( delta T)) = 0 by A218, SEQ_2:def 7;

      (FAB | ['a, b']) is bounded by A4;

      then

       A255: ( upper_integral FAB) = ( lim ( upper_sum (FAB,T))) by A12, A253, A254, INTEGRA4: 9;

      

       A256: for i be Element of NAT holds ( lower_volume (FAB,(T . i))) = (( lower_volume (FAC,(T1 . i))) ^ ( lower_volume (FCB,(T2 . i))))

      proof

        let i be Element of NAT ;

        reconsider F = ( lower_volume (FAB,(T . i))) as FinSequence of REAL ;

        reconsider F1 = ( lower_volume (FAC,(T1 . i))) as FinSequence of REAL ;

        reconsider F2 = ( lower_volume (FCB,(T2 . i))) as FinSequence of REAL ;

        reconsider S = (T . i) as Division of ['a, b'];

        consider S1 be Division of ['a, c'], S2 be Division of ['c, b'] such that

         A257: S1 = (T1 . i) and

         A258: S2 = (T2 . i) and

         A259: (T . i) = (S1 ^ S2) by A93;

        

         A260: ( len F) = ( len S) by INTEGRA1:def 7

        .= (( len S1) + ( len S2)) by A259, FINSEQ_1: 22

        .= (( len F1) + ( len S2)) by A257, INTEGRA1:def 7;

        then

         A261: ( len F) = (( len F1) + ( len F2)) by A258, INTEGRA1:def 7;

         A262:

        now

          let k be Nat;

          assume k in ( dom F2);

          then

           A263: k in ( Seg ( len F2)) by FINSEQ_1:def 3;

          then 1 <= k by FINSEQ_1: 1;

          then

           A264: (1 + ( len F1)) <= (k + ( len F1)) by XREAL_1: 6;

          k <= ( len F2) by A263, FINSEQ_1: 1;

          then

           A265: (( len F1) + k) <= ( len F) by A261, XREAL_1: 6;

          1 <= (1 + ( len F1)) by NAT_1: 11;

          then 1 <= (k + ( len F1)) by A264, XXREAL_0: 2;

          then (k + ( len F1)) in ( Seg ( len F)) by A265;

          then (( len F1) + k) in ( Seg ( len S)) by INTEGRA1:def 7;

          then (( len F1) + k) in ( dom S) by FINSEQ_1:def 3;

          then

           A266: (F . (( len F1) + k)) = (( lower_bound ( rng (FAB | ( divset ((T . i),(( len F1) + k)))))) * ( vol ( divset ((T . i),(( len F1) + k))))) by INTEGRA1:def 7;

          

           A267: k in ( Seg ( len S2)) by A258, A263, INTEGRA1:def 7;

          then

           A268: k in ( dom S2) by FINSEQ_1:def 3;

          ( len F1) = ( len S1) by A257, INTEGRA1:def 7;

          then

           A269: ( divset ((T . i),(( len F1) + k))) = ( divset ((T2 . i),k)) by A112, A257, A258, A267;

          

           A270: ( divset ((T2 . i),k)) c= ['c, b'] by A134, A258, A267;

          then ( divset ((T . i),(( len F1) + k))) c= ['a, b'] by A17, A269;

          then (F . (( len F1) + k)) = (( lower_bound ( rng (FCB | ( divset ((T2 . i),k))))) * ( vol ( divset ((T2 . i),k)))) by A266, A269, A270, Th3;

          hence (F . (( len F1) + k)) = (F2 . k) by A258, A268, INTEGRA1:def 7;

        end;

         A271:

        now

          let k be Nat;

          ( len ( lower_volume (FAB,(T . i)))) = ( len S) by INTEGRA1:def 7;

          then

           A272: ( dom ( lower_volume (FAB,(T . i)))) = ( dom S) by FINSEQ_3: 29;

          assume

           A273: k in ( dom F1);

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

          then

           A274: k in ( Seg ( len S1)) by A257, INTEGRA1:def 7;

          then

           A275: k in ( dom S1) by FINSEQ_1:def 3;

          ( len F1) <= ( len F) by A260, NAT_1: 11;

          then ( dom F1) c= ( dom F) by FINSEQ_3: 30;

          then

           A276: (F . k) = (( lower_bound ( rng (FAB | ( divset ((T . i),k))))) * ( vol ( divset ((T . i),k)))) by A273, A272, INTEGRA1:def 7;

          

           A277: ( divset ((T . i),k)) = ( divset ((T1 . i),k)) & ( divset ((T1 . i),k)) c= ['a, c'] by A139, A95, A257, A274;

          then ( divset ((T . i),k)) c= ['a, b'] by A137;

          then (F . k) = (( lower_bound ( rng (FAC | ( divset ((T1 . i),k))))) * ( vol ( divset ((T1 . i),k)))) by A276, A277, Th3;

          hence (F . k) = (F1 . k) by A257, A275, INTEGRA1:def 7;

        end;

        ( dom F) = ( Seg (( len F1) + ( len F2))) by A261, FINSEQ_1:def 3;

        hence thesis by A271, A262, FINSEQ_1:def 7;

      end;

      

       A278: for i be Element of NAT holds ( Sum ( lower_volume (FAB,(T . i)))) = (( Sum ( lower_volume (FAC,(T1 . i)))) + ( Sum ( lower_volume (FCB,(T2 . i)))))

      proof

        let i be Element of NAT ;

        ( lower_volume (FAB,(T . i))) = (( lower_volume (FAC,(T1 . i))) ^ ( lower_volume (FCB,(T2 . i)))) by A256;

        hence thesis by RVSUM_1: 75;

      end;

      now

        let i be Nat;

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

        

        thus (( lower_sum (FAB,T)) . i) = ( lower_sum (FAB,(T . ii))) by INTEGRA2:def 3

        .= (( lower_sum (FAC,(T1 . ii))) + ( Sum ( lower_volume (FCB,(T2 . ii))))) by A278

        .= ((( lower_sum (FAC,T1)) . i) + ( lower_sum (FCB,(T2 . ii)))) by INTEGRA2:def 3

        .= ((( lower_sum (FAC,T1)) . i) + (( lower_sum (FCB,T2)) . i)) by INTEGRA2:def 3;

      end;

      then

       A279: ( lower_sum (FAB,T)) = (( lower_sum (FAC,T1)) + ( lower_sum (FCB,T2))) by SEQ_1: 7;

      

       A280: FAC is Function of ['a, c'], REAL by A2, A137, Lm1, XBOOLE_1: 1;

      then

       A281: FAC is upper_integrable & FAC is lower_integrable by A138, INTEGRA4: 10;

      

       A282: ( upper_sum (FAC,T1)) is convergent & ( lim ( upper_sum (FAC,T1))) = ( upper_integral FAC) by A280, A138, A53, INTEGRA4: 9;

      then

       A283: (( upper_integral FAC) + ( upper_integral FCB)) = ( upper_integral FAB) by A165, A217, A255, SEQ_2: 6;

      

       A284: ( lower_sum (FAC,T1)) is convergent & ( lim ( lower_sum (FAC,T1))) = ( lower_integral FAC) by A280, A138, A53, INTEGRA4: 8;

      (FAB | ['a, b']) is bounded by A4;

      then

       A285: ( lower_integral FAB) = ( lim ( lower_sum (FAB,T))) by A12, A253, A254, INTEGRA4: 8;

      ( lower_sum (FCB,T2)) is convergent & ( lim ( lower_sum (FCB,T2))) = ( lower_integral FCB) by A166, A18, A215, A216, INTEGRA4: 8;

      then

       A286: (( lower_integral FAC) + ( lower_integral FCB)) = ( lower_integral FAB) by A279, A284, A285, SEQ_2: 6;

      ( integral (f,a,b)) = ( integral (f, ['a, b'])) by A1, INTEGRA5:def 4

      .= (( integral FAC) + ( integral FCB)) by A165, A282, A217, A255, SEQ_2: 6;

      hence ( integral (f,a,b)) = (( integral (f,a,c)) + ( integral (f,c,b))) by A58, A57;

      FAB is integrable by A3;

      then

       A287: ( upper_integral FAB) = ( lower_integral FAB);

      

       A288: FCB is upper_integrable & FCB is lower_integrable by A166, A18, INTEGRA4: 10;

      

       A289: ( lower_integral FAC) <= ( upper_integral FAC) by A280, A138, INTEGRA1: 49;

      then ( lower_integral FCB) = ( upper_integral FCB) by A287, A283, A286, A167, Th1;

      then

       A290: FCB is integrable by A288;

      ( lower_integral FAC) = ( upper_integral FAC) by A287, A283, A286, A289, A167, Th1;

      then FAC is integrable by A281;

      hence thesis by A290;

    end;

    theorem :: INTEGRA6:17

    

     Th17: a <= b & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] implies f is_integrable_on ['a, c'] & f is_integrable_on ['c, b'] & ( integral (f,a,b)) = (( integral (f,a,c)) + ( integral (f,c,b)))

    proof

      assume that

       A1: a <= b and

       A2: f is_integrable_on ['a, b'] and

       A3: (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'];

      now

        assume

         A4: b = c;

        then

         A5: ['c, b'] = [.c, b.] by INTEGRA5:def 3;

        thus f is_integrable_on ['a, c'] by A2, A4;

         ['c, b'] = [.( lower_bound ['c, b']), ( upper_bound ['c, b']).] by INTEGRA1: 4;

        then ( lower_bound ['c, b']) = c & ( upper_bound ['c, b']) = b by A5, INTEGRA1: 5;

        then

         A6: ( vol ['c, b']) = 0 by A4;

        then (f || ['c, b']) is integrable by INTEGRA4: 6;

        hence f is_integrable_on ['c, b'];

        ( integral (f,c,b)) = ( integral (f, ['c, b'])) by A5, INTEGRA5: 19;

        then ( integral (f,c,b)) = 0 by A6, INTEGRA4: 6;

        hence ( integral (f,a,b)) = (( integral (f,a,c)) + ( integral (f,c,b))) by A4;

      end;

      hence thesis by A1, A2, A3, Lm2;

    end;

    

     Lm3: for a,b,c be Real st a <= c & c <= b holds c in ['a, b'] & ['a, c'] c= ['a, b'] & ['c, b'] c= ['a, b']

    proof

      let a,b,c be Real;

      assume that

       A1: a <= c and

       A2: c <= b;

      

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

      hence c in ['a, b'] by A1, A2, INTEGRA5:def 3, XXREAL_0: 2;

      

       A4: ['c, b'] = [.c, b.] by A2, INTEGRA5:def 3;

      a <= b by A1, A2, XXREAL_0: 2;

      then

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

       ['a, b'] = [.a, b.] & ['a, c'] = [.a, c.] by A1, A2, INTEGRA5:def 3, XXREAL_0: 2;

      hence thesis by A4, A3, A5, XXREAL_2:def 12;

    end;

    theorem :: INTEGRA6:18

    

     Th18: a <= c & c <= d & d <= b & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) implies f is_integrable_on ['c, d'] & (f | ['c, d']) is bounded & ['c, d'] c= ( dom f)

    proof

      assume that

       A1: a <= c and

       A2: c <= d and

       A3: d <= b and

       A4: f is_integrable_on ['a, b'] and

       A5: (f | ['a, b']) is bounded and

       A6: ['a, b'] c= ( dom f);

      a <= d by A1, A2, XXREAL_0: 2;

      then

       A7: a <= b by A3, XXREAL_0: 2;

      

       A8: c <= b by A2, A3, XXREAL_0: 2;

      then c in ['a, b'] by A1, Lm3;

      then

       A9: f is_integrable_on ['c, b'] by A4, A5, A6, A7, Th17;

      

       A10: d in ['c, b'] by A2, A3, Lm3;

      

       A11: ['c, b'] c= ['a, b'] by A1, A8, Lm3;

      then ['c, b'] c= ( dom f) & (f | ['c, b']) is bounded by A5, A6, RFUNCT_1: 74;

      hence f is_integrable_on ['c, d'] by A8, A10, A9, Th17;

       ['c, d'] c= ['c, b'] by A2, A3, Lm3;

      then

       A12: ['c, d'] c= ['a, b'] by A11;

      hence (f | ['c, d']) is bounded by A5, RFUNCT_1: 74;

      thus thesis by A6, A12;

    end;

    theorem :: INTEGRA6:19

    a <= c & c <= d & d <= b & f is_integrable_on ['a, b'] & g is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & (g | ['a, b']) is bounded & ['a, b'] c= ( dom f) & ['a, b'] c= ( dom g) implies (f + g) is_integrable_on ['c, d'] & ((f + g) | ['c, d']) is bounded

    proof

      assume that

       A1: a <= c and

       A2: c <= d & d <= b and

       A3: f is_integrable_on ['a, b'] & g is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & (g | ['a, b']) is bounded and

       A4: ['a, b'] c= ( dom f) and

       A5: ['a, b'] c= ( dom g);

      

       A6: ['c, d'] c= ['c, b'] by A2, Lm3;

      

       A7: (f | ['c, d']) is bounded & (g | ['c, d']) is bounded by A1, A2, A3, A4, A5, Th18;

      c <= b by A2, XXREAL_0: 2;

      then

       A8: ['c, b'] c= ['a, b'] by A1, Lm3;

      then ['c, b'] c= ( dom f) by A4;

      then

       A9: ['c, d'] c= ( dom f) by A6;

       ['c, b'] c= ( dom g) by A5, A8;

      then

       A10: ['c, d'] c= ( dom g) by A6;

      f is_integrable_on ['c, d'] & g is_integrable_on ['c, d'] by A1, A2, A3, A4, A5, Th18;

      hence (f + g) is_integrable_on ['c, d'] by A7, A9, A10, Th11;

      ((f + g) | ( ['c, d'] /\ ['c, d'])) is bounded by A7, RFUNCT_1: 83;

      hence thesis;

    end;

    

     Lm4: for a,b,c,d be Real, f be PartFunc of REAL , REAL st a <= b & c <= d & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'] holds ( integral (f,a,d)) = (( integral (f,a,c)) + ( integral (f,c,d)))

    proof

      let a,b,c,d be Real, f be PartFunc of REAL , REAL ;

      assume that

       A1: a <= b and

       A2: c <= d and

       A3: f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded and

       A4: ['a, b'] c= ( dom f) and

       A5: c in ['a, b'] and

       A6: d in ['a, b'];

      

       A7: f is_integrable_on ['a, d'] by A1, A3, A4, A6, Th17;

      

       A8: ['a, b'] = [.a, b.] by A1, INTEGRA5:def 3;

      then

       A9: a <= d by A6, XXREAL_1: 1;

      

       A10: d <= b by A6, A8, XXREAL_1: 1;

      then ['a, d'] c= ['a, b'] by A9, Lm3;

      then

       A11: ['a, d'] c= ( dom f) by A4;

      a <= c by A5, A8, XXREAL_1: 1;

      then

       A12: c in ['a, d'] by A2, Lm3;

      (f | ['a, d']) is bounded by A3, A4, A9, A10, Th18;

      hence thesis by A9, A12, A11, A7, Th17;

    end;

    theorem :: INTEGRA6:20

    

     Th20: a <= b & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'] implies ( integral (f,a,d)) = (( integral (f,a,c)) + ( integral (f,c,d)))

    proof

      assume

       A1: a <= b & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'];

      now

        assume

         A2: not c <= d;

        then ( integral (f,a,c)) = (( integral (f,a,d)) + ( integral (f,d,c))) by A1, Lm4;

        then

         A3: ( integral (f,a,d)) = (( integral (f,a,c)) - ( integral (f,d,c)));

        ( integral (f,c,d)) = ( - ( integral (f, ['d, c']))) by A2, INTEGRA5:def 4;

        hence thesis by A2, A3, INTEGRA5:def 4;

      end;

      hence thesis by A1, Lm4;

    end;

    

     Lm5: for a,b,c,d be Real, f be PartFunc of REAL , REAL st a <= b & c <= d & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'] holds ['c, d'] c= ( dom ( abs f)) & ( abs f) is_integrable_on ['c, d'] & (( abs f) | ['c, d']) is bounded & |.( integral (f,c,d)).| <= ( integral (( abs f),c,d))

    proof

      let a,b,c,d be Real, f be PartFunc of REAL , REAL such that

       A1: a <= b and

       A2: c <= d and

       A3: f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) and

       A4: c in ['a, b'] & d in ['a, b'];

       ['a, b'] = [.a, b.] by A1, INTEGRA5:def 3;

      then

       A5: a <= c & d <= b by A4, XXREAL_1: 1;

      then

       A6: (f | ['c, d']) is bounded by A2, A3, Th18;

       ['c, d'] c= ( dom f) & f is_integrable_on ['c, d'] by A2, A3, A5, Th18;

      hence thesis by A2, A6, Th7, Th8, RFUNCT_1: 82, VALUED_1:def 11;

    end;

    theorem :: INTEGRA6:21

    

     Th21: a <= b & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'] implies ['( min (c,d)), ( max (c,d))'] c= ( dom ( abs f)) & ( abs f) is_integrable_on ['( min (c,d)), ( max (c,d))'] & (( abs f) | ['( min (c,d)), ( max (c,d))']) is bounded & |.( integral (f,c,d)).| <= ( integral (( abs f),( min (c,d)),( max (c,d))))

    proof

      assume

       A1: a <= b & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'];

       A2:

      now

        assume

         A3: not c <= d;

        then ( integral (f,c,d)) = ( - ( integral (f, ['d, c']))) by INTEGRA5:def 4;

        then ( integral (f,c,d)) = ( - ( integral (f,d,c))) by A3, INTEGRA5:def 4;

        then

         A4: |.( integral (f,c,d)).| = |.( integral (f,d,c)).| by COMPLEX1: 52;

        d = ( min (c,d)) & c = ( max (c,d)) by A3, XXREAL_0:def 9, XXREAL_0:def 10;

        hence thesis by A1, A3, A4, Lm5;

      end;

      now

        assume

         A5: c <= d;

        then c = ( min (c,d)) & d = ( max (c,d)) by XXREAL_0:def 9, XXREAL_0:def 10;

        hence thesis by A1, A5, Lm5;

      end;

      hence thesis by A2;

    end;

    

     Lm6: a <= b & c <= d & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'] implies ['c, d'] c= ( dom ( abs f)) & ( abs f) is_integrable_on ['c, d'] & (( abs f) | ['c, d']) is bounded & |.( integral (f,c,d)).| <= ( integral (( abs f),c,d))

    proof

      assume that

       A1: a <= b and

       A2: c <= d and

       A3: f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'];

      ( min (c,d)) = c & ( max (c,d)) = d by A2, XXREAL_0:def 9, XXREAL_0:def 10;

      hence thesis by A1, A3, Th21;

    end;

    

     Lm7: a <= b & c <= d & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'] implies |.( integral (f,d,c)).| <= ( integral (( abs f),c,d))

    proof

      assume that

       A1: a <= b and

       A2: c <= d and

       A3: f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] and

       A4: d in ['a, b'];

      

       A5: |.( integral (f,c,d)).| <= ( integral (( abs f),c,d)) & ( integral (f,c,d)) = ( integral (f, ['c, d'])) by A1, A2, A3, A4, Lm6, INTEGRA5:def 4;

      per cases ;

        suppose c = d;

        hence thesis by A1, A3, Lm6;

      end;

        suppose c <> d;

        then c < d by A2, XXREAL_0: 1;

        then ( integral (f,d,c)) = ( - ( integral (f, ['c, d']))) by INTEGRA5:def 4;

        hence thesis by A5, COMPLEX1: 52;

      end;

    end;

    theorem :: INTEGRA6:22

    a <= b & c <= d & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'] implies ['c, d'] c= ( dom ( abs f)) & ( abs f) is_integrable_on ['c, d'] & (( abs f) | ['c, d']) is bounded & |.( integral (f,c,d)).| <= ( integral (( abs f),c,d)) & |.( integral (f,d,c)).| <= ( integral (( abs f),c,d)) by Lm6, Lm7;

    

     Lm8: (a <= b & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'] & for x be Real st x in ['( min (c,d)), ( max (c,d))'] holds |.(f . x).| <= e) implies |.( integral (f,c,d)).| <= (e * |.(d - c).|)

    proof

      set A = ['( min (c,d)), ( max (c,d))'];

      assume that

       A1: a <= b & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'] and

       A2: for x be Real st x in ['( min (c,d)), ( max (c,d))'] holds |.(f . x).| <= e;

      ( rng ( abs f)) c= REAL ;

      then

       A3: ( abs f) is Function of ( dom ( abs f)), REAL by FUNCT_2: 2;

       ['( min (c,d)), ( max (c,d))'] c= ( dom ( abs f)) by A1, Th21;

      then

      reconsider g = (( abs f) || A) as Function of A, REAL by A3, FUNCT_2: 32;

      

       A4: ( vol A) = |.(d - c).| by Th6;

      ( abs f) is_integrable_on A by A1, Th21;

      then

       A5: g is integrable;

      reconsider e as Real;

      consider h be Function of A, REAL such that

       A6: ( rng h) = {e} and

       A7: (h | A) is bounded by INTEGRA4: 5;

       A8:

      now

        let x be Real;

        assume

         A9: x in A;

        then (g . x) = (( abs f) . x) by FUNCT_1: 49;

        then

         A10: (g . x) = |.(f . x).| by VALUED_1: 18;

        (h . x) in {e} by A6, A9, FUNCT_2: 4;

        then (h . x) = e by TARSKI:def 1;

        hence (g . x) <= (h . x) by A2, A9, A10;

      end;

      

       A11: |.( integral (f,c,d)).| <= ( integral (( abs f),( min (c,d)),( max (c,d)))) by A1, Th21;

      ( min (c,d)) <= c & c <= ( max (c,d)) by XXREAL_0: 17, XXREAL_0: 25;

      then ( min (c,d)) <= ( max (c,d)) by XXREAL_0: 2;

      then

       A12: ( integral (( abs f),( min (c,d)),( max (c,d)))) = ( integral (( abs f),A)) by INTEGRA5:def 4;

      (( abs f) | A) is bounded by A1, Th21;

      then

       A13: (g | A) is bounded;

      h is integrable & ( integral h) = (e * ( vol A)) by A6, INTEGRA4: 4;

      then ( integral (( abs f),( min (c,d)),( max (c,d)))) <= (e * |.(d - c).|) by A12, A7, A8, A5, A13, A4, INTEGRA2: 34;

      hence thesis by A11, XXREAL_0: 2;

    end;

    

     Lm9: (a <= b & c <= d & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'] & for x be Real st x in ['c, d'] holds |.(f . x).| <= e) implies |.( integral (f,c,d)).| <= (e * (d - c))

    proof

      assume that

       A1: a <= b and

       A2: c <= d and

       A3: f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] & (d in ['a, b'] & for x be Real st x in ['c, d'] holds |.(f . x).| <= e);

       0 <= (d - c) by A2, XREAL_1: 48;

      then

       A4: |.(d - c).| = (d - c) by ABSVALUE:def 1;

      ( min (c,d)) = c & ( max (c,d)) = d by A2, XXREAL_0:def 9, XXREAL_0:def 10;

      hence thesis by A1, A3, A4, Lm8;

    end;

    

     Lm10: (a <= b & c <= d & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'] & for x be Real st x in ['c, d'] holds |.(f . x).| <= e) implies |.( integral (f,d,c)).| <= (e * (d - c))

    proof

      assume that

       A1: a <= b and

       A2: c <= d and

       A3: f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] and

       A4: d in ['a, b'] and

       A5: for x be Real st x in ['c, d'] holds |.(f . x).| <= e;

      

       A6: |.( integral (f,c,d)).| <= (e * (d - c)) & ( integral (f,c,d)) = ( integral (f, ['c, d'])) by A1, A2, A3, A4, A5, Lm9, INTEGRA5:def 4;

      per cases ;

        suppose c = d;

        hence thesis by A1, A3, A5, Lm9;

      end;

        suppose c <> d;

        then c < d by A2, XXREAL_0: 1;

        then ( integral (f,d,c)) = ( - ( integral (f, ['c, d']))) by INTEGRA5:def 4;

        hence thesis by A6, COMPLEX1: 52;

      end;

    end;

    theorem :: INTEGRA6:23

    (a <= b & c <= d & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'] & for x be Real st x in ['c, d'] holds |.(f . x).| <= e) implies |.( integral (f,c,d)).| <= (e * (d - c)) & |.( integral (f,d,c)).| <= (e * (d - c)) by Lm9, Lm10;

    

     Lm11: for a,b,c,d be Real, f,g be PartFunc of REAL , REAL st a <= b & c <= d & f is_integrable_on ['a, b'] & g is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & (g | ['a, b']) is bounded & ['a, b'] c= ( dom f) & ['a, b'] c= ( dom g) & c in ['a, b'] & d in ['a, b'] holds (f + g) is_integrable_on ['c, d'] & ((f + g) | ['c, d']) is bounded & ( integral ((f + g),c,d)) = (( integral (f,c,d)) + ( integral (g,c,d))) & (f - g) is_integrable_on ['c, d'] & ((f - g) | ['c, d']) is bounded & ( integral ((f - g),c,d)) = (( integral (f,c,d)) - ( integral (g,c,d)))

    proof

      let a,b,c,d be Real, f,g be PartFunc of REAL , REAL ;

      assume that

       A1: a <= b and

       A2: c <= d and

       A3: f is_integrable_on ['a, b'] and

       A4: g is_integrable_on ['a, b'] and

       A5: (f | ['a, b']) is bounded and

       A6: (g | ['a, b']) is bounded and

       A7: ['a, b'] c= ( dom f) and

       A8: ['a, b'] c= ( dom g) and

       A9: c in ['a, b'] & d in ['a, b'];

       ['a, b'] = [.a, b.] by A1, INTEGRA5:def 3;

      then

       A10: a <= c & d <= b by A9, XXREAL_1: 1;

      then

       A11: f is_integrable_on ['c, d'] & ['c, d'] c= ( dom f) by A2, A3, A5, A7, Th18;

      

       A12: g is_integrable_on ['c, d'] & ['c, d'] c= ( dom g) by A2, A4, A6, A8, A10, Th18;

      

       A13: (f | ['c, d']) is bounded & (g | ['c, d']) is bounded by A2, A3, A4, A5, A6, A7, A8, A10, Th18;

      then ((f + g) | ( ['c, d'] /\ ['c, d'])) is bounded by RFUNCT_1: 83;

      hence thesis by A2, A11, A13, A12, Th11, Th12, RFUNCT_1: 84;

    end;

    theorem :: INTEGRA6:24

    

     Th24: a <= b & f is_integrable_on ['a, b'] & g is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & (g | ['a, b']) is bounded & ['a, b'] c= ( dom f) & ['a, b'] c= ( dom g) & c in ['a, b'] & d in ['a, b'] implies ( integral ((f + g),c,d)) = (( integral (f,c,d)) + ( integral (g,c,d))) & ( integral ((f - g),c,d)) = (( integral (f,c,d)) - ( integral (g,c,d)))

    proof

      assume

       A1: a <= b & f is_integrable_on ['a, b'] & g is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & (g | ['a, b']) is bounded & ['a, b'] c= ( dom f) & ['a, b'] c= ( dom g) & c in ['a, b'] & d in ['a, b'];

      now

        assume

         A2: not c <= d;

        then

         A3: ( integral (f,c,d)) = ( - ( integral (f, ['d, c']))) by INTEGRA5:def 4;

        

         A4: ( integral (g,c,d)) = ( - ( integral (g, ['d, c']))) by A2, INTEGRA5:def 4;

        ( integral ((f + g),c,d)) = ( - ( integral ((f + g), ['d, c']))) by A2, INTEGRA5:def 4;

        

        hence ( integral ((f + g),c,d)) = ( - ( integral ((f + g),d,c))) by A2, INTEGRA5:def 4

        .= ( - (( integral (f,d,c)) + ( integral (g,d,c)))) by A1, A2, Lm11

        .= (( - ( integral (f,d,c))) - ( integral (g,d,c)))

        .= (( integral (f,c,d)) - ( integral (g,d,c))) by A2, A3, INTEGRA5:def 4

        .= (( integral (f,c,d)) + ( integral (g,c,d))) by A2, A4, INTEGRA5:def 4;

        ( integral ((f - g),c,d)) = ( - ( integral ((f - g), ['d, c']))) by A2, INTEGRA5:def 4;

        

        hence ( integral ((f - g),c,d)) = ( - ( integral ((f - g),d,c))) by A2, INTEGRA5:def 4

        .= ( - (( integral (f,d,c)) - ( integral (g,d,c)))) by A1, A2, Lm11

        .= ( - (( integral (f,d,c)) + ( integral (g,c,d)))) by A2, A4, INTEGRA5:def 4

        .= (( - ( integral (f,d,c))) - ( integral (g,c,d)))

        .= (( integral (f,c,d)) - ( integral (g,c,d))) by A2, A3, INTEGRA5:def 4;

      end;

      hence thesis by A1, Lm11;

    end;

    

     Lm12: for a,b,c,d,e be Real, f be PartFunc of REAL , REAL st a <= b & c <= d & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'] holds ( integral ((e (#) f),c,d)) = (e * ( integral (f,c,d)))

    proof

      let a,b,c,d,e be Real, f be PartFunc of REAL , REAL ;

      assume that

       A1: a <= b and

       A2: c <= d and

       A3: f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) and

       A4: c in ['a, b'] & d in ['a, b'];

       ['a, b'] = [.a, b.] by A1, INTEGRA5:def 3;

      then

       A5: a <= c & d <= b by A4, XXREAL_1: 1;

      then

       A6: ['c, d'] c= ( dom f) by A2, A3, Th18;

      f is_integrable_on ['c, d'] & (f | ['c, d']) is bounded by A2, A3, A5, Th18;

      hence thesis by A2, A6, Th10;

    end;

    theorem :: INTEGRA6:25

    a <= b & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'] implies ( integral ((e (#) f),c,d)) = (e * ( integral (f,c,d)))

    proof

      assume

       A1: a <= b & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'];

      now

        assume

         A2: not c <= d;

        then

         A3: ( integral (f,c,d)) = ( - ( integral (f, ['d, c']))) by INTEGRA5:def 4;

        

        thus ( integral ((e (#) f),c,d)) = ( - ( integral ((e (#) f), ['d, c']))) by A2, INTEGRA5:def 4

        .= ( - ( integral ((e (#) f),d,c))) by A2, INTEGRA5:def 4

        .= ( - (e * ( integral (f,d,c)))) by A1, A2, Lm12

        .= (e * ( - ( integral (f,d,c))))

        .= (e * ( integral (f,c,d))) by A2, A3, INTEGRA5:def 4;

      end;

      hence thesis by A1, Lm12;

    end;

    theorem :: INTEGRA6:26

    

     Th26: (a <= b & ['a, b'] c= ( dom f) & for x be Real st x in ['a, b'] holds (f . x) = e) implies f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ( integral (f,a,b)) = (e * (b - a))

    proof

      assume that

       A1: a <= b and

       A2: ['a, b'] c= ( dom f) and

       A3: for x be Real st x in ['a, b'] holds (f . x) = e;

      ( rng f) c= REAL ;

      then f is Function of ( dom f), REAL by FUNCT_2: 2;

      then

      reconsider g = (f || ['a, b']) as Function of ['a, b'], REAL by A2, FUNCT_2: 32;

      reconsider e1 = e as Real;

      consider h be Function of ['a, b'], REAL such that

       A4: ( rng h) = {e1} and

       A5: (h | ['a, b']) is bounded by INTEGRA4: 5;

      ( integral h) = (e1 * ( vol ['a, b'])) by A4, INTEGRA4: 4;

      then

       A6: ( integral h) = (e * (b - a)) by A1, Th5;

      

       A7: for x be object st x in ['a, b'] holds (g . x) = (h . x)

      proof

        let x0 be object;

        assume

         A8: x0 in ['a, b'];

        then

        reconsider x = x0 as Real;

        (g . x0) = (f . x) by A8, FUNCT_1: 49;

        then

         A9: (g . x0) = e by A3, A8;

        (h . x) in {e1} by A4, A8, FUNCT_2: 4;

        hence thesis by A9, TARSKI:def 1;

      end;

      then

       A10: h = g by FUNCT_2: 12;

      h is integrable by A4, INTEGRA4: 4;

      hence f is_integrable_on ['a, b'] by A10;

      thus (f | ['a, b']) is bounded by A5, A10;

      ( integral (f,a,b)) = ( integral (f, ['a, b'])) by A1, INTEGRA5:def 4;

      hence thesis by A7, A6, FUNCT_2: 12;

    end;

    theorem :: INTEGRA6:27

    

     Th27: a <= b & (for x be Real st x in ['a, b'] holds (f . x) = e) & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'] implies ( integral (f,c,d)) = (e * (d - c))

    proof

      assume that

       A1: a <= b and

       A2: for x be Real st x in ['a, b'] holds (f . x) = e and

       A3: ['a, b'] c= ( dom f) and

       A4: c in ['a, b'] and

       A5: d in ['a, b'];

      

       A6: f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded by A1, A2, A3, Th26;

      

       A7: ['a, b'] = [.a, b.] by A1, INTEGRA5:def 3;

      then

       A8: c <= b by A4, XXREAL_1: 1;

      

       A9: a <= c by A4, A7, XXREAL_1: 1;

      then

       A10: ['c, b'] c= ['a, b'] by A8, Lm3;

      

       A11: d <= b by A5, A7, XXREAL_1: 1;

      

       A12: a <= d by A5, A7, XXREAL_1: 1;

      

       A13: ['a, c'] c= ['a, b'] by A9, A8, Lm3;

      per cases ;

        suppose

         A14: c <= d;

        then ['c, d'] c= ['c, b'] by A11, Lm3;

        then ['c, d'] c= ['a, b'] by A10;

        then

         A15: for x be Real st x in ['c, d'] holds (f . x) = e by A2;

         ['c, d'] c= ( dom f) by A3, A9, A11, A6, A14, Th18;

        hence thesis by A14, A15, Th26;

      end;

        suppose

         A16: not c <= d;

        then ['d, c'] c= ['a, c'] by A12, Lm3;

        then ['d, c'] c= ['a, b'] by A13;

        then

         A17: for x be Real st x in ['d, c'] holds (f . x) = e by A2;

        ( integral (f,c,d)) = ( - ( integral (f, ['d, c']))) by A16, INTEGRA5:def 4;

        then

         A18: ( integral (f,c,d)) = ( - ( integral (f,d,c))) by A16, INTEGRA5:def 4;

         ['d, c'] c= ( dom f) by A3, A12, A8, A6, A16, Th18;

        then ( integral (f,d,c)) = (e * (c - d)) by A16, A17, Th26;

        hence thesis by A18;

      end;

    end;

    begin

    theorem :: INTEGRA6:28

    

     Th28: for x0 be Real, F be PartFunc of REAL , REAL st a <= b & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & ].a, b.[ c= ( dom F) & (for x be Real st x in ].a, b.[ holds (F . x) = ( integral (f,a,x))) & x0 in ].a, b.[ & f is_continuous_in x0 holds F is_differentiable_in x0 & ( diff (F,x0)) = (f . x0)

    proof

      deffunc F2( object) = 0 ;

      let x0 be Real, F be PartFunc of REAL , REAL ;

      assume that

       A1: a <= b and

       A2: f is_integrable_on ['a, b'] and

       A3: (f | ['a, b']) is bounded and

       A4: ['a, b'] c= ( dom f) and

       A5: ].a, b.[ c= ( dom F) and

       A6: for x be Real st x in ].a, b.[ holds (F . x) = ( integral (f,a,x)) and

       A7: x0 in ].a, b.[ and

       A8: f is_continuous_in x0;

      defpred C1[ object] means (x0 + ( In ($1, REAL ))) in ].a, b.[;

      deffunc F0( Real) = ( In (((f . x0) * $1), REAL ));

      consider L be Function of REAL , REAL such that

       A9: for h be Element of REAL holds (L . h) = F0(h) from FUNCT_2:sch 4;

      

       A10: for h be Real holds (L . h) = ((f . x0) * h)

      proof

        let h be Real;

        reconsider h as Element of REAL by XREAL_0:def 1;

        (L . h) = F0(h) by A9;

        hence thesis;

      end;

      reconsider L as PartFunc of REAL , REAL ;

      deffunc F1( object) = (((F . (x0 + ( In ($1, REAL )))) - (F . x0)) - (L . ( In ($1, REAL ))));

      reconsider L as LinearFunc by A10, FDIFF_1:def 3;

      consider R be Function such that

       A11: ( dom R) = REAL & for x be object st x in REAL holds ( C1[x] implies (R . x) = F1(x)) & ( not C1[x] implies (R . x) = F2(x)) from PARTFUN1:sch 1;

      ( rng R) c= REAL

      proof

        let y be object;

        assume y in ( rng R);

        then

        consider x be object such that

         A12: x in ( dom R) and

         A13: y = (R . x) by FUNCT_1:def 3;

        

         A14: not C1[x] implies (R . x) = F2(x) by A11, A12;

         C1[x] implies (R . x) = F1(x) by A11, A12;

        hence thesis by A13, A14, XREAL_0:def 1;

      end;

      then

      reconsider R as PartFunc of REAL , REAL by A11, RELSET_1: 4;

      

       A15: R is total by A11, PARTFUN1:def 2;

      

       A16: ['a, b'] = [.a, b.] by A1, INTEGRA5:def 3;

      

       A17: for h be 0 -convergent non-zero Real_Sequence holds ((h " ) (#) (R /* h)) is convergent & ( lim ((h " ) (#) (R /* h))) = 0

      proof

        let h be 0 -convergent non-zero Real_Sequence;

        

         A18: for e be Real st 0 < e holds ex n be Nat st for m be Nat st n <= m holds |.((((h " ) (#) (R /* h)) . m) - 0 ).| < e

        proof

          reconsider fx0 = (f . x0) as Element of REAL by XREAL_0:def 1;

          set g = ( REAL --> fx0);

          let e0 be Real;

          set e = (e0 / 2);

          

           A19: h is convergent & ( lim h) = 0 ;

          assume

           A20: 0 < e0;

          then 0 < e by XREAL_1: 215;

          then

          consider p be Real such that

           A21: 0 < p and

           A22: for t be Real st t in ( dom f) & |.(t - x0).| < p holds |.((f . t) - (f . x0)).| < e by A8, FCONT_1: 3;

          

           A23: 0 < (p / 2) by A21, XREAL_1: 215;

          

           A24: (p / 2) < p by A21, XREAL_1: 216;

          consider N be Neighbourhood of x0 such that

           A25: N c= ].a, b.[ by A7, RCOMP_1: 18;

          consider q be Real such that

           A26: 0 < q and

           A27: N = ].(x0 - q), (x0 + q).[ by RCOMP_1:def 6;

          

           A28: (q / 2) < q by A26, XREAL_1: 216;

          set r = ( min ((p / 2),(q / 2)));

           0 < (q / 2) by A26, XREAL_1: 215;

          then 0 < r by A23, XXREAL_0: 15;

          then

          consider n be Nat such that

           A29: for m be Nat st n <= m holds |.((h . m) - 0 ).| < r by A19, SEQ_2:def 7;

          take n;

          let m be Nat;

          r <= (q / 2) by XXREAL_0: 17;

          then

           A30: ].(x0 - r), (x0 + r).[ c= ].(x0 - q), (x0 + q).[ by A28, Th2, XXREAL_0: 2;

          assume n <= m;

          then

           A31: |.((h . m) - 0 ).| < r by A29;

          then |.((x0 + (h . m)) - x0).| < r;

          then (x0 + (h . m)) in ].(x0 - r), (x0 + r).[ by RCOMP_1: 1;

          then

           A32: (x0 + (h . m)) in ].(x0 - q), (x0 + q).[ by A30;

          then

           A33: (x0 + (h . m)) in ].a, b.[ by A25, A27;

          then (x0 + ( In ((h . m), REAL ))) in ].a, b.[;

          then (R . (h . m)) = (((F . (x0 + ( In ((h . m), REAL )))) - (F . x0)) - (L . ( In ((h . m), REAL )))) by A11;

          then (R . (h . m)) = (((F . (x0 + (h . m))) - (F . x0)) - (L . ( In ((h . m), REAL ))));

          then (R . (h . m)) = (((F . (x0 + (h . m))) - (F . x0)) - (L . (h . m)));

          then

           A34: (R . (h . m)) = (((F . (x0 + (h . m))) - (F . x0)) - ((f . x0) * (h . m))) by A10;

          (F . (x0 + (h . m))) = ( integral (f,a,(x0 + (h . m)))) by A6, A25, A27, A32;

          then

           A35: (R . (h . m)) = ((( integral (f,a,(x0 + (h . m)))) - ( integral (f,a,x0))) - ((f . x0) * (h . m))) by A6, A7, A34;

          

           A36: ( dom g) = REAL by FUNCT_2:def 1;

          then ( ['a, b'] /\ ['a, b']) c= (( dom f) /\ ( dom g)) by A4, XBOOLE_1: 27;

          then

           A37: ['a, b'] c= ( dom (f - g)) by VALUED_1: 12;

          

           A38: ].a, b.[ c= [.a, b.] by XXREAL_1: 25;

          then

           A39: ( integral (f,a,(x0 + (h . m)))) = (( integral (f,a,x0)) + ( integral (f,x0,(x0 + (h . m))))) by A1, A2, A3, A4, A7, A16, A33, Th20;

          

           A40: r <= (p / 2) by XXREAL_0: 17;

          

           A41: for x be Real st x in ['( min (x0,(x0 + (h . m)))), ( max (x0,(x0 + (h . m))))'] holds |.((f - g) . x).| <= e

          proof

            let x be Real;

            reconsider x1 = x as Real;

            

             A42: ( min (x0,(x0 + (h . m)))) <= x0 & x0 <= ( max (x0,(x0 + (h . m)))) by XXREAL_0: 17, XXREAL_0: 25;

            assume x in ['( min (x0,(x0 + (h . m)))), ( max (x0,(x0 + (h . m))))'];

            then

             A43: x in [.( min (x0,(x0 + (h . m)))), ( max (x0,(x0 + (h . m)))).] by A42, INTEGRA5:def 3, XXREAL_0: 2;

             |.(x - x0).| <= |.(h . m).|

            proof

              per cases ;

                suppose x0 <= (x0 + (h . m));

                then x0 = ( min (x0,(x0 + (h . m)))) & (x0 + (h . m)) = ( max (x0,(x0 + (h . m)))) by XXREAL_0:def 9, XXREAL_0:def 10;

                then x in { z where z be Real : x0 <= z & z <= (x0 + (h . m)) } by A43, RCOMP_1:def 1;

                then

                 A44: ex z be Real st x = z & x0 <= z & z <= (x0 + (h . m));

                then 0 <= (x - x0) by XREAL_1: 48;

                then

                 A45: |.(x - x0).| = (x - x0) by ABSVALUE:def 1;

                

                 A46: (x - x0) <= ((x0 + (h . m)) - x0) by A44, XREAL_1: 9;

                then 0 <= (h . m) by A44, XREAL_1: 48;

                hence thesis by A46, A45, ABSVALUE:def 1;

              end;

                suppose

                 A47: not x0 <= (x0 + (h . m));

                then x0 = ( max (x0,(x0 + (h . m)))) & (x0 + (h . m)) = ( min (x0,(x0 + (h . m)))) by XXREAL_0:def 9, XXREAL_0:def 10;

                then x in { z where z be Real : (x0 + (h . m)) <= z & z <= x0 } by A43, RCOMP_1:def 1;

                then

                 A48: ex z be Real st x = z & (x0 + (h . m)) <= z & z <= x0;

                then

                 A49: ((x0 + (h . m)) - x0) <= (x - x0) by XREAL_1: 9;

                per cases ;

                  suppose

                   A50: (x - x0) <> 0 ;

                  ((x0 + (h . m)) - x0) < (x0 - x0) by A47, XREAL_1: 14;

                  then

                   A51: |.(h . m).| = ( - (h . m)) by ABSVALUE:def 1;

                  (x - x0) < 0 by A48, A50, XREAL_1: 47;

                  then |.(x - x0).| = ( - (x - x0)) by ABSVALUE:def 1;

                  hence thesis by A49, A51, XREAL_1: 24;

                end;

                  suppose (x - x0) = 0 ;

                  then |.(x - x0).| = 0 by ABSVALUE:def 1;

                  hence thesis by COMPLEX1: 46;

                end;

              end;

            end;

            then

             A52: |.(x - x0).| < r by A31, XXREAL_0: 2;

            then x in ].(x0 - r), (x0 + r).[ by RCOMP_1: 1;

            then x in ].(x0 - q), (x0 + q).[ by A30;

            then x in ].a, b.[ by A25, A27;

            then

             A53: x in [.a, b.] by A38;

            

             A54: x1 in REAL by XREAL_0:def 1;

             |.(x - x0).| < (p / 2) by A40, A52, XXREAL_0: 2;

            then |.(x - x0).| < p by A24, XXREAL_0: 2;

            then |.((f . x) - (f . x0)).| <= e by A4, A16, A22, A53;

            then |.((f . x1) - (g . x1)).| <= e by FUNCOP_1: 7, A54;

            hence thesis by A16, A37, A53, VALUED_1: 13;

          end;

          

           A55: for x be Real st x in ['a, b'] holds (g . x) = (f . x0) by FUNCOP_1: 7;

          then

           A56: (g | ['a, b']) is bounded by A1, A36, Th26;

          then

           A57: ((f - g) | ( ['a, b'] /\ ['a, b'])) is bounded by A3, RFUNCT_1: 84;

          

           A58: m in NAT by ORDINAL1:def 12;

          ( rng h) c= ( dom R) by A11;

          then ((R . (h . m)) / (h . m)) = (((R /* h) . m) / (h . m)) by FUNCT_2: 108, A58;

          then ((R . (h . m)) / (h . m)) = (((R /* h) . m) * ((h " ) . m)) by VALUED_1: 10;

          then

           A59: ((R . (h . m)) / (h . m)) = (((h " ) (#) (R /* h)) . m) by SEQ_1: 8;

          (h . m) <> 0 by SEQ_1: 4, A58;

          then

           A60: 0 < |.(h . m).| by COMPLEX1: 47;

          

           A61: g is_integrable_on ['a, b'] by A1, A36, A55, Th26;

          then (f - g) is_integrable_on ['a, b'] by A2, A3, A4, A36, A56, Th11;

          then

           A62: |.( integral ((f - g),x0,(x0 + (h . m)))).| <= (e * |.((x0 + (h . m)) - x0).|) by A1, A7, A16, A38, A33, A57, A37, A41, Lm8;

          ( integral (g,x0,(x0 + (h . m)))) = ((f . x0) * ((x0 + (h . m)) - x0)) by A1, A7, A16, A38, A33, A36, A55, Th27;

          then (R . (h . m)) = ( integral ((f - g),x0,(x0 + (h . m)))) by A1, A2, A3, A4, A7, A16, A38, A33, A35, A36, A61, A56, A39, Th24;

          then |.((R . (h . m)) / (h . m)).| = ( |.(R . (h . m)).| / |.(h . m).|) & ( |.(R . (h . m)).| / |.(h . m).|) <= ((e * |.(h . m).|) / |.(h . m).|) by A62, A60, COMPLEX1: 67, XREAL_1: 72;

          then

           A63: |.((R . (h . m)) / (h . m)).| <= e by A60, XCMPLX_1: 89;

          e < e0 by A20, XREAL_1: 216;

          hence thesis by A63, A59, XXREAL_0: 2;

        end;

        hence ((h " ) (#) (R /* h)) is convergent by SEQ_2:def 6;

        hence thesis by A18, SEQ_2:def 7;

      end;

      consider N be Neighbourhood of x0 such that

       A64: N c= ].a, b.[ by A7, RCOMP_1: 18;

      reconsider R as RestFunc by A15, A17, FDIFF_1:def 2;

      

       A65: for x be Real st x in N holds ((F . x) - (F . x0)) = ((L . (x - x0)) + (R . (x - x0)))

      proof

        let x be Real;

        assume x in N;

        then

         A66: (x0 + (x - x0)) in N;

        reconsider x as Real;

        

         A67: (x0 + (x - x0)) in N by A66;

         C1[(x - x0)] by A67, A64;

        then (R . (x - x0)) = F1(-) by A11;

        hence thesis;

      end;

      

       A68: N c= ( dom F) by A5, A64;

      hence

       A69: F is_differentiable_in x0 by A65, FDIFF_1:def 4;

      (L . 1) = ((f . x0) * 1) by A10;

      hence thesis by A68, A65, A69, FDIFF_1:def 5;

    end;

    

     Lm13: for a,b be Real, f be PartFunc of REAL , REAL holds ex F be PartFunc of REAL , REAL st ].a, b.[ c= ( dom F) & for x be Real st x in ].a, b.[ holds (F . x) = ( integral (f,a,x))

    proof

      deffunc G( Real) = 0 ;

      let a,b be Real;

      let f be PartFunc of REAL , REAL ;

      defpred C[ set] means $1 in ].a, b.[;

      deffunc F( Real) = ( integral (f,a,$1));

      consider F be Function such that

       A1: ( dom F) = REAL & for x be Element of REAL holds ( C[x] implies (F . x) = F(x)) & ( not C[x] implies (F . x) = G(x)) from PARTFUN1:sch 4;

      now

        let y be object;

        assume y in ( rng F);

        then

        consider x be object such that

         A2: x in ( dom F) and

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

        reconsider x as Element of REAL by A1, A2;

         A4:

        now

          assume not x in ].a, b.[;

          then (F . x) = ( In ( 0 , REAL )) by A1;

          hence y in REAL by A3;

        end;

        now

          assume x in ].a, b.[;

          then (F . x) = ( integral (f,a,x)) by A1;

          hence y in REAL by A3, XREAL_0:def 1;

        end;

        hence y in REAL by A4;

      end;

      then ( rng F) c= REAL ;

      then

      reconsider F as PartFunc of REAL , REAL by A1, RELSET_1: 4;

      take F;

      thus thesis by A1;

    end;

    theorem :: INTEGRA6:29

    for x0 be Real st a <= b & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & x0 in ].a, b.[ & f is_continuous_in x0 holds ex F be PartFunc of REAL , REAL st ].a, b.[ c= ( dom F) & (for x be Real st x in ].a, b.[ holds (F . x) = ( integral (f,a,x))) & F is_differentiable_in x0 & ( diff (F,x0)) = (f . x0)

    proof

      let x0 be Real;

      consider F be PartFunc of REAL , REAL such that

       A1: ].a, b.[ c= ( dom F) & for x be Real st x in ].a, b.[ holds (F . x) = ( integral (f,a,x)) by Lm13;

      assume a <= b & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & x0 in ].a, b.[ & f is_continuous_in x0;

      then F is_differentiable_in x0 & ( diff (F,x0)) = (f . x0) by A1, Th28;

      hence thesis by A1;

    end;