integra5.miz



    begin

    reserve i,k,n,m for Element of NAT ;

    reserve a,b,r,r1,r2,s,x,x1,x2 for Real;

    reserve A for non empty closed_interval Subset of REAL ;

    reserve X for set;

    theorem :: INTEGRA5:1

    

     Th1: for F,F1,F2 be FinSequence of REAL , r1, r2 st (F1 = ( <*r1*> ^ F) or F1 = (F ^ <*r1*>)) & (F2 = ( <*r2*> ^ F) or F2 = (F ^ <*r2*>)) holds ( Sum (F1 - F2)) = (r1 - r2)

    proof

      let F,F1,F2 be FinSequence of REAL ;

      let r1, r2;

      assume that

       A1: F1 = ( <*r1*> ^ F) or F1 = (F ^ <*r1*>) and

       A2: F2 = ( <*r2*> ^ F) or F2 = (F ^ <*r2*>);

      ( len F1) = (( len F) + ( len <*r1*>)) by A1, FINSEQ_1: 22;

      then

       A3: ( len F1) = (( len F) + 1) by FINSEQ_1: 39;

      ( len F2) = (( len <*r2*>) + ( len F)) by A2, FINSEQ_1: 22;

      then

       A4: ( len F2) = (1 + ( len F)) by FINSEQ_1: 39;

      (F1 - F2) = ( diffreal .: (F1,F2)) by RVSUM_1:def 6;

      then

       A5: ( len F1) = ( len (F1 - F2)) by A3, A4, FINSEQ_2: 72;

      for k st k in ( dom F1) holds ((F1 - F2) . k) = ((F1 /. k) - (F2 /. k))

      proof

        let k;

        assume

         A6: k in ( dom F1);

        then

         A7: (F1 . k) = (F1 /. k) by PARTFUN1:def 6;

        

         A8: k in ( Seg ( len F1)) by A6, FINSEQ_1:def 3;

        then k in ( dom F2) by A3, A4, FINSEQ_1:def 3;

        then

         A9: (F2 . k) = (F2 /. k) by PARTFUN1:def 6;

        k in ( dom (F1 - F2)) by A5, A8, FINSEQ_1:def 3;

        hence thesis by A7, A9, VALUED_1: 13;

      end;

      then

       A10: ( Sum (F1 - F2)) = (( Sum F1) - ( Sum F2)) by A3, A4, A5, INTEGRA1: 22;

      ( Sum F1) = (r1 + ( Sum F)) & ( Sum F2) = (( Sum F) + r2) by A1, A2, RVSUM_1: 74, RVSUM_1: 76;

      hence thesis by A10;

    end;

    theorem :: INTEGRA5:2

    

     Th2: for F1,F2 be FinSequence of REAL st ( len F1) = ( len F2) holds ( len (F1 + F2)) = ( len F1) & ( len (F1 - F2)) = ( len F1) & ( Sum (F1 + F2)) = (( Sum F1) + ( Sum F2)) & ( Sum (F1 - F2)) = (( Sum F1) - ( Sum F2))

    proof

      let F1,F2 be FinSequence of REAL ;

      assume

       A1: ( len F1) = ( len F2);

      (F1 + F2) = ( addreal .: (F1,F2)) by RVSUM_1:def 4;

      hence

       A2: ( len F1) = ( len (F1 + F2)) by A1, FINSEQ_2: 72;

      (F1 - F2) = ( diffreal .: (F1,F2)) by RVSUM_1:def 6;

      hence

       A3: ( len F1) = ( len (F1 - F2)) by A1, FINSEQ_2: 72;

      for k st k in ( dom F1) holds ((F1 + F2) . k) = ((F1 /. k) + (F2 /. k))

      proof

        let k;

        assume

         A4: k in ( dom F1);

        then

         A5: (F1 . k) = (F1 /. k) by PARTFUN1:def 6;

        

         A6: k in ( Seg ( len F1)) by A4, FINSEQ_1:def 3;

        then k in ( dom F2) by A1, FINSEQ_1:def 3;

        then

         A7: (F2 . k) = (F2 /. k) by PARTFUN1:def 6;

        k in ( dom (F1 + F2)) by A2, A6, FINSEQ_1:def 3;

        hence thesis by A5, A7, VALUED_1:def 1;

      end;

      hence ( Sum (F1 + F2)) = (( Sum F1) + ( Sum F2)) by A1, A2, INTEGRA1: 21;

      for k st k in ( dom F1) holds ((F1 - F2) . k) = ((F1 /. k) - (F2 /. k))

      proof

        let k;

        assume

         A8: k in ( dom F1);

        then

         A9: (F1 . k) = (F1 /. k) by PARTFUN1:def 6;

        

         A10: k in ( Seg ( len F1)) by A8, FINSEQ_1:def 3;

        then k in ( dom F2) by A1, FINSEQ_1:def 3;

        then

         A11: (F2 . k) = (F2 /. k) by PARTFUN1:def 6;

        k in ( dom (F1 - F2)) by A3, A10, FINSEQ_1:def 3;

        hence thesis by A9, A11, VALUED_1: 13;

      end;

      hence thesis by A1, A3, INTEGRA1: 22;

    end;

    theorem :: INTEGRA5:3

    

     Th3: for F1,F2 be FinSequence of REAL st ( len F1) = ( len F2) & (for i st i in ( dom F1) holds (F1 . i) <= (F2 . i)) holds ( Sum F1) <= ( Sum F2)

    proof

      let F1,F2 be FinSequence of REAL ;

      assume that

       A1: ( len F1) = ( len F2) and

       A2: for i st i in ( dom F1) holds (F1 . i) <= (F2 . i);

      reconsider R1 = F1 as Element of (( len F1) -tuples_on REAL ) by FINSEQ_2: 92;

      reconsider R2 = F2 as Element of (( len F1) -tuples_on REAL ) by A1, FINSEQ_2: 92;

      for i be Nat st i in ( Seg ( len F1)) holds (R1 . i) <= (R2 . i)

      proof

        let i be Nat;

        assume i in ( Seg ( len F1));

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

        hence thesis by A2;

      end;

      hence thesis by RVSUM_1: 82;

    end;

    begin

    notation

      let f be PartFunc of REAL , REAL ;

      let C be non empty Subset of REAL ;

      synonym f || C for f | C;

    end

    definition

      let f be PartFunc of REAL , REAL ;

      let C be non empty Subset of REAL ;

      :: original: ||

      redefine

      func f || C -> PartFunc of C, REAL ;

      correctness by PARTFUN1: 10;

    end

    theorem :: INTEGRA5:4

    

     Th4: for f,g be PartFunc of REAL , REAL , C be non empty Subset of REAL holds ((f || C) (#) (g || C)) = ((f (#) g) || C)

    proof

      let f,g be PartFunc of REAL , REAL ;

      let C be non empty Subset of REAL ;

      

       A1: ( dom ((f (#) g) || C)) = (( dom (f (#) g)) /\ C) by RELAT_1: 61

      .= ((( dom f) /\ ( dom g)) /\ C) by VALUED_1:def 4;

      

       A2: ( dom ((f || C) (#) (g || C))) = (( dom (f | C)) /\ ( dom (g || C))) by VALUED_1:def 4

      .= ((( dom f) /\ C) /\ ( dom (g | C))) by RELAT_1: 61

      .= ((( dom f) /\ C) /\ (( dom g) /\ C)) by RELAT_1: 61

      .= (((( dom f) /\ C) /\ C) /\ ( dom g)) by XBOOLE_1: 16

      .= ((( dom f) /\ (C /\ C)) /\ ( dom g)) by XBOOLE_1: 16

      .= ((( dom f) /\ C) /\ ( dom g));

      then

       A3: ( dom ((f || C) (#) (g || C))) = ( dom ((f (#) g) || C)) by A1, XBOOLE_1: 16;

      for c be Element of C st c in ( dom ((f || C) (#) (g || C))) holds (((f || C) (#) (g || C)) . c) = (((f (#) g) || C) . c)

      proof

        let c be Element of C;

        

         A4: (((f || C) (#) (g || C)) . c) = (((f | C) . c) * ((g | C) . c)) by VALUED_1: 5;

        assume

         A5: c in ( dom ((f || C) (#) (g || C)));

        then

         A6: c in (( dom (f || C)) /\ ( dom (g || C))) by VALUED_1:def 4;

        then

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

        

         A8: c in ( dom (g || C)) by A6, XBOOLE_0:def 4;

        (((f (#) g) || C) . c) = ((f (#) g) . c) by A3, A5, FUNCT_1: 47

        .= ((f . c) * (g . c)) by VALUED_1: 5

        .= (((f | C) . c) * (g . c)) by A7, FUNCT_1: 47;

        hence thesis by A8, A4, FUNCT_1: 47;

      end;

      hence thesis by A2, A1, PARTFUN1: 5, XBOOLE_1: 16;

    end;

    theorem :: INTEGRA5:5

    

     Th5: for f,g be PartFunc of REAL , REAL , C be non empty Subset of REAL holds ((f + g) || C) = ((f || C) + (g || C))

    proof

      let f,g be PartFunc of REAL , REAL ;

      let C be non empty Subset of REAL ;

      

       A1: ( dom ((f || C) + (g || C))) = (( dom (f | C)) /\ ( dom (g || C))) by VALUED_1:def 1

      .= ((( dom f) /\ C) /\ ( dom (g | C))) by RELAT_1: 61

      .= ((( dom f) /\ C) /\ (( dom g) /\ C)) by RELAT_1: 61

      .= (( dom f) /\ (C /\ (( dom g) /\ C))) by XBOOLE_1: 16

      .= (( dom f) /\ (( dom g) /\ (C /\ C))) by XBOOLE_1: 16

      .= (( dom f) /\ (( dom g) /\ C));

      

       A2: ( dom ((f + g) || C)) = (( dom (f + g)) /\ C) by RELAT_1: 61

      .= ((( dom f) /\ ( dom g)) /\ C) by VALUED_1:def 1;

      then

       A3: ( dom ((f + g) || C)) = ( dom ((f || C) + (g || C))) by A1, XBOOLE_1: 16;

      for c be Element of C st c in ( dom ((f + g) || C)) holds (((f + g) || C) . c) = (((f || C) + (g || C)) . c)

      proof

        let c be Element of C;

        assume

         A4: c in ( dom ((f + g) || C));

        then c in (( dom (f + g)) /\ C) by RELAT_1: 61;

        then

         A5: c in ( dom (f + g)) by XBOOLE_0:def 4;

        

         A6: c in (( dom (f || C)) /\ ( dom (g || C))) by A3, A4, VALUED_1:def 1;

        then

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

        

         A8: (((f + g) || C) . c) = ((f + g) . c) by A4, FUNCT_1: 47

        .= ((f . c) + (g . c)) by A5, VALUED_1:def 1;

        

         A9: c in ( dom (g || C)) by A6, XBOOLE_0:def 4;

        (((f || C) + (g || C)) . c) = (((f | C) . c) + ((g || C) . c)) by A3, A4, VALUED_1:def 1

        .= ((f . c) + ((g | C) . c)) by A7, FUNCT_1: 47;

        hence thesis by A8, A9, FUNCT_1: 47;

      end;

      hence thesis by A2, A1, PARTFUN1: 5, XBOOLE_1: 16;

    end;

    definition

      let A be non empty closed_interval Subset of REAL ;

      let f be PartFunc of REAL , REAL ;

      :: INTEGRA5:def1

      pred f is_integrable_on A means (f || A) is integrable;

    end

    definition

      let A be non empty closed_interval Subset of REAL ;

      let f be PartFunc of REAL , REAL ;

      :: INTEGRA5:def2

      func integral (f,A) -> Real equals ( integral (f || A));

      correctness ;

    end

    theorem :: INTEGRA5:6

    

     Th6: for f be PartFunc of REAL , REAL st A c= ( dom f) holds (f || A) is total

    proof

      let f be PartFunc of REAL , REAL ;

      assume

       A1: A c= ( dom f);

      ( dom (f || A)) = (( dom f) /\ A) by RELAT_1: 61

      .= A by A1, XBOOLE_1: 28;

      hence thesis by PARTFUN1:def 2;

    end;

    theorem :: INTEGRA5:7

    for f be PartFunc of REAL , REAL st (f | A) is bounded_above holds ((f || A) | A) is bounded_above;

    theorem :: INTEGRA5:8

    for f be PartFunc of REAL , REAL st (f | A) is bounded_below holds ((f || A) | A) is bounded_below;

    theorem :: INTEGRA5:9

    for f be PartFunc of REAL , REAL st (f | A) is bounded holds ((f || A) | A) is bounded;

    begin

    theorem :: INTEGRA5:10

    

     Th10: for f be PartFunc of REAL , REAL st A c= ( dom f) & (f | A) is continuous holds (f | A) is bounded

    proof

      let f be PartFunc of REAL , REAL ;

      assume

       A1: A c= ( dom f);

      assume (f | A) is continuous;

      then

       A2: (f .: A) is real-bounded by A1, FCONT_1: 29, RCOMP_1: 10;

      then

      consider a be Real such that

       A3: a is UpperBound of (f .: A) by XXREAL_2:def 10;

      

       A4: for r be Real st r in (f .: A) holds r <= a by A3, XXREAL_2:def 1;

      consider b be Real such that

       A5: b is LowerBound of (f .: A) by A2, XXREAL_2:def 9;

      

       A6: for r be Real st r in (f .: A) holds b <= r by A5, XXREAL_2:def 2;

      for x be object st x in (A /\ ( dom f)) holds b <= (f . x)

      proof

        let x be object;

        assume x in (A /\ ( dom f));

        then x in A & x in ( dom f) by XBOOLE_0:def 4;

        then (f . x) in (f .: A) by FUNCT_1:def 6;

        hence thesis by A6;

      end;

      then

       A7: (f | A) is bounded_below by RFUNCT_1: 71;

      for x be object st x in (A /\ ( dom f)) holds (f . x) <= a

      proof

        let x be object;

        assume x in (A /\ ( dom f));

        then x in A & x in ( dom f) by XBOOLE_0:def 4;

        then (f . x) in (f .: A) by FUNCT_1:def 6;

        hence thesis by A4;

      end;

      then (f | A) is bounded_above by RFUNCT_1: 70;

      hence thesis by A7;

    end;

    theorem :: INTEGRA5:11

    

     Th11: for f be PartFunc of REAL , REAL st A c= ( dom f) & (f | A) is continuous holds f is_integrable_on A

    proof

      let f be PartFunc of REAL , REAL ;

      assume

       A1: A c= ( dom f);

      reconsider g = (f | A) as PartFunc of A, REAL by PARTFUN1: 10;

      

       A2: ( dom g) = (( dom f) /\ A) by RELAT_1: 61

      .= A by A1, XBOOLE_1: 28;

      then

       A3: g is total by PARTFUN1:def 2;

      for y be object st y in (f .: A) holds y in ( rng g)

      proof

        let y be object;

        assume y in (f .: A);

        then

        consider x be object such that x in ( dom f) and

         A4: x in A and

         A5: y = (f . x) by FUNCT_1:def 6;

        (g . x) in ( rng g) by A2, A4, FUNCT_1:def 3;

        hence thesis by A2, A4, A5, FUNCT_1: 47;

      end;

      then

       A6: (f .: A) c= ( rng g) by TARSKI:def 3;

      for y be object st y in ( rng g) holds y in (f .: A)

      proof

        let y be object;

        assume y in ( rng g);

        then

        consider x be object such that

         A7: x in ( dom g) and

         A8: y = (g . x) by FUNCT_1:def 3;

        (f . x) in (f .: A) by A1, A2, A7, FUNCT_1:def 6;

        hence thesis by A7, A8, FUNCT_1: 47;

      end;

      then ( rng g) c= (f .: A) by TARSKI:def 3;

      then

       A9: ( rng g) = (f .: A) by A6, XBOOLE_0:def 10;

      assume

       A10: (f | A) is continuous;

      then (f .: A) is real-bounded by A1, FCONT_1: 29, RCOMP_1: 10;

      then

       A11: (g | A) is bounded_above & (g | A) is bounded_below by A9, INTEGRA1: 12, INTEGRA1: 14;

      reconsider g as Function of A, REAL by A3;

      

       A12: (f | A) is uniformly_continuous by A1, A10, FCONT_2: 11;

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

      proof

        let T be DivSequence of A;

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

        assume

         A13: ( delta T) is convergent & ( lim ( delta T)) = 0 ;

        

         A14: for r be Real st 0 < r holds ex n be Nat st for m be Nat st n <= m holds |.((osc . m) - 0 ).| < r

        proof

          let r be Real;

          assume

           A15: r > 0 ;

          ex r1 st r1 > 0 & (r1 * ( vol A)) < r

          proof

            per cases by INTEGRA1: 9;

              suppose

               A16: ( vol A) = 0 ;

              take 1;

              (r1 * ( vol A)) < r by A15, A16;

              hence thesis;

            end;

              suppose

               A17: ( vol A) > 0 ;

              then (r / ( vol A)) > 0 by A15, XREAL_1: 139;

              then

              consider r1 be Real such that

               A18: 0 < r1 and

               A19: r1 < (r / ( vol A)) by XREAL_1: 5;

              take r1;

              (r1 * ( vol A)) < r by A17, A19, XREAL_1: 79;

              hence thesis by A18;

            end;

          end;

          then

          consider r1 such that

           A20: r1 > 0 and

           A21: (r1 * ( vol A)) < r;

          consider s such that

           A22: 0 < s and

           A23: for x1, x2 st x1 in ( dom (f | A)) & x2 in ( dom (f | A)) & |.(x1 - x2).| < s holds |.((f . x1) - (f . x2)).| < r1 by A12, A20, FCONT_2: 1;

          consider n be Nat such that

           A24: for m be Nat st n <= m holds |.((( delta T) . m) - 0 ).| < s by A13, A22, SEQ_2:def 7;

          

           A25: for m st n <= m holds ((( upper_sum (g,T)) . m) - (( lower_sum (g,T)) . m)) <= (r1 * ( vol A))

          proof

            let m;

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

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

            then

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

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

            then

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

            reconsider OSC = (UV - LV) as Element of (( len D) -tuples_on REAL );

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

            then

            reconsider VOL = ( upper_volume (( chi (A,A)),D)) as Element of (( len D) -tuples_on REAL ) by FINSEQ_2: 92;

            assume

             A26: n <= m;

            

             A27: for k st k in ( dom D) holds ((( upper_volume (g,D)) . k) - (( lower_volume (g,D)) . k)) <= (r1 * (( upper_volume (( chi (A,A)),D)) . k))

            proof

              let k;

              assume

               A28: k in ( dom D);

              reconsider h = (g | ( divset (D,k))) as PartFunc of ( divset (D,k)), REAL by PARTFUN1: 10;

              ( dom g) = A by PARTFUN1:def 2;

              then (( dom g) /\ ( divset (D,k))) = ( divset (D,k)) by A28, INTEGRA1: 8, XBOOLE_1: 28;

              then ( dom h) = ( divset (D,k)) by RELAT_1: 61;

              then h is total by PARTFUN1:def 2;

              then

              reconsider h as Function of ( divset (D,k)), REAL ;

              

               A29: for x1, x2 st x1 in ( divset (D,k)) & x2 in ( divset (D,k)) holds |.((h . x1) - (h . x2)).| <= r1

              proof

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

                then

                 A30: (( upper_volume (( chi (A,A)),D)) . k) >= 0 by INTEGRA1: 9;

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

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

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

                then

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

                ( dom h) = (( dom g) /\ ( divset (D,k))) by RELAT_1: 61;

                then

                 A32: ( dom h) c= ( dom g) by XBOOLE_1: 17;

                let x1, x2;

                assume that

                 A33: x1 in ( divset (D,k)) and

                 A34: x2 in ( divset (D,k));

                

                 A35: x2 in ( dom h) by A34, PARTFUN1:def 2;

                then (g . x2) = (h . x2) by FUNCT_1: 47;

                then

                 A36: (f . x2) = (h . x2) by A35, A32, FUNCT_1: 47;

                

                 A37: |.(x1 - x2).| <= (( delta T) . m)

                proof

                  now

                    per cases ;

                      suppose x1 >= x2;

                      then (x1 - x2) >= 0 by XREAL_1: 48;

                      then

                       A38: |.(x1 - x2).| = (x1 - x2) by ABSVALUE:def 1;

                      x1 <= ( upper_bound ( divset (D,k))) & x2 >= ( lower_bound ( divset (D,k))) by A33, A34, INTEGRA2: 1;

                      then |.(x1 - x2).| <= (( upper_bound ( divset (D,k))) - ( lower_bound ( divset (D,k)))) by A38, XREAL_1: 13;

                      then

                       A39: |.(x1 - x2).| <= ( vol ( divset (D,k))) by INTEGRA1:def 5;

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

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

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

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

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

                      then

                       A40: (( upper_volume (( chi (A,A)),D)) . k) <= ( delta (T . m)) by INTEGRA3:def 1;

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

                      then |.(x1 - x2).| <= ( delta (T . m)) by A39, A40, XXREAL_0: 2;

                      hence thesis by INTEGRA3:def 2;

                    end;

                      suppose x1 < x2;

                      then (x1 - x2) < 0 by XREAL_1: 49;

                      then |.(x1 - x2).| = ( - (x1 - x2)) by ABSVALUE:def 1;

                      then

                       A41: |.(x1 - x2).| = (x2 - x1);

                      x2 <= ( upper_bound ( divset (D,k))) & x1 >= ( lower_bound ( divset (D,k))) by A33, A34, INTEGRA2: 1;

                      then |.(x1 - x2).| <= (( upper_bound ( divset (D,k))) - ( lower_bound ( divset (D,k)))) by A41, XREAL_1: 13;

                      then

                       A42: |.(x1 - x2).| <= ( vol ( divset (D,k))) by INTEGRA1:def 5;

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

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

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

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

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

                      then

                       A43: (( upper_volume (( chi (A,A)),D)) . k) <= ( delta (T . m)) by INTEGRA3:def 1;

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

                      then |.(x1 - x2).| <= ( delta (T . m)) by A42, A43, XXREAL_0: 2;

                      hence thesis by INTEGRA3:def 2;

                    end;

                  end;

                  hence thesis;

                end;

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

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

                then ((( delta T) . m) - 0 ) >= 0 by A30, A31, XXREAL_2:def 8;

                then

                 A44: |.(x1 - x2).| <= |.((( delta T) . m) - 0 ).| by A37, ABSVALUE:def 1;

                 |.((( delta T) . m) - 0 ).| < s by A24, A26;

                then

                 A45: |.(x1 - x2).| < s by A44, XXREAL_0: 2;

                

                 A46: x1 in ( dom h) by A33, PARTFUN1:def 2;

                then (g . x1) = (h . x1) by FUNCT_1: 47;

                then (f . x1) = (h . x1) by A46, A32, FUNCT_1: 47;

                hence thesis by A23, A45, A46, A35, A32, A36;

              end;

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

              then ((( upper_bound ( rng (g | ( divset (D,k))))) - ( lower_bound ( rng (g | ( divset (D,k)))))) * ( vol ( divset (D,k)))) <= (r1 * ( vol ( divset (D,k)))) by A29, INTEGRA4: 24, XREAL_1: 64;

              then ((( upper_bound ( rng (g | ( divset (D,k))))) * ( vol ( divset (D,k)))) - (( lower_bound ( rng (g | ( divset (D,k))))) * ( vol ( divset (D,k))))) <= (r1 * ( vol ( divset (D,k))));

              then ((( upper_volume (g,D)) . k) - (( lower_bound ( rng (g | ( divset (D,k))))) * ( vol ( divset (D,k))))) <= (r1 * ( vol ( divset (D,k)))) by A28, INTEGRA1:def 6;

              then ((( upper_volume (g,D)) . k) - (( lower_volume (g,D)) . k)) <= (r1 * ( vol ( divset (D,k)))) by A28, INTEGRA1:def 7;

              hence thesis by A28, INTEGRA1: 20;

            end;

            for k be Nat st k in ( Seg ( len D)) holds (OSC . k) <= ((r1 * VOL) . k)

            proof

              let k be Nat;

              assume k in ( Seg ( len D));

              then

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

              (OSC . k) = ((( upper_volume (g,D)) . k) - (( lower_volume (g,D)) . k)) by RVSUM_1: 27;

              then (OSC . k) <= (r1 * (VOL . k)) by A27, A47;

              hence thesis by RVSUM_1: 45;

            end;

            then ( Sum OSC) <= ( Sum (r1 * VOL)) by RVSUM_1: 82;

            then ( Sum OSC) <= (r1 * ( Sum VOL)) by RVSUM_1: 87;

            then (( Sum UV) - ( Sum LV)) <= (r1 * ( Sum VOL)) by RVSUM_1: 90;

            then (( upper_sum (g,D)) - ( Sum LV)) <= (r1 * ( Sum VOL)) by INTEGRA1:def 8;

            then (( upper_sum (g,D)) - ( lower_sum (g,D))) <= (r1 * ( Sum VOL)) by INTEGRA1:def 9;

            then (( upper_sum (g,D)) - ( lower_sum (g,D))) <= (r1 * ( vol A)) by INTEGRA1: 24;

            then ((( upper_sum (g,T)) . m) - ( lower_sum (g,D))) <= (r1 * ( vol A)) by INTEGRA2:def 2;

            hence thesis by INTEGRA2:def 3;

          end;

          take n;

          let m be Nat;

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

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

          assume n <= m;

          then ((( upper_sum (g,T)) . mm) - (( lower_sum (g,T)) . mm)) <= (r1 * ( vol A)) by A25;

          then

           A48: ((( upper_sum (g,T)) . m) - (( lower_sum (g,T)) . m)) < r by A21, XXREAL_0: 2;

          ( upper_sum (g,D)) >= ( lower_sum (g,D)) by A11, INTEGRA1: 28;

          then (( upper_sum (g,T)) . mm) >= ( lower_sum (g,D)) by INTEGRA2:def 2;

          then (( upper_sum (g,T)) . mm) >= (( lower_sum (g,T)) . mm) by INTEGRA2:def 3;

          then

           A49: ((( upper_sum (g,T)) . m) - (( lower_sum (g,T)) . m)) >= 0 by XREAL_1: 48;

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

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

          .= ((( upper_sum (g,T)) . m) - (( lower_sum (g,T)) . m));

          hence thesis by A48, A49, ABSVALUE:def 1;

        end;

        then osc is convergent by SEQ_2:def 6;

        then

         A50: ( lim osc) = 0 by A14, SEQ_2:def 7;

        ( upper_sum (g,T)) is convergent & ( lower_sum (g,T)) is convergent by A11, A13, INTEGRA4: 8, INTEGRA4: 9;

        hence thesis by A50, SEQ_2: 12;

      end;

      then g is integrable by A11, INTEGRA4: 12;

      hence thesis;

    end;

    theorem :: INTEGRA5:12

    

     Th12: for f be PartFunc of REAL , REAL , D be Division of A st A c= X & f is_differentiable_on X & ((f `| X) | A) is bounded holds ( lower_sum (((f `| X) || A),D)) <= ((f . ( upper_bound A)) - (f . ( lower_bound A))) & ((f . ( upper_bound A)) - (f . ( lower_bound A))) <= ( upper_sum (((f `| X) || A),D))

    proof

      let f be PartFunc of REAL , REAL ;

      let D be Division of A;

      assume that

       A1: A c= X and

       A2: f is_differentiable_on X and

       A3: ((f `| X) | A) is bounded;

      (( len D) - 1) in NAT

      proof

        ex j be Nat st ( len D) = (1 + j) by NAT_1: 10, NAT_1: 14;

        hence thesis by ORDINAL1:def 12;

      end;

      then

      reconsider k1 = (( len D) - 1) as Element of NAT ;

      deffunc G( Nat) = ( In ((f . ( lower_bound ( divset (D,($1 + 1))))), REAL ));

      deffunc F( Nat) = ( In (((f . ( upper_bound ( divset (D,$1)))) - (f . ( lower_bound ( divset (D,$1))))), REAL ));

      consider p be FinSequence of REAL such that

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

      X c= ( dom f) by A2, FDIFF_1:def 6;

      then

       A5: A c= ( dom f) by A1, XBOOLE_1: 1;

      

       A6: for k st k in ( dom D) holds ex r st r in ( divset (D,k)) & ((f . ( upper_bound ( divset (D,k)))) - (f . ( lower_bound ( divset (D,k))))) = (( diff (f,r)) * ( vol ( divset (D,k))))

      proof

        let k;

        assume

         A7: k in ( dom D);

        now

          per cases ;

            suppose

             A8: ( lower_bound ( divset (D,k))) = ( upper_bound ( divset (D,k)));

            consider r such that

             A9: r = ( upper_bound ( divset (D,k)));

            

             A10: r in ( divset (D,k))

            proof

              ex a, b st a <= b & a = ( lower_bound ( divset (D,k))) & b = ( upper_bound ( divset (D,k))) by SEQ_4: 11;

              hence thesis by A9, INTEGRA2: 1;

            end;

            (( upper_bound ( divset (D,k))) - ( lower_bound ( divset (D,k)))) = 0 by A8;

            then ( vol ( divset (D,k))) = 0 by INTEGRA1:def 5;

            then (( diff (f,r)) * ( vol ( divset (D,k)))) = 0 ;

            hence thesis by A8, A10;

          end;

            suppose

             A11: ( lower_bound ( divset (D,k))) <> ( upper_bound ( divset (D,k)));

            ex r1, r2 st r1 <= r2 & r1 = ( lower_bound ( divset (D,k))) & r2 = ( upper_bound ( divset (D,k))) by SEQ_4: 11;

            then

             A12: ( lower_bound ( divset (D,k))) < ( upper_bound ( divset (D,k))) by A11, XXREAL_0: 1;

            (f | X) is continuous by A2, FDIFF_1: 25;

            then (f | A) is continuous by A1, FCONT_1: 16;

            then

             A13: (f | ( divset (D,k))) is continuous by A7, FCONT_1: 16, INTEGRA1: 8;

            

             A14: ( divset (D,k)) = [.( lower_bound ( divset (D,k))), ( upper_bound ( divset (D,k))).] by INTEGRA1: 4;

            then

             A15: ].( lower_bound ( divset (D,k))), ( upper_bound ( divset (D,k))).[ c= ( divset (D,k)) by XXREAL_1: 25;

            

             A16: ( divset (D,k)) c= A by A7, INTEGRA1: 8;

            then ].( lower_bound ( divset (D,k))), ( upper_bound ( divset (D,k))).[ c= A by A15, XBOOLE_1: 1;

            then f is_differentiable_on ].( lower_bound ( divset (D,k))), ( upper_bound ( divset (D,k))).[ by A1, A2, FDIFF_1: 26, XBOOLE_1: 1;

            then

            consider r such that

             A17: r in ].( lower_bound ( divset (D,k))), ( upper_bound ( divset (D,k))).[ and

             A18: ( diff (f,r)) = (((f . ( upper_bound ( divset (D,k)))) - (f . ( lower_bound ( divset (D,k))))) / (( upper_bound ( divset (D,k))) - ( lower_bound ( divset (D,k))))) by A5, A16, A13, A12, A14, ROLLE: 3, XBOOLE_1: 1;

            (( upper_bound ( divset (D,k))) - ( lower_bound ( divset (D,k)))) > 0 by A12, XREAL_1: 50;

            then (( diff (f,r)) * (( upper_bound ( divset (D,k))) - ( lower_bound ( divset (D,k))))) = ((f . ( upper_bound ( divset (D,k)))) - (f . ( lower_bound ( divset (D,k))))) by A18, XCMPLX_1: 87;

            then (( diff (f,r)) * ( vol ( divset (D,k)))) = ((f . ( upper_bound ( divset (D,k)))) - (f . ( lower_bound ( divset (D,k))))) by INTEGRA1:def 5;

            hence thesis by A15, A17;

          end;

        end;

        hence thesis;

      end;

      

       A19: ( dom p) = ( Seg ( len D)) by A4, FINSEQ_1:def 3;

      

       A20: for i st i in ( Seg k1) holds ( upper_bound ( divset (D,i))) = ( lower_bound ( divset (D,(i + 1))))

      proof

        let i;

        assume

         A21: i in ( Seg k1);

        then i <= k1 by FINSEQ_1: 1;

        then

         A22: (i + 1) <= (k1 + 1) by XREAL_1: 7;

        1 <= i by A21, FINSEQ_1: 1;

        then (1 + 0 ) <= (i + 1) by XREAL_1: 7;

        then (i + 1) in ( Seg ( len D)) by A22, FINSEQ_1: 1;

        then

         A23: (i + 1) in ( dom D) by FINSEQ_1:def 3;

        (k1 + 1) = ( len D);

        then k1 <= ( len D) by NAT_1: 11;

        then ( Seg k1) c= ( Seg ( len D)) by FINSEQ_1: 5;

        then i in ( Seg ( len D)) by A21;

        then

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

        

         A25: ((i + 1) - 1) = i;

        now

          per cases ;

            suppose

             A26: i = 1;

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

            hence thesis by A23, A25, A26, INTEGRA1:def 4;

          end;

            suppose

             A27: i <> 1;

            i >= 1 by A21, FINSEQ_1: 1;

            then (i + 1) >= (1 + 1) by XREAL_1: 6;

            then

             A28: (i + 1) <> 1;

            ( upper_bound ( divset (D,i))) = (D . i) by A24, A27, INTEGRA1:def 4;

            hence thesis by A23, A25, A28, INTEGRA1:def 4;

          end;

        end;

        hence thesis;

      end;

      consider s2 be FinSequence of REAL such that

       A29: ( len s2) = k1 & for i be Nat st i in ( dom s2) holds (s2 . i) = G(i) from FINSEQ_2:sch 1;

      

       A30: for k st k in ( dom D) holds ( rng (((f `| X) || A) | ( divset (D,k)))) is real-bounded

      proof

        ( dom (f `| X)) = X by A2, FDIFF_1:def 7;

        then

        reconsider g = (f `| X) as PartFunc of X, REAL by RELSET_1: 5;

        let k;

        assume k in ( dom D);

        consider r1 be Real such that

         A31: for x be object st x in (A /\ ( dom (f `| X))) holds ((f `| X) . x) <= r1 by A3, RFUNCT_1: 70;

        consider r2 be Real such that

         A32: for x be object st x in (A /\ ( dom (f `| X))) holds ((f `| X) . x) >= r2 by A3, RFUNCT_1: 71;

        

         A33: ( dom ((f `| X) | A)) = (( dom (f `| X)) /\ A) by RELAT_1: 61;

        for x be object st x in (A /\ ( dom ((f `| X) || A))) holds (((f `| X) || A) . x) >= r2

        proof

          let x be object;

          

           A34: (A /\ (A /\ ( dom (f `| X)))) = ((A /\ A) /\ ( dom (f `| X))) by XBOOLE_1: 16

          .= (A /\ ( dom (f `| X)));

          reconsider y = (g . x) as Real;

          assume

           A35: x in (A /\ ( dom ((f `| X) || A)));

          then y >= r2 by A32, A33, A34;

          hence thesis by A33, A35, A34, FUNCT_1: 47;

        end;

        then (((f `| X) || A) | A) is bounded_below by RFUNCT_1: 71;

        then

         A36: ( rng (((f `| X) || A) | ( divset (D,k)))) is bounded_below by INTEGRA4: 19;

        for x be object st x in (A /\ ( dom ((f `| X) || A))) holds (((f `| X) || A) . x) <= r1

        proof

          let x be object;

          

           A37: (A /\ (A /\ ( dom (f `| X)))) = ((A /\ A) /\ ( dom (f `| X))) by XBOOLE_1: 16

          .= (A /\ ( dom (f `| X)));

          reconsider y = (g . x) as Real;

          assume

           A38: x in (A /\ ( dom ((f `| X) || A)));

          then y <= r1 by A31, A33, A37;

          hence thesis by A33, A38, A37, FUNCT_1: 47;

        end;

        then (((f `| X) || A) | A) is bounded_above by RFUNCT_1: 70;

        then ( rng (((f `| X) || A) | ( divset (D,k)))) is bounded_above by INTEGRA4: 18;

        hence thesis by A36;

      end;

      deffunc F1( Nat) = ( In ((f . ( upper_bound ( divset (D,$1)))), REAL ));

      consider s1 be FinSequence of REAL such that

       A39: ( len s1) = k1 & for i be Nat st i in ( dom s1) holds (s1 . i) = F1(i) from FINSEQ_2:sch 1;

      

       A40: ( dom s2) = ( Seg k1) by A29, FINSEQ_1:def 3;

      reconsider flb = (f . ( lower_bound A)), fub = (f . ( upper_bound A)) as Element of REAL by XREAL_0:def 1;

      ( len (s1 ^ <*(f . ( upper_bound A))*>)) = ( len ( <*(f . ( lower_bound A))*> ^ s2)) & ( len (s1 ^ <*(f . ( upper_bound A))*>)) = ( len p) & for i st i in ( dom (s1 ^ <*fub*>)) holds (p . i) = (((s1 ^ <*fub*>) /. i) - (( <*flb*> ^ s2) /. i))

      proof

        ( dom <*(f . ( upper_bound A))*>) = ( Seg 1) by FINSEQ_1:def 8;

        then ( len <*(f . ( upper_bound A))*>) = 1 by FINSEQ_1:def 3;

        then

         A41: ( len (s1 ^ <*(f . ( upper_bound A))*>)) = (k1 + 1) by A39, FINSEQ_1: 22;

        ( dom <*(f . ( lower_bound A))*>) = ( Seg 1) by FINSEQ_1:def 8;

        then ( len <*(f . ( lower_bound A))*>) = 1 by FINSEQ_1:def 3;

        hence

         A42: ( len (s1 ^ <*(f . ( upper_bound A))*>)) = ( len ( <*(f . ( lower_bound A))*> ^ s2)) by A29, A41, FINSEQ_1: 22;

        thus ( len (s1 ^ <*(f . ( upper_bound A))*>)) = ( len p) by A4, A41;

        let i;

        assume

         A43: i in ( dom (s1 ^ <*fub*>));

        then

         A44: ((s1 ^ <*fub*>) /. i) = ((s1 ^ <*(f . ( upper_bound A))*>) . i) by PARTFUN1:def 6;

        i in ( Seg ( len (s1 ^ <*(f . ( upper_bound A))*>))) by A43, FINSEQ_1:def 3;

        then i in ( dom ( <*(f . ( lower_bound A))*> ^ s2)) by A42, FINSEQ_1:def 3;

        then

         A45: (( <*flb*> ^ s2) /. i) = (( <*flb*> ^ s2) . i) by PARTFUN1:def 6;

        

         A46: ( len D) = 1 or ( len D) is non trivial by NAT_2:def 1;

        now

          per cases by A46, NAT_2: 29;

            suppose

             A47: ( len D) = 1;

            then

             A48: i in ( Seg 1) by A41, A43, FINSEQ_1:def 3;

            then

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

            s1 = {} by A39, A47;

            then (s1 ^ <*(f . ( upper_bound A))*>) = <*(f . ( upper_bound A))*> by FINSEQ_1: 34;

            then

             A50: ((s1 ^ <*fub*>) /. i) = (f . ( upper_bound A)) by A44, A49, FINSEQ_1:def 8;

            

             A51: i in ( dom D) by A47, A48, FINSEQ_1:def 3;

            s2 = {} by A29, A47;

            then ( <*(f . ( lower_bound A))*> ^ s2) = <*(f . ( lower_bound A))*> by FINSEQ_1: 34;

            then

             A52: (( <*flb*> ^ s2) /. i) = (f . ( lower_bound A)) by A45, A49, FINSEQ_1:def 8;

            (D . i) = ( upper_bound A) by A47, A49, INTEGRA1:def 2;

            then

             A53: ( upper_bound ( divset (D,i))) = ( upper_bound A) by A49, A51, INTEGRA1:def 4;

            (p . i) = F(i) by A4, A19, A47, A48

            .= ((f . ( upper_bound ( divset (D,i)))) - (f . ( lower_bound ( divset (D,i)))));

            hence thesis by A49, A51, A50, A52, A53, INTEGRA1:def 4;

          end;

            suppose

             A54: ( len D) >= 2;

            1 = (2 - 1);

            then

             A55: k1 >= 1 by A54, XREAL_1: 9;

            now

              per cases ;

                suppose

                 A56: i = 1;

                then

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

                then i in ( dom <*(f . ( lower_bound A))*>) by FINSEQ_1:def 8;

                then (( <*(f . ( lower_bound A))*> ^ s2) . i) = ( <*(f . ( lower_bound A))*> . i) by FINSEQ_1:def 7;

                then

                 A58: (( <*(f . ( lower_bound A))*> ^ s2) . i) = (f . ( lower_bound A)) by A56, FINSEQ_1:def 8;

                ( Seg 1) c= ( Seg k1) by A55, FINSEQ_1: 5;

                then i in ( Seg k1) by A57;

                then

                 A59: i in ( dom s1) by A39, FINSEQ_1:def 3;

                

                then ((s1 ^ <*(f . ( upper_bound A))*>) . i) = (s1 . i) by FINSEQ_1:def 7

                .= F1(i) by A39, A59;

                then

                 A60: ((s1 ^ <*(f . ( upper_bound A))*>) . i) = (f . ( upper_bound ( divset (D,i))));

                

                 A61: i in ( Seg 2) by A56, FINSEQ_1: 2, TARSKI:def 2;

                

                 A62: ( Seg 2) c= ( Seg ( len D)) by A54, FINSEQ_1: 5;

                then i in ( Seg ( len D)) by A61;

                then

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

                (p . i) = F(i) by A4, A19, A62, A61

                .= ((f . ( upper_bound ( divset (D,i)))) - (f . ( lower_bound ( divset (D,i)))));

                hence thesis by A44, A45, A56, A63, A60, A58, INTEGRA1:def 4;

              end;

                suppose

                 A64: i = ( len D);

                then (i - ( len s1)) in ( Seg 1) by A39, FINSEQ_1: 2, TARSKI:def 1;

                then

                 A65: (i - ( len s1)) in ( dom <*(f . ( upper_bound A))*>) by FINSEQ_1:def 8;

                i = ((i - ( len s1)) + ( len s1));

                then ((s1 ^ <*(f . ( upper_bound A))*>) . i) = ( <*(f . ( upper_bound A))*> . (i - ( len s1))) by A65, FINSEQ_1:def 7;

                then

                 A66: ((s1 ^ <*fub*>) /. i) = (f . ( upper_bound A)) by A39, A44, A64, FINSEQ_1:def 8;

                

                 A67: ( len <*(f . ( lower_bound A))*>) = 1 by FINSEQ_1: 40;

                

                 A68: i <> 1 by A54, A64;

                i in ( Seg ( len D)) by A64, FINSEQ_1: 3;

                then

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

                (p . i) = F(i) by A4, A19, A64, FINSEQ_1: 3

                .= ((f . ( upper_bound ( divset (D,i)))) - (f . ( lower_bound ( divset (D,i)))));

                then (p . i) = ((f . ( upper_bound ( divset (D,i)))) - (f . (D . (i - 1)))) by A69, A68, INTEGRA1:def 4;

                then

                 A70: (p . i) = ((f . (D . i)) - (f . (D . (i - 1)))) by A69, A68, INTEGRA1:def 4;

                (i - 1) <> 0 by A54, A64;

                then

                 A71: (i - 1) in ( Seg k1) by A64, FINSEQ_1: 3;

                then

                reconsider i1 = (i - 1) as Nat;

                

                 A72: (( len <*(f . ( lower_bound A))*>) + (i - ( len <*(f . ( lower_bound A))*>))) = i & (i - ( len <*(f . ( lower_bound A))*>)) in ( dom s2) by A29, A67, FINSEQ_1:def 3, A71;

                

                then (( <*(f . ( lower_bound A))*> ^ s2) . i) = (s2 . i1) by FINSEQ_1:def 7, A67

                .= G(i1) by A29, A67, A72;

                then (( <*(f . ( lower_bound A))*> ^ s2) . i) = (f . ( lower_bound ( divset (D,i))));

                then (( <*(f . ( lower_bound A))*> ^ s2) . i) = (f . (D . (i - 1))) by A69, A68, INTEGRA1:def 4;

                hence thesis by A45, A64, A66, A70, INTEGRA1:def 2;

              end;

                suppose

                 A73: i <> 1 & i <> ( len D);

                (( len s1) + ( len <*(f . ( upper_bound A))*>)) = (k1 + 1) by A39, FINSEQ_1: 39;

                then

                 A74: i in ( Seg ( len D)) by A43, FINSEQ_1:def 7;

                

                 A75: i in ( dom s1) & i in ( Seg k1) & (i - 1) in ( Seg k1) & ((i - 1) + 1) = i & (i - ( len <*(f . ( lower_bound A))*>)) in ( dom s2)

                proof

                  i <> 0 by A74, FINSEQ_1: 1;

                  then i is non trivial by A73, NAT_2:def 1;

                  then i >= (1 + 1) by NAT_2: 29;

                  then

                   A76: (i - 1) >= 1 by XREAL_1: 19;

                  

                   A77: 1 <= i by A74, FINSEQ_1: 1;

                  i <= ( len D) by A74, FINSEQ_1: 1;

                  then

                   A78: i < (k1 + 1) by A73, XXREAL_0: 1;

                  then

                   A79: i <= k1 by NAT_1: 13;

                  then i in ( Seg ( len s1)) by A39, A77, FINSEQ_1: 1;

                  hence i in ( dom s1) by FINSEQ_1:def 3;

                  thus i in ( Seg k1) by A77, A79, FINSEQ_1: 1;

                  i <= k1 by A78, NAT_1: 13;

                  then (i - 1) <= (k1 - 1) by XREAL_1: 9;

                  then

                   A80: ((i - 1) + 0 ) <= ((k1 - 1) + 1) by XREAL_1: 7;

                  ex j be Nat st i = (1 + j) by A77, NAT_1: 10;

                  hence (i - 1) in ( Seg k1) by A76, A80, FINSEQ_1: 1;

                  then

                   A81: (i - ( len <*(f . ( lower_bound A))*>)) in ( Seg ( len s2)) by A29, FINSEQ_1: 39;

                  thus ((i - 1) + 1) = i;

                  thus thesis by A81, FINSEQ_1:def 3;

                end;

                then

                 A82: (i - ( len <*(f . ( lower_bound A))*>)) in ( Seg ( len s2)) by FINSEQ_1:def 3;

                then (i - ( len <*(f . ( lower_bound A))*>)) <= ( len s2) by FINSEQ_1: 1;

                then

                 A83: i <= (( len <*(f . ( lower_bound A))*>) + ( len s2)) by XREAL_1: 20;

                i >= 1 by A74, FINSEQ_1: 1;

                then

                reconsider i1 = (i - 1) as Element of NAT by INT_1: 5;

                1 <= (i - ( len <*(f . ( lower_bound A))*>)) by A82, FINSEQ_1: 1;

                then (( len <*(f . ( lower_bound A))*>) + 1) <= i by XREAL_1: 19;

                then (( <*(f . ( lower_bound A))*> ^ s2) . i) = (s2 . (i - ( len <*(f . ( lower_bound A))*>))) by A83, FINSEQ_1: 23;

                

                then (( <*(f . ( lower_bound A))*> ^ s2) . i) = (s2 . (i - 1)) by FINSEQ_1: 39

                .= G(i1) by A29, A40, A75;

                then

                 A84: (( <*(f . ( lower_bound A))*> ^ s2) . i) = (f . ( lower_bound ( divset (D,i))));

                ((s1 ^ <*(f . ( upper_bound A))*>) . i) = (s1 . i) by A75, FINSEQ_1:def 7

                .= F1(i) by A39, A75;

                then

                 A85: ((s1 ^ <*(f . ( upper_bound A))*>) . i) = (f . ( upper_bound ( divset (D,i))));

                

                thus (p . i) = F(i) by A4, A19, A74

                .= (((s1 ^ <*fub*>) /. i) - (( <*flb*> ^ s2) /. i)) by A44, A45, A84, A85;

              end;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      then ( Sum p) = (( Sum (s1 ^ <*(f . ( upper_bound A))*>)) - ( Sum ( <*(f . ( lower_bound A))*> ^ s2))) by INTEGRA1: 22;

      then ( Sum p) = ((( Sum s1) + (f . ( upper_bound A))) - ( Sum ( <*(f . ( lower_bound A))*> ^ s2))) by RVSUM_1: 74;

      then

       A86: ( Sum p) = ((( Sum s1) + (f . ( upper_bound A))) - ((f . ( lower_bound A)) + ( Sum s2))) by RVSUM_1: 76;

      

       A87: ( dom s1) = ( Seg k1) by A39, FINSEQ_1:def 3;

      

       A88: ( dom s1) = ( Seg k1) by A39, FINSEQ_1:def 3;

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

      proof

        let i be Nat;

        assume

         A89: i in ( dom s1);

        

        then (s1 . i) = F1(i) by A39

        .= (f . ( upper_bound ( divset (D,i))));

        

        then (s1 . i) = (f . ( lower_bound ( divset (D,(i + 1))))) by A20, A87, A89

        .= G(i);

        hence thesis by A88, A29, A40, A89;

      end;

      then

       A90: s1 = s2 by A39, A29, FINSEQ_2: 9;

      

       A91: for k, r st k in ( dom D) & r in ( divset (D,k)) holds ( diff (f,r)) in ( rng (((f `| X) || A) | ( divset (D,k))))

      proof

        

         A92: ( dom ((f `| X) | A)) = (( dom (f `| X)) /\ A) by RELAT_1: 61

        .= (X /\ A) by A2, FDIFF_1:def 7

        .= A by A1, XBOOLE_1: 28;

        let k, r;

        assume that

         A93: k in ( dom D) and

         A94: r in ( divset (D,k));

        

         A95: ( divset (D,k)) c= A by A93, INTEGRA1: 8;

        then ( divset (D,k)) c= X by A1, XBOOLE_1: 1;

        then ((f `| X) . r) = ( diff (f,r)) by A2, A94, FDIFF_1:def 7;

        then

         A96: ( diff (f,r)) = (((f `| X) || A) . r) by A94, A95, A92, FUNCT_1: 47;

        

         A97: ( dom (((f `| X) || A) | ( divset (D,k)))) = (A /\ ( divset (D,k))) by A92, RELAT_1: 61

        .= ( divset (D,k)) by A93, INTEGRA1: 8, XBOOLE_1: 28;

        then ((((f `| X) || A) | ( divset (D,k))) . r) in ( rng (((f `| X) || A) | ( divset (D,k)))) by A94, FUNCT_1:def 3;

        hence thesis by A94, A96, A97, FUNCT_1: 47;

      end;

      

       A98: for k st k in ( dom D) holds ((f . ( upper_bound ( divset (D,k)))) - (f . ( lower_bound ( divset (D,k))))) <= (( upper_volume (((f `| X) || A),D)) . k)

      proof

        let k;

        

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

        assume

         A100: k in ( dom D);

        then

        consider r such that

         A101: r in ( divset (D,k)) and

         A102: ((f . ( upper_bound ( divset (D,k)))) - (f . ( lower_bound ( divset (D,k))))) = (( diff (f,r)) * ( vol ( divset (D,k)))) by A6;

        

         A103: ( rng (((f `| X) || A) | ( divset (D,k)))) is real-bounded by A30, A100;

        ( diff (f,r)) in ( rng (((f `| X) || A) | ( divset (D,k)))) by A91, A100, A101;

        then ( diff (f,r)) <= ( upper_bound ( rng (((f `| X) || A) | ( divset (D,k))))) by A103, SEQ_4:def 1;

        then (( diff (f,r)) * ( vol ( divset (D,k)))) <= (( upper_bound ( rng (((f `| X) || A) | ( divset (D,k))))) * ( vol ( divset (D,k)))) by A99, XREAL_1: 64;

        hence thesis by A100, A102, INTEGRA1:def 6;

      end;

      

       A104: ((f . ( upper_bound A)) - (f . ( lower_bound A))) <= ( upper_sum (((f `| X) || A),D))

      proof

        ( len ( upper_volume (((f `| X) || A),D))) = ( len D) by INTEGRA1:def 6;

        then

        reconsider q = ( upper_volume (((f `| X) || A),D)) as Element of (( len D) -tuples_on REAL ) by FINSEQ_2: 92;

        

         A105: for k be Nat st k in ( Seg ( len D)) holds (p . k) <= (( upper_volume (((f `| X) || A),D)) . k)

        proof

          let k be Nat;

          assume

           A106: k in ( Seg ( len D));

          

           A107: ((f . ( upper_bound ( divset (D,k)))) - (f . ( lower_bound ( divset (D,k))))) = F(k)

          .= (p . k) by A4, A19, A106;

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

          hence thesis by A98, A107;

        end;

        reconsider p as Element of (( len D) -tuples_on REAL ) by A4, FINSEQ_2: 92;

        ( Sum p) <= ( Sum q) by A105, RVSUM_1: 82;

        hence thesis by A90, A86, INTEGRA1:def 8;

      end;

      

       A108: for k st k in ( dom D) holds ((f . ( upper_bound ( divset (D,k)))) - (f . ( lower_bound ( divset (D,k))))) >= (( lower_volume (((f `| X) || A),D)) . k)

      proof

        let k;

        assume

         A109: k in ( dom D);

        then

         A110: ( vol ( divset (D,k))) >= 0 & (( lower_bound ( rng (((f `| X) || A) | ( divset (D,k))))) * ( vol ( divset (D,k)))) = (( lower_volume (((f `| X) || A),D)) . k) by INTEGRA1: 9, INTEGRA1:def 7;

        

         A111: ( rng (((f `| X) || A) | ( divset (D,k)))) is real-bounded by A30, A109;

        consider r such that

         A112: r in ( divset (D,k)) and

         A113: ((f . ( upper_bound ( divset (D,k)))) - (f . ( lower_bound ( divset (D,k))))) = (( diff (f,r)) * ( vol ( divset (D,k)))) by A6, A109;

        ( diff (f,r)) in ( rng (((f `| X) || A) | ( divset (D,k)))) by A91, A109, A112;

        then ( diff (f,r)) >= ( lower_bound ( rng (((f `| X) || A) | ( divset (D,k))))) by A111, SEQ_4:def 2;

        hence thesis by A113, A110, XREAL_1: 64;

      end;

      ((f . ( upper_bound A)) - (f . ( lower_bound A))) >= ( lower_sum (((f `| X) || A),D))

      proof

        ( len ( lower_volume (((f `| X) || A),D))) = ( len D) by INTEGRA1:def 7;

        then

        reconsider q = ( lower_volume (((f `| X) || A),D)) as Element of (( len D) -tuples_on REAL ) by FINSEQ_2: 92;

        

         A114: for k be Nat st k in ( Seg ( len D)) holds (p . k) >= (( lower_volume (((f `| X) || A),D)) . k)

        proof

          let k be Nat;

          assume

           A115: k in ( Seg ( len D));

          

           A116: ((f . ( upper_bound ( divset (D,k)))) - (f . ( lower_bound ( divset (D,k))))) = F(k)

          .= (p . k) by A4, A19, A115;

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

          hence thesis by A108, A116;

        end;

        reconsider p as Element of (( len D) -tuples_on REAL ) by A4, FINSEQ_2: 92;

        ( Sum q) <= ( Sum p) by A114, RVSUM_1: 82;

        hence thesis by A90, A86, INTEGRA1:def 9;

      end;

      hence thesis by A104;

    end;

    ::$Notion-Name

    theorem :: INTEGRA5:13

    

     Th13: for f be PartFunc of REAL , REAL st A c= X & f is_differentiable_on X & (f `| X) is_integrable_on A & ((f `| X) | A) is bounded holds ( integral ((f `| X),A)) = ((f . ( upper_bound A)) - (f . ( lower_bound A)))

    proof

      let f be PartFunc of REAL , REAL ;

      assume that

       A1: A c= X & f is_differentiable_on X and

       A2: (f `| X) is_integrable_on A and

       A3: ((f `| X) | A) is bounded;

      ((f `| X) || A) is integrable by A2;

      then

       A4: ( upper_integral ((f `| X) || A)) = ( lower_integral ((f `| X) || A)) by INTEGRA1:def 16;

      

       A5: for r be Real st r in ( rng ( upper_sum_set ((f `| X) || A))) holds ((f . ( upper_bound A)) - (f . ( lower_bound A))) <= r

      proof

        let r be Real;

        assume r in ( rng ( upper_sum_set ((f `| X) || A)));

        then

        consider D be Element of ( divs A) such that

         A6: D in ( dom ( upper_sum_set ((f `| X) || A))) & r = (( upper_sum_set ((f `| X) || A)) . D) by PARTFUN1: 3;

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

        r = ( upper_sum (((f `| X) || A),D)) by A6, INTEGRA1:def 10;

        hence thesis by A1, A3, Th12;

      end;

      ((f . ( upper_bound A)) - (f . ( lower_bound A))) <= ( lower_bound ( rng ( upper_sum_set ((f `| X) || A)))) by A5, SEQ_4: 43;

      then

       A7: ( upper_integral ((f `| X) || A)) >= ((f . ( upper_bound A)) - (f . ( lower_bound A))) by INTEGRA1:def 14;

      

       A8: for r be Real st r in ( rng ( lower_sum_set ((f `| X) || A))) holds r <= ((f . ( upper_bound A)) - (f . ( lower_bound A)))

      proof

        let r be Real;

        assume r in ( rng ( lower_sum_set ((f `| X) || A)));

        then

        consider D be Element of ( divs A) such that

         A9: D in ( dom ( lower_sum_set ((f `| X) || A))) & r = (( lower_sum_set ((f `| X) || A)) . D) by PARTFUN1: 3;

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

        r = ( lower_sum (((f `| X) || A),D)) by A9, INTEGRA1:def 11;

        hence thesis by A1, A3, Th12;

      end;

      ( upper_bound ( rng ( lower_sum_set ((f `| X) || A)))) <= ((f . ( upper_bound A)) - (f . ( lower_bound A))) by A8, SEQ_4: 45;

      then ( upper_integral ((f `| X) || A)) <= ((f . ( upper_bound A)) - (f . ( lower_bound A))) by A4, INTEGRA1:def 15;

      then ( upper_integral ((f `| X) || A)) = ((f . ( upper_bound A)) - (f . ( lower_bound A))) by A7, XXREAL_0: 1;

      hence thesis by INTEGRA1:def 17;

    end;

    theorem :: INTEGRA5:14

    

     Th14: for f be PartFunc of REAL , REAL st (f | A) is non-decreasing & A c= ( dom f) holds ( rng (f | A)) is real-bounded

    proof

      let f be PartFunc of REAL , REAL ;

      assume that

       A1: (f | A) is non-decreasing and

       A2: A c= ( dom f);

      

       A3: ( dom (f | A)) = (( dom f) /\ A) by RELAT_1: 61

      .= A by A2, XBOOLE_1: 28;

      (f . ( lower_bound A)) is LowerBound of ( rng (f | A))

      proof

        ( lower_bound A) <= ( upper_bound A) by SEQ_4: 11;

        then ( lower_bound A) in ( dom (f | A)) by A3, INTEGRA2: 1;

        then

         A4: ( lower_bound A) in (( dom f) /\ A) by RELAT_1: 61;

        let y be ExtReal;

        assume y in ( rng (f | A));

        then

        consider x be Element of REAL such that

         A5: x in ( dom (f | A)) and

         A6: y = ((f | A) . x) by PARTFUN1: 3;

        

         A7: x in (( dom f) /\ A) by A5, RELAT_1: 61;

        y = (f . x) & x >= ( lower_bound A) by A5, A6, FUNCT_1: 47, INTEGRA2: 1;

        hence thesis by A1, A7, A4, RFUNCT_2: 24;

      end;

      then

       A8: ( rng (f | A)) is bounded_below;

      (f . ( upper_bound A)) is UpperBound of ( rng (f | A))

      proof

        ( lower_bound A) <= ( upper_bound A) by SEQ_4: 11;

        then ( upper_bound A) in ( dom (f | A)) by A3, INTEGRA2: 1;

        then

         A9: ( upper_bound A) in (( dom f) /\ A) by RELAT_1: 61;

        let y be ExtReal;

        assume y in ( rng (f | A));

        then

        consider x be Element of REAL such that

         A10: x in ( dom (f | A)) and

         A11: y = ((f | A) . x) by PARTFUN1: 3;

        

         A12: x in (( dom f) /\ A) by A10, RELAT_1: 61;

        y = (f . x) & x <= ( upper_bound A) by A10, A11, FUNCT_1: 47, INTEGRA2: 1;

        hence thesis by A1, A12, A9, RFUNCT_2: 24;

      end;

      then ( rng (f | A)) is bounded_above;

      hence thesis by A8;

    end;

    theorem :: INTEGRA5:15

    

     Th15: for f be PartFunc of REAL , REAL st (f | A) is non-decreasing & A c= ( dom f) holds ( lower_bound ( rng (f | A))) = (f . ( lower_bound A)) & ( upper_bound ( rng (f | A))) = (f . ( upper_bound A))

    proof

      let f be PartFunc of REAL , REAL ;

      assume that

       A1: (f | A) is non-decreasing and

       A2: A c= ( dom f);

      

       A3: ( dom (f | A)) = (( dom f) /\ A) by RELAT_1: 61

      .= A by A2, XBOOLE_1: 28;

      then

       A4: ( rng (f | A)) <> {} by RELAT_1: 42;

      

       A5: ( lower_bound A) <= ( upper_bound A) by SEQ_4: 11;

      then

       A6: ( upper_bound A) in ( dom (f | A)) by A3, INTEGRA2: 1;

      then

       A7: ( upper_bound A) in (( dom f) /\ A) by RELAT_1: 61;

      

       A8: for x be Real st x in ( rng (f | A)) holds x <= (f . ( upper_bound A))

      proof

        let y be Real;

        assume y in ( rng (f | A));

        then

        consider x be Element of REAL such that

         A9: x in ( dom (f | A)) and

         A10: y = ((f | A) . x) by PARTFUN1: 3;

        x in (( dom f) /\ A) & ( upper_bound A) >= x by A9, INTEGRA2: 1, RELAT_1: 61;

        then (f . ( upper_bound A)) >= (f . x) by A1, A7, RFUNCT_2: 24;

        hence thesis by A9, A10, FUNCT_1: 47;

      end;

      

       A11: ( lower_bound A) in ( dom (f | A)) by A3, A5, INTEGRA2: 1;

      then

       A12: ( lower_bound A) in (( dom f) /\ A) by RELAT_1: 61;

      

       A13: for y be Real st y in ( rng (f | A)) holds y >= (f . ( lower_bound A))

      proof

        let y be Real;

        assume y in ( rng (f | A));

        then

        consider x be Element of REAL such that

         A14: x in ( dom (f | A)) and

         A15: y = ((f | A) . x) by PARTFUN1: 3;

        x in (( dom f) /\ A) & ( lower_bound A) <= x by A14, INTEGRA2: 1, RELAT_1: 61;

        then (f . ( lower_bound A)) <= (f . x) by A1, A12, RFUNCT_2: 24;

        hence thesis by A14, A15, FUNCT_1: 47;

      end;

      for a be Real st for x be Real st x in ( rng (f | A)) holds x >= a holds (f . ( lower_bound A)) >= a

      proof

        let a be Real;

        assume

         A16: for x be Real st x in ( rng (f | A)) holds x >= a;

        (f . ( lower_bound A)) = ((f | A) . ( lower_bound A)) & ((f | A) . ( lower_bound A)) in ( rng (f | A)) by A11, FUNCT_1: 47, FUNCT_1:def 3;

        hence thesis by A16;

      end;

      hence ( lower_bound ( rng (f | A))) = (f . ( lower_bound A)) by A4, A13, SEQ_4: 44;

      for a be Real st for x be Real st x in ( rng (f | A)) holds x <= a holds (f . ( upper_bound A)) <= a

      proof

        let a be Real;

        assume

         A17: for x be Real st x in ( rng (f | A)) holds x <= a;

        (f . ( upper_bound A)) = ((f | A) . ( upper_bound A)) & ((f | A) . ( upper_bound A)) in ( rng (f | A)) by A6, FUNCT_1: 47, FUNCT_1:def 3;

        hence thesis by A17;

      end;

      hence thesis by A4, A8, SEQ_4: 46;

    end;

    

     Lm1: for f be PartFunc of REAL , REAL st (f | A) is non-decreasing & A c= ( dom f) holds f is_integrable_on A

    proof

      let f be PartFunc of REAL , REAL ;

      assume that

       A1: (f | A) is non-decreasing and

       A2: A c= ( dom f);

      

       A3: for D be Division of A, k st k in ( dom D) holds 0 <= ((( upper_volume ((f || A),D)) . k) - (( lower_volume ((f || A),D)) . k)) & ((( upper_volume ((f || A),D)) . k) - (( lower_volume ((f || A),D)) . k)) <= (((f . ( upper_bound ( divset (D,k)))) - (f . ( lower_bound ( divset (D,k))))) * ( delta D))

      proof

        let D be Division of A;

        let k;

        assume

         A4: k in ( dom D);

        then

         A5: (( upper_volume ((f || A),D)) . k) = (( upper_bound ( rng ((f || A) | ( divset (D,k))))) * ( vol ( divset (D,k)))) & (( lower_volume ((f || A),D)) . k) = (( lower_bound ( rng ((f || A) | ( divset (D,k))))) * ( vol ( divset (D,k)))) by INTEGRA1:def 6, INTEGRA1:def 7;

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

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

        then

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

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

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

        then ( vol ( divset (D,k))) <= ( max ( rng ( upper_volume (( chi (A,A)),D)))) by XXREAL_2:def 8;

        then

         A7: ( vol ( divset (D,k))) <= ( delta D) by INTEGRA3:def 1;

        

         A8: ( divset (D,k)) c= A by A4, INTEGRA1: 8;

        then

         A9: ( divset (D,k)) c= ( dom f) by A2, XBOOLE_1: 1;

        (f | ( divset (D,k))) is non-decreasing by A1, A4, INTEGRA1: 8, RFUNCT_2: 30;

        then

         A10: ( lower_bound ( rng (f | ( divset (D,k))))) = (f . ( lower_bound ( divset (D,k)))) & ( upper_bound ( rng (f | ( divset (D,k))))) = (f . ( upper_bound ( divset (D,k)))) by A9, Th15;

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

        .= ( divset (D,k)) by A2, A8, XBOOLE_1: 1, XBOOLE_1: 28;

        then

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

        

         A12: ( rng (f | ( divset (D,k)))) = ( rng ((f || A) | ( divset (D,k)))) by A8, FUNCT_1: 51;

        ( rng (f | A)) is real-bounded by A1, A2, Th14;

        then ( rng (f | ( divset (D,k)))) is real-bounded by A12, RELAT_1: 70, XXREAL_2: 45;

        then

         A13: ((f . ( upper_bound ( divset (D,k)))) - (f . ( lower_bound ( divset (D,k))))) >= 0 by A10, A11, SEQ_4: 11, XREAL_1: 48;

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

        then ( 0 * ( vol ( divset (D,k)))) <= (((f . ( upper_bound ( divset (D,k)))) - (f . ( lower_bound ( divset (D,k))))) * ( vol ( divset (D,k)))) by A13;

        hence 0 <= ((( upper_volume ((f || A),D)) . k) - (( lower_volume ((f || A),D)) . k)) by A10, A5, A12;

        ((( upper_volume ((f || A),D)) . k) - (( lower_volume ((f || A),D)) . k)) = (((f . ( upper_bound ( divset (D,k)))) - (f . ( lower_bound ( divset (D,k))))) * ( vol ( divset (D,k)))) by A10, A5, A12;

        hence thesis by A13, A7, XREAL_1: 64;

      end;

      

       A14: for D be Division of A holds (( upper_sum ((f || A),D)) - ( lower_sum ((f || A),D))) <= (( delta D) * ((f . ( upper_bound A)) - (f . ( lower_bound A)))) & (( upper_sum ((f || A),D)) - ( lower_sum ((f || A),D))) >= 0

      proof

        let D be Division of A;

        deffunc F2( Nat) = ( In ((f . ( upper_bound ( divset (D,$1)))), REAL ));

        consider F1 be FinSequence of REAL such that

         A15: ( len F1) = ( len D) & for i be Nat st i in ( dom F1) holds (F1 . i) = F2(i) from FINSEQ_2:sch 1;

        (( len D) - 1) in NAT

        proof

          ex j be Nat st ( len D) = (1 + j) by NAT_1: 10, NAT_1: 14;

          hence thesis by ORDINAL1:def 12;

        end;

        then

        consider k1 be Element of NAT such that

         A16: k1 = (( len D) - 1);

        deffunc G( Nat) = ( In ((f . ( lower_bound ( divset (D,$1)))), REAL ));

        consider F2 be FinSequence of REAL such that

         A17: ( len F2) = ( len D) & for i be Nat st i in ( dom F2) holds (F2 . i) = G(i) from FINSEQ_2:sch 1;

        deffunc G1( Nat) = ( In ((f . ( upper_bound ( divset (D,$1)))), REAL ));

        

         A18: ( dom F2) = ( Seg ( len D)) by A17, FINSEQ_1:def 3;

        consider F be FinSequence of REAL such that

         A19: ( len F) = k1 & for i be Nat st i in ( dom F) holds (F . i) = G1(i) from FINSEQ_2:sch 1;

        

         A20: ( dom F) = ( Seg k1) by A19, FINSEQ_1:def 3;

        

         A21: for i be Nat st 1 <= i & i <= ( len F2) holds (F2 . i) = (( <*(f . ( lower_bound A))*> ^ F) . i)

        proof

          let i be Nat;

          assume that

           A22: 1 <= i and

           A23: i <= ( len F2);

          per cases ;

            suppose

             A24: i = 1;

            

             A25: i in ( Seg ( len D)) by A17, A22, A23, FINSEQ_1: 1;

            then

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

            (F2 . i) = G(i) by A17, A18, A25

            .= (f . ( lower_bound ( divset (D,i))))

            .= (f . ( lower_bound A)) by A24, A26, INTEGRA1:def 4;

            hence thesis by A24, FINSEQ_1: 41;

          end;

            suppose

             A27: i <> 1;

            then

             A28: i > 1 by A22, XXREAL_0: 1;

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

            then

             A29: (( len <*(f . ( lower_bound A))*>) + 1) <= i by FINSEQ_1: 39;

            

             A30: i in ( Seg ( len D)) by A17, A22, A23, FINSEQ_1: 1;

            then

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

            then

            reconsider k2 = (i - 1) as Element of NAT by A27, INTEGRA1: 7;

            (1 + 1) <= (k2 + 1) by A28, NAT_1: 13;

            then

             A32: 1 <= k2 by XREAL_1: 19;

            (k2 + 1) <= ( len F2) by A23;

            then

             A33: k2 <= (( len D) - 1) by A17, XREAL_1: 19;

            then

             A34: k2 in ( Seg k1) by A16, A32, FINSEQ_1: 1;

            

             A35: ( upper_bound ( divset (D,k2))) = (D . (i - 1))

            proof

              ( len D) <= (( len D) + 1) by NAT_1: 13;

              then (( len D) - 1) <= ( len D) by XREAL_1: 20;

              then k2 <= ( len D) by A33, XXREAL_0: 2;

              then k2 in ( Seg ( len D)) by A32, FINSEQ_1: 1;

              then

               A36: k2 in ( dom D) by FINSEQ_1:def 3;

              per cases ;

                suppose k2 = 1;

                hence thesis by A36, INTEGRA1:def 4;

              end;

                suppose k2 <> 1;

                hence thesis by A36, INTEGRA1:def 4;

              end;

            end;

            ( len F2) = (1 + (( len D) - 1)) by A17

            .= (( len <*(f . ( lower_bound A))*>) + ( len F)) by A16, A19, FINSEQ_1: 39;

            

            then

             A37: (( <*(f . ( lower_bound A))*> ^ F) . i) = (F . (i - ( len <*(f . ( lower_bound A))*>))) by A23, A29, FINSEQ_1: 23

            .= (F . (i - 1)) by FINSEQ_1: 39;

            (F2 . i) = G(i) by A17, A18, A30

            .= (f . ( lower_bound ( divset (D,i))))

            .= (f . ( upper_bound ( divset (D,k2)))) by A27, A31, INTEGRA1:def 4, A35

            .= G1(k2);

            hence thesis by A19, A20, A37, A34;

          end;

        end;

        ( len ( <*(f . ( lower_bound A))*> ^ F)) = (( len <*(f . ( lower_bound A))*>) + ( len F)) by FINSEQ_1: 22

        .= (1 + (( len D) - 1)) by A16, A19, FINSEQ_1: 39

        .= ( len D);

        then

         A38: F2 = ( <*(f . ( lower_bound A))*> ^ F) by A17, A21, FINSEQ_1: 14;

        ( len ( upper_volume ((f || A),D))) = ( len D) & ( len ( lower_volume ((f || A),D))) = ( len D) by INTEGRA1:def 6, INTEGRA1:def 7;

        

        then

         A39: ( Sum (( upper_volume ((f || A),D)) - ( lower_volume ((f || A),D)))) = (( Sum ( upper_volume ((f || A),D))) - ( Sum ( lower_volume ((f || A),D)))) by Th2

        .= (( upper_sum ((f || A),D)) - ( Sum ( lower_volume ((f || A),D)))) by INTEGRA1:def 8

        .= (( upper_sum ((f || A),D)) - ( lower_sum ((f || A),D))) by INTEGRA1:def 9;

        

         A40: ( dom F1) = ( Seg ( len D)) by A15, FINSEQ_1:def 3;

        

         A41: for i be Nat st 1 <= i & i <= ( len F1) holds (F1 . i) = ((F ^ <*(f . ( upper_bound A))*>) . i)

        proof

          let i be Nat;

          assume that

           A42: 1 <= i and

           A43: i <= ( len F1);

          now

            per cases ;

              suppose i <= ( len F);

              then

               A44: i in ( Seg ( len F)) by A42, FINSEQ_1: 1;

              

              then

               A45: (F . i) = G1(i) by A19, A20

              .= (f . ( upper_bound ( divset (D,i))));

              

               A46: i in ( dom F) by A19, A20, A44;

              i in ( Seg ( len F1)) by A42, A43, FINSEQ_1: 1;

              

              then (F1 . i) = F2(i) by A15, A40

              .= (f . ( upper_bound ( divset (D,i))));

              hence thesis by A46, A45, FINSEQ_1:def 7;

            end;

              suppose i > ( len F);

              then

               A47: i >= (( len F) + 1) by NAT_1: 13;

              then

               A48: i = (( len F) + 1) by A15, A16, A19, A43, XXREAL_0: 1;

              

               A49: i in ( Seg ( len F1)) by A42, A43, FINSEQ_1: 1;

              then

               A50: i in ( dom D) by A15, FINSEQ_1:def 3;

              

               A51: ( upper_bound ( divset (D,i))) = (D . i)

              proof

                now

                  per cases ;

                    suppose i = 1;

                    hence thesis by A50, INTEGRA1:def 4;

                  end;

                    suppose i <> 1;

                    hence thesis by A50, INTEGRA1:def 4;

                  end;

                end;

                hence thesis;

              end;

              (F1 . i) = F2(i) by A15, A40, A49

              .= (f . ( upper_bound ( divset (D,i))));

              

              then (F1 . i) = (f . (D . ( len D))) by A15, A16, A19, A43, A47, A51, XXREAL_0: 1

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

              hence thesis by A48, FINSEQ_1: 42;

            end;

          end;

          hence thesis;

        end;

        ( len ( upper_volume ((f || A),D))) = ( len D) & ( len ( lower_volume ((f || A),D))) = ( len D) by INTEGRA1:def 6, INTEGRA1:def 7;

        then

         A52: ( len (( upper_volume ((f || A),D)) - ( lower_volume ((f || A),D)))) = ( len D) by Th2;

        

         A53: ( len (F1 - F2)) = ( len D) by A15, A17, Th2;

        

         A54: for k st k in ( dom (( upper_volume ((f || A),D)) - ( lower_volume ((f || A),D)))) holds ((( upper_volume ((f || A),D)) - ( lower_volume ((f || A),D))) . k) <= ((( delta D) * (F1 - F2)) . k)

        proof

          let k;

          assume

           A55: k in ( dom (( upper_volume ((f || A),D)) - ( lower_volume ((f || A),D))));

          then k in ( Seg ( len (F1 - F2))) by A52, A53, FINSEQ_1:def 3;

          then

           A56: k in ( dom (F1 - F2)) by FINSEQ_1:def 3;

          

           A57: k in ( Seg ( len D)) by A52, A55, FINSEQ_1:def 3;

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

          then ((( upper_volume ((f || A),D)) . k) - (( lower_volume ((f || A),D)) . k)) <= (((f . ( upper_bound ( divset (D,k)))) - (f . ( lower_bound ( divset (D,k))))) * ( delta D)) by A3;

          then

           A58: ((( upper_volume ((f || A),D)) - ( lower_volume ((f || A),D))) . k) <= (((f . ( upper_bound ( divset (D,k)))) - (f . ( lower_bound ( divset (D,k))))) * ( delta D)) by A55, VALUED_1: 13;

          

           A59: (F1 . k) = F2(k) by A15, A40, A57

          .= (f . ( upper_bound ( divset (D,k))));

          (F2 . k) = G(k) by A17, A18, A57

          .= (f . ( lower_bound ( divset (D,k))));

          then ((( upper_volume ((f || A),D)) - ( lower_volume ((f || A),D))) . k) <= (( delta D) * ((F1 - F2) . k)) by A58, A56, VALUED_1: 13, A59;

          hence thesis by RVSUM_1: 44;

        end;

        (( delta D) * (F1 - F2)) = ((( delta D) multreal ) * (F1 - F2)) by RVSUM_1:def 7;

        then ( len (( delta D) * (F1 - F2))) = ( len (F1 - F2)) by FINSEQ_2: 33;

        then ( len (( upper_volume ((f || A),D)) - ( lower_volume ((f || A),D)))) = ( len (( delta D) * (F1 - F2))) by A15, A17, A52, Th2;

        then

         A60: ( Sum (( upper_volume ((f || A),D)) - ( lower_volume ((f || A),D)))) <= ( Sum (( delta D) * (F1 - F2))) by A54, Th3;

        ( len (F ^ <*(f . ( upper_bound A))*>)) = (( len F) + ( len <*(f . ( upper_bound A))*>)) by FINSEQ_1: 22

        .= ((( len D) - 1) + 1) by A16, A19, FINSEQ_1: 39

        .= ( len D);

        then F1 = (F ^ <*(f . ( upper_bound A))*>) by A15, A41, FINSEQ_1: 14;

        then ( Sum (F1 - F2)) = ((f . ( upper_bound A)) - (f . ( lower_bound A))) by A38, Th1;

        hence (( upper_sum ((f || A),D)) - ( lower_sum ((f || A),D))) <= (( delta D) * ((f . ( upper_bound A)) - (f . ( lower_bound A)))) by A39, A60, RVSUM_1: 87;

        for k be Nat st k in ( dom (( upper_volume ((f || A),D)) - ( lower_volume ((f || A),D)))) holds 0 <= ((( upper_volume ((f || A),D)) - ( lower_volume ((f || A),D))) . k)

        proof

          let k be Nat;

          set r = ((( upper_volume ((f || A),D)) - ( lower_volume ((f || A),D))) . k);

          

           A61: ( len ( upper_volume ((f || A),D))) = ( len D) & ( len ( lower_volume ((f || A),D))) = ( len D) by INTEGRA1:def 6, INTEGRA1:def 7;

          assume

           A62: k in ( dom (( upper_volume ((f || A),D)) - ( lower_volume ((f || A),D))));

          then k in ( Seg ( len (( upper_volume ((f || A),D)) - ( lower_volume ((f || A),D))))) by FINSEQ_1:def 3;

          then k in ( Seg ( len D)) by A61, Th2;

          then

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

          r = ((( upper_volume ((f || A),D)) . k) - (( lower_volume ((f || A),D)) . k)) by A62, VALUED_1: 13;

          hence thesis by A3, A63;

        end;

        hence thesis by A39, RVSUM_1: 84;

      end;

      

       A64: (f || A) is total & ((f || A) | A) is bounded

      proof

        consider x be Element of REAL such that

         A65: x in A by SUBSET_1: 4;

        

         A66: ( dom (f || A)) = (( dom f) /\ A) by RELAT_1: 61

        .= A by A2, XBOOLE_1: 28;

        hence (f || A) is total by PARTFUN1:def 2;

        ( lower_bound A) <= x & x <= ( upper_bound A) by A65, INTEGRA2: 1;

        then

         A67: ( lower_bound A) <= ( upper_bound A) by XXREAL_0: 2;

        for x be object st x in (A /\ ( dom (f || A))) holds ((f || A) . x) >= ((f || A) . ( lower_bound A))

        proof

          ( lower_bound A) in A by A67, INTEGRA2: 1;

          then

           A68: ( lower_bound A) in (A /\ ( dom f)) & (f . ( lower_bound A)) = ((f | A) . ( lower_bound A)) by A2, A66, FUNCT_1: 47, XBOOLE_1: 28;

          let x be object;

          assume

           A69: x in (A /\ ( dom (f || A)));

          then x in A;

          then

           A70: x in (A /\ ( dom f)) by A2, XBOOLE_1: 28;

          reconsider x as Element of A by A69;

          x >= ( lower_bound A) & (f . x) = ((f | A) . x) by A66, FUNCT_1: 47, INTEGRA2: 1;

          hence thesis by A1, A70, A68, RFUNCT_2: 24;

        end;

        then

         A71: ((f || A) | A) is bounded_below by RFUNCT_1: 71;

        for x be object st x in (A /\ ( dom (f || A))) holds ((f || A) . x) <= ((f || A) . ( upper_bound A))

        proof

          ( upper_bound A) in A by A67, INTEGRA2: 1;

          then

           A72: ( upper_bound A) in (A /\ ( dom f)) & (f . ( upper_bound A)) = ((f | A) . ( upper_bound A)) by A2, A66, FUNCT_1: 47, XBOOLE_1: 28;

          let x be object;

          assume

           A73: x in (A /\ ( dom (f || A)));

          then x in A;

          then

           A74: x in (A /\ ( dom f)) by A2, XBOOLE_1: 28;

          reconsider x as Element of A by A73;

          x <= ( upper_bound A) & (f . x) = ((f | A) . x) by A66, FUNCT_1: 47, INTEGRA2: 1;

          hence thesis by A1, A74, A72, RFUNCT_2: 24;

        end;

        then ((f || A) | A) is bounded_above by RFUNCT_1: 70;

        hence thesis by A71;

      end;

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

      proof

        let T be DivSequence of A;

        assume

         A75: ( delta T) is convergent & ( lim ( delta T)) = 0 ;

        

         A76: for r be Real st 0 < r holds ex n be Nat st for m be Nat st n <= m holds |.(((( upper_sum ((f || A),T)) - ( lower_sum ((f || A),T))) . m) - 0 ).| < r

        proof

          consider x be Element of REAL such that

           A77: x in A by SUBSET_1: 4;

          

           A78: A = (A /\ ( dom f)) by A2, XBOOLE_1: 28;

          let r be Real;

          assume

           A79: 0 < r;

          ( lower_bound A) <= x & x <= ( upper_bound A) by A77, INTEGRA2: 1;

          then

           A80: ( lower_bound A) <= ( upper_bound A) by XXREAL_0: 2;

          then ( lower_bound A) in A & ( upper_bound A) in A by INTEGRA2: 1;

          then

           A81: (f . ( lower_bound A)) <= (f . ( upper_bound A)) by A1, A80, A78, RFUNCT_2: 24;

          per cases by A81, XXREAL_0: 1;

            suppose

             A82: (f . ( lower_bound A)) = (f . ( upper_bound A));

            reconsider n = 0 as Nat;

            take n;

            let m be Nat;

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

            assume n <= m;

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

            

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

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

            .= (( upper_sum ((f || A),D1)) + ( - (( lower_sum ((f || A),T)) . m))) by INTEGRA2:def 2

            .= (( upper_sum ((f || A),D1)) + ( - ( lower_sum ((f || A),D1)))) by INTEGRA2:def 3;

            (( upper_sum ((f || A),D1)) - ( lower_sum ((f || A),D1))) <= (( delta D1) * ((f . ( upper_bound A)) - (f . ( lower_bound A)))) & (( upper_sum ((f || A),D1)) - ( lower_sum ((f || A),D1))) >= 0 by A14;

            hence thesis by A79, A82, A83, ABSVALUE:def 1;

          end;

            suppose (f . ( lower_bound A)) < (f . ( upper_bound A));

            then

             A84: ((f . ( upper_bound A)) - (f . ( lower_bound A))) > 0 by XREAL_1: 50;

            then (r / ((f . ( upper_bound A)) - (f . ( lower_bound A)))) > 0 by A79, XREAL_1: 139;

            then

            consider n be Nat such that

             A85: for m be Nat st n <= m holds |.((( delta T) . m) - 0 ).| < (r / ((f . ( upper_bound A)) - (f . ( lower_bound A)))) by A75, SEQ_2:def 7;

            

             A86: for m st n <= m holds (( delta T) . m) < (r / ((f . ( upper_bound A)) - (f . ( lower_bound A))))

            proof

              let m;

              assume n <= m;

              then

               A87: |.((( delta T) . m) - 0 ).| < (r / ((f . ( upper_bound A)) - (f . ( lower_bound A)))) by A85;

              (( delta T) . m) <= |.(( delta T) . m).| by ABSVALUE: 4;

              hence thesis by A87, XXREAL_0: 2;

            end;

            take n;

            let m be Nat;

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

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

            

             A88: |.(( upper_sum ((f || A),D)) - ( lower_sum ((f || A),D))).| = |.(((( upper_sum ((f || A),T)) . mm) - ( lower_sum ((f || A),D))) - 0 ).| by INTEGRA2:def 2

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

            .= |.(((( upper_sum ((f || A),T)) . m) + ( - (( lower_sum ((f || A),T)) . m))) - 0 ).|

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

            .= |.(((( upper_sum ((f || A),T)) - ( lower_sum ((f || A),T))) . m) - 0 ).| by SEQ_1: 7;

            assume n <= m;

            then (( delta T) . mm) < (r / ((f . ( upper_bound A)) - (f . ( lower_bound A)))) by A86;

            then ((( delta T) . m) * ((f . ( upper_bound A)) - (f . ( lower_bound A)))) < r by A84, XREAL_1: 79;

            then

             A89: (( delta D) * ((f . ( upper_bound A)) - (f . ( lower_bound A)))) < r by INTEGRA3:def 2;

            (( upper_sum ((f || A),D)) - ( lower_sum ((f || A),D))) <= (( delta D) * ((f . ( upper_bound A)) - (f . ( lower_bound A)))) by A14;

            then

             A90: (( upper_sum ((f || A),D)) - ( lower_sum ((f || A),D))) < r by A89, XXREAL_0: 2;

            (( upper_sum ((f || A),D)) - ( lower_sum ((f || A),D))) >= 0 by A14;

            hence thesis by A90, A88, ABSVALUE:def 1;

          end;

        end;

        

         A91: ( upper_sum ((f || A),T)) is convergent & ( lower_sum ((f || A),T)) is convergent by A64, A75, INTEGRA4: 8, INTEGRA4: 9;

        then (( upper_sum ((f || A),T)) - ( lower_sum ((f || A),T))) is convergent;

        then ( lim (( upper_sum ((f || A),T)) - ( lower_sum ((f || A),T)))) = 0 by A76, SEQ_2:def 7;

        hence thesis by A91, SEQ_2: 12;

      end;

      then (f || A) is integrable by A64, INTEGRA4: 12;

      hence thesis;

    end;

    theorem :: INTEGRA5:16

    for f be PartFunc of REAL , REAL st (f | A) is monotone & A c= ( dom f) holds f is_integrable_on A

    proof

      let f be PartFunc of REAL , REAL ;

      assume that

       A1: (f | A) is monotone and

       A2: A c= ( dom f);

      per cases by A1, RFUNCT_2:def 5;

        suppose (f | A) is non-decreasing;

        hence thesis by A2, Lm1;

      end;

        suppose (f | A) is non-increasing;

        then

         A3: ((( - 1) (#) f) | A) is non-decreasing by RFUNCT_2: 35;

        

         A4: (( - f) || A) is total & ((( - f) || A) | A) is bounded

        proof

          consider x be Element of REAL such that

           A5: x in A by SUBSET_1: 4;

          

           A6: ( dom (( - f) || A)) = (( dom ( - f)) /\ A) by RELAT_1: 61

          .= (( dom f) /\ A) by VALUED_1: 8

          .= A by A2, XBOOLE_1: 28;

          hence (( - f) || A) is total by PARTFUN1:def 2;

          ( lower_bound A) <= x & x <= ( upper_bound A) by A5, INTEGRA2: 1;

          then

           A7: ( lower_bound A) <= ( upper_bound A) by XXREAL_0: 2;

          for x be object st x in (A /\ ( dom (( - f) || A))) holds ((( - f) || A) . x) >= ((( - f) || A) . ( lower_bound A))

          proof

            let x be object;

            assume x in (A /\ ( dom (( - f) || A)));

            then

            reconsider x as Element of A;

            

             A8: x >= ( lower_bound A) & (( - f) . x) = ((( - f) | A) . x) by A6, FUNCT_1: 47, INTEGRA2: 1;

            ( lower_bound A) in A by A7, INTEGRA2: 1;

            then

             A9: (( - f) . ( lower_bound A)) = ((( - f) | A) . ( lower_bound A)) by A6, FUNCT_1: 47;

            

             A10: A = (A /\ ( dom f)) by A2, XBOOLE_1: 28

            .= (A /\ ( dom ( - f))) by VALUED_1: 8;

            then ( lower_bound A) in (A /\ ( dom ( - f))) by A7, INTEGRA2: 1;

            hence thesis by A3, A10, A8, A9, RFUNCT_2: 24;

          end;

          then

           A11: ((( - f) || A) | A) is bounded_below by RFUNCT_1: 71;

          for x be object st x in (A /\ ( dom (( - f) || A))) holds ((( - f) || A) . x) <= ((( - f) || A) . ( upper_bound A))

          proof

            let x be object;

            assume x in (A /\ ( dom (( - f) || A)));

            then

            reconsider x as Element of A;

            

             A12: x <= ( upper_bound A) & (( - f) . x) = ((( - f) | A) . x) by A6, FUNCT_1: 47, INTEGRA2: 1;

            ( upper_bound A) in A by A7, INTEGRA2: 1;

            then

             A13: (( - f) . ( upper_bound A)) = ((( - f) | A) . ( upper_bound A)) by A6, FUNCT_1: 47;

            

             A14: A = (A /\ ( dom f)) by A2, XBOOLE_1: 28

            .= (A /\ ( dom ( - f))) by VALUED_1: 8;

            then ( upper_bound A) in (A /\ ( dom ( - f))) by A7, INTEGRA2: 1;

            hence thesis by A3, A14, A12, A13, RFUNCT_2: 24;

          end;

          then ((( - f) || A) | A) is bounded_above by RFUNCT_1: 70;

          hence thesis by A11;

        end;

        ( dom f) = ( dom ( - f)) by VALUED_1: 8;

        then ( - f) is_integrable_on A by A2, A3, Lm1;

        then (( - f) || A) is integrable;

        then

         A15: (( - 1) (#) (( - f) || A)) is integrable by A4, INTEGRA2: 31;

        

         A16: ( dom (( - f) || A)) = (( dom ( - f)) /\ A) by RELAT_1: 61

        .= (( dom f) /\ A) by VALUED_1: 8

        .= A by A2, XBOOLE_1: 28;

        then

         A17: A = ( dom (( - 1) (#) (( - f) || A))) by VALUED_1:def 5;

        

         A18: ( dom (f || A)) = (( dom f) /\ A) by RELAT_1: 61;

        then

         A19: ( dom (f || A)) = A by A2, XBOOLE_1: 28;

        

         A20: ( dom (( - 1) (#) (( - f) || A))) = A by A16, VALUED_1:def 5;

        

         A21: for z be Element of A st z in A holds ((( - 1) (#) (( - f) || A)) . z) = ((f || A) . z)

        proof

          let z be Element of A;

          assume z in A;

          ((( - f) || A) . z) = (( - f) . z) by A16, FUNCT_1: 47

          .= ( - (f . z)) by VALUED_1: 8;

          

          then ((( - 1) (#) (( - f) || A)) . z) = (( - 1) * ( - (f . z))) by A20, VALUED_1:def 5

          .= (f . z);

          hence thesis by A19, FUNCT_1: 47;

        end;

        A = ( dom (f || A)) by A2, A18, XBOOLE_1: 28;

        then (( - 1) (#) (( - f) || A)) = (f || A) by A21, A17, PARTFUN1: 5;

        hence thesis by A15;

      end;

    end;

    theorem :: INTEGRA5:17

    for f be PartFunc of REAL , REAL , A,B be non empty closed_interval Subset of REAL st A c= ( dom f) & (f | A) is continuous & B c= A holds f is_integrable_on B

    proof

      let f be PartFunc of REAL , REAL , A,B be non empty closed_interval Subset of REAL such that

       A1: A c= ( dom f) and

       A2: (f | A) is continuous and

       A3: B c= A;

      (f | B) is continuous by A2, A3, FCONT_1: 16;

      hence thesis by A1, A3, Th11, XBOOLE_1: 1;

    end;

    theorem :: INTEGRA5:18

    for f be PartFunc of REAL , REAL , A,B,C be non empty closed_interval Subset of REAL , X st A c= X & f is_differentiable_on X & ((f `| X) | A) is continuous & ( lower_bound A) = ( lower_bound B) & ( upper_bound B) = ( lower_bound C) & ( upper_bound C) = ( upper_bound A) holds B c= A & C c= A & ( integral ((f `| X),A)) = (( integral ((f `| X),B)) + ( integral ((f `| X),C)))

    proof

      let f be PartFunc of REAL , REAL ;

      let A,B,C be non empty closed_interval Subset of REAL ;

      let X;

      assume that

       A1: A c= X & f is_differentiable_on X and

       A2: ((f `| X) | A) is continuous and

       A3: ( lower_bound A) = ( lower_bound B) and

       A4: ( upper_bound B) = ( lower_bound C) and

       A5: ( upper_bound C) = ( upper_bound A);

      consider x be Element of REAL such that

       A6: x in B by SUBSET_1: 4;

      ( lower_bound B) <= x & x <= ( upper_bound B) by A6, INTEGRA2: 1;

      then

       A7: ( lower_bound B) <= ( upper_bound B) by XXREAL_0: 2;

      consider x be Element of REAL such that

       A8: x in C by SUBSET_1: 4;

      ( lower_bound C) <= x & x <= ( upper_bound C) by A8, INTEGRA2: 1;

      then

       A9: ( lower_bound C) <= ( upper_bound C) by XXREAL_0: 2;

      for x be object st x in B holds x in A

      proof

        let x be object;

        assume

         A10: x in B;

        then

        reconsider x as Real;

        x <= ( upper_bound B) by A10, INTEGRA2: 1;

        then

         A11: x <= ( upper_bound A) by A4, A5, A9, XXREAL_0: 2;

        ( lower_bound A) <= x by A3, A10, INTEGRA2: 1;

        hence thesis by A11, INTEGRA2: 1;

      end;

      hence

       A12: B c= A by TARSKI:def 3;

      

       A13: A c= ( dom (f `| X)) by A1, FDIFF_1:def 7;

      then

       A14: ((f `| X) | A) is bounded by A2, Th10;

      then

       A15: ((f `| X) | B) is bounded by A12, RFUNCT_1: 74;

      for x be object st x in C holds x in A

      proof

        let x be object;

        assume

         A16: x in C;

        then

        reconsider x as Real;

        ( lower_bound C) <= x by A16, INTEGRA2: 1;

        then

         A17: ( lower_bound A) <= x by A3, A4, A7, XXREAL_0: 2;

        x <= ( upper_bound A) by A5, A16, INTEGRA2: 1;

        hence thesis by A17, INTEGRA2: 1;

      end;

      hence

       A18: C c= A by TARSKI:def 3;

      then

       A19: ((f `| X) | C) is bounded by A14, RFUNCT_1: 74;

      ((f `| X) | C) is continuous by A2, A18, FCONT_1: 16;

      then (f `| X) is_integrable_on C by A13, A18, Th11, XBOOLE_1: 1;

      then

       A20: ( integral ((f `| X),C)) = ((f . ( upper_bound C)) - (f . ( lower_bound C))) by A1, A18, A19, Th13, XBOOLE_1: 1;

      ((f `| X) | B) is continuous by A2, A12, FCONT_1: 16;

      then (f `| X) is_integrable_on B by A13, A12, Th11, XBOOLE_1: 1;

      then

       A21: ( integral ((f `| X),B)) = ((f . ( upper_bound B)) - (f . ( lower_bound B))) by A1, A12, A15, Th13, XBOOLE_1: 1;

      (f `| X) is_integrable_on A by A2, A13, Th11;

      then ( integral ((f `| X),A)) = ((f . ( upper_bound A)) - (f . ( lower_bound A))) by A1, A2, A13, Th10, Th13;

      hence thesis by A3, A4, A5, A21, A20;

    end;

    definition

      let a,b be Real;

      assume

       A1: a <= b;

      :: INTEGRA5:def3

      func ['a,b'] -> non empty closed_interval Subset of REAL equals

      : Def3: [.a, b.];

      correctness by A1, MEASURE5: 14;

    end

    definition

      let a,b be Real;

      let f be PartFunc of REAL , REAL ;

      :: INTEGRA5:def4

      func integral (f,a,b) -> Real equals

      : Def4: ( integral (f, ['a, b'])) if a <= b

      otherwise ( - ( integral (f, ['b, a'])));

      correctness ;

    end

    theorem :: INTEGRA5:19

    for f be PartFunc of REAL , REAL , A be non empty closed_interval Subset of REAL , a, b st A = [.a, b.] holds ( integral (f,A)) = ( integral (f,a,b))

    proof

      let f be PartFunc of REAL , REAL ;

      let A be non empty closed_interval Subset of REAL ;

      let a, b;

      consider a1,b1 be Real such that

       A1: a1 <= b1 and

       A2: A = [.a1, b1.] by MEASURE5: 14;

      assume A = [.a, b.];

      then

       A3: a1 = a & b1 = b by A2, INTEGRA1: 5;

      then ( integral (f,a,b)) = ( integral (f, ['a, b'])) by A1, Def4;

      hence thesis by A1, A2, A3, Def3;

    end;

    theorem :: INTEGRA5:20

    for f be PartFunc of REAL , REAL , A be non empty closed_interval Subset of REAL , a, b st A = [.b, a.] holds ( - ( integral (f,A))) = ( integral (f,a,b))

    proof

      let f be PartFunc of REAL , REAL ;

      let A be non empty closed_interval Subset of REAL ;

      let a, b;

      consider a1,b1 be Real such that

       A1: a1 <= b1 and

       A2: A = [.a1, b1.] by MEASURE5: 14;

      assume

       A3: A = [.b, a.];

      then

       A4: a1 = b & b1 = a by A2, INTEGRA1: 5;

      now

        per cases by A1, A4, XXREAL_0: 1;

          suppose

           A5: b < a;

          then ( integral (f,a,b)) = ( - ( integral (f, ['b, a']))) by Def4;

          hence thesis by A3, A5, Def3;

        end;

          suppose

           A6: b = a;

          A = [.( lower_bound A), ( upper_bound A).] by INTEGRA1: 4;

          then ( lower_bound A) = b & ( upper_bound A) = a by A3, INTEGRA1: 5;

          

          then ( vol A) = (( upper_bound A) - ( upper_bound A)) by A6, INTEGRA1:def 5

          .= 0 ;

          then

           A7: ( integral (f,A)) = 0 by INTEGRA4: 6;

          ( integral (f,a,b)) = ( integral (f, ['a, b'])) by A6, Def4;

          hence thesis by A3, A6, A7, Def3;

        end;

      end;

      hence thesis;

    end;

    theorem :: INTEGRA5:21

    for f,g be PartFunc of REAL , REAL , X be open Subset of REAL st f is_differentiable_on X & g is_differentiable_on X & A c= X & (f `| X) is_integrable_on A & ((f `| X) | A) is bounded & (g `| X) is_integrable_on A & ((g `| X) | A) is bounded holds ( integral (((f `| X) (#) g),A)) = ((((f . ( upper_bound A)) * (g . ( upper_bound A))) - ((f . ( lower_bound A)) * (g . ( lower_bound A)))) - ( integral ((f (#) (g `| X)),A)))

    proof

      let f,g be PartFunc of REAL , REAL ;

      let X be open Subset of REAL ;

      assume that

       A1: f is_differentiable_on X and

       A2: g is_differentiable_on X and

       A3: A c= X and

       A4: (f `| X) is_integrable_on A and

       A5: ((f `| X) | A) is bounded and

       A6: (g `| X) is_integrable_on A and

       A7: ((g `| X) | A) is bounded;

      

       A8: ((f (#) g) `| X) = (((f `| X) (#) g) + (f (#) (g `| X))) by A1, A2, FDIFF_2: 20;

      (g | X) is continuous by A2, FDIFF_1: 25;

      then

       A9: (g | A) is continuous by A3, FCONT_1: 16;

      X c= ( dom g) by A2, FDIFF_1:def 6;

      then

       A10: A c= ( dom g) by A3, XBOOLE_1: 1;

      then

       A11: (g || A) is Function of A, REAL by Th6, FUNCT_2: 68;

      X c= ( dom g) by A2, FDIFF_1:def 6;

      then g is_integrable_on A by A3, A9, Th11, XBOOLE_1: 1;

      then

       A12: (g || A) is integrable;

      

       A13: A c= ( dom (g `| X)) by A2, A3, FDIFF_1:def 7;

      then

       A14: ((g `| X) || A) is Function of A, REAL by Th6, FUNCT_2: 68;

      (g | X) is continuous by A2, FDIFF_1: 25;

      then (g | A) is bounded by A3, A10, Th10, FCONT_1: 16;

      then

       A15: (((f `| X) (#) g) | (A /\ A)) is bounded by A5, RFUNCT_1: 84;

      then

       A16: ((((f `| X) (#) g) || A) | A) is bounded;

      (f | X) is continuous by A1, FDIFF_1: 25;

      then

       A17: (f | A) is continuous by A3, FCONT_1: 16;

      X c= ( dom f) by A1, FDIFF_1:def 6;

      then f is_integrable_on A by A3, A17, Th11, XBOOLE_1: 1;

      then

       A18: (f || A) is integrable;

      

       A19: A c= ( dom (f `| X)) by A1, A3, FDIFF_1:def 7;

      then

       A20: ((f `| X) || A) is Function of A, REAL by Th6, FUNCT_2: 68;

      

       A21: ((g `| X) || A) is integrable & (((g `| X) || A) | A) is bounded by A6, A7;

      

       A22: ((f `| X) || A) is integrable & (((f `| X) || A) | A) is bounded by A4, A5;

      ( dom ((f `| X) (#) g)) = (( dom (f `| X)) /\ ( dom g)) by VALUED_1:def 4;

      then A c= ( dom ((f `| X) (#) g)) by A10, A19, XBOOLE_1: 19;

      then

       A23: (((f `| X) (#) g) || A) is Function of A, REAL by Th6, FUNCT_2: 68;

      X c= ( dom f) by A1, FDIFF_1:def 6;

      then

       A24: A c= ( dom f) by A3, XBOOLE_1: 1;

      then

       A25: (f || A) is Function of A, REAL by Th6, FUNCT_2: 68;

      (f | X) is continuous by A1, FDIFF_1: 25;

      then (f | A) is bounded by A3, A24, Th10, FCONT_1: 16;

      then

       A26: ((f (#) (g `| X)) | (A /\ A)) is bounded by A7, RFUNCT_1: 84;

      then

       A27: (((f (#) (g `| X)) || A) | A) is bounded;

      ((((f `| X) (#) g) + (f (#) (g `| X))) | (A /\ A)) is bounded by A15, A26, RFUNCT_1: 83;

      then

       A28: (((f (#) g) `| X) | A) is bounded by A1, A2, FDIFF_2: 20;

      

       A29: ((f (#) g) . ( upper_bound A)) = ((f . ( upper_bound A)) * (g . ( upper_bound A))) & ((f (#) g) . ( lower_bound A)) = ((f . ( lower_bound A)) * (g . ( lower_bound A))) by VALUED_1: 5;

      ( dom (f (#) (g `| X))) = (( dom f) /\ ( dom (g `| X))) by VALUED_1:def 4;

      then A c= ( dom (f (#) (g `| X))) by A24, A13, XBOOLE_1: 19;

      then

       A30: ((f (#) (g `| X)) || A) is Function of A, REAL by Th6, FUNCT_2: 68;

      ((g || A) | A) is bounded by A9, A10, Th10;

      then (((f `| X) || A) (#) (g || A)) is integrable by A12, A11, A20, A22, INTEGRA4: 29;

      then

       A31: (((f `| X) (#) g) || A) is integrable by Th4;

      ((f || A) | A) is bounded by A17, A24, Th10;

      then ((f || A) (#) ((g `| X) || A)) is integrable by A18, A25, A14, A21, INTEGRA4: 29;

      then

       A32: ((f (#) (g `| X)) || A) is integrable by Th4;

      then ( integral ((((f `| X) (#) g) || A) + ((f (#) (g `| X)) || A))) = (( integral (((f `| X) (#) g) || A)) + ( integral ((f (#) (g `| X)) || A))) by A31, A23, A16, A30, A27, INTEGRA1: 57;

      then

       A33: ( integral ((((f `| X) (#) g) + (f (#) (g `| X))) || A)) = (( integral (((f `| X) (#) g),A)) + ( integral ((f (#) (g `| X)),A))) by Th5;

      ((((f `| X) (#) g) || A) + ((f (#) (g `| X)) || A)) is integrable by A31, A32, A23, A16, A30, A27, INTEGRA1: 57;

      then ((((f `| X) (#) g) + (f (#) (g `| X))) || A) is integrable by Th5;

      then

       A34: ((f (#) g) `| X) is_integrable_on A by A8;

      ( integral (((f (#) g) `| X) || A)) = ( integral (((f (#) g) `| X),A))

      .= (((f (#) g) . ( upper_bound A)) - ((f (#) g) . ( lower_bound A))) by A1, A2, A3, A34, A28, Th13, FDIFF_2: 20;

      hence thesis by A8, A29, A33;

    end;