integra7.miz



    begin

    reserve a,b,r for Real;

    reserve A for non empty set;

    reserve X,x for set;

    reserve f,g,F,G for PartFunc of REAL , REAL ;

    reserve n for Element of NAT ;

    theorem :: INTEGRA7:1

    

     Th1: for f,g be Function of A, REAL st ( rng f) is bounded_above & ( rng g) is bounded_above & (for x be set st x in A holds |.((f . x) - (g . x)).| <= a) holds (( upper_bound ( rng f)) - ( upper_bound ( rng g))) <= a & (( upper_bound ( rng g)) - ( upper_bound ( rng f))) <= a

    proof

      let f,g be Function of A, REAL ;

      assume that

       A1: ( rng f) is bounded_above and

       A2: ( rng g) is bounded_above and

       A3: for x be set st x in A holds |.((f . x) - (g . x)).| <= a;

      

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

      

       A5: for b st b in ( rng g) holds b <= (( upper_bound ( rng f)) + a)

      proof

        let b;

        assume b in ( rng g);

        then

        consider x be Element of A such that x in ( dom g) and

         A6: b = (g . x) by PARTFUN1: 3;

         |.((f . x) - (g . x)).| <= a by A3;

        then |.((g . x) - (f . x)).| <= a by COMPLEX1: 60;

        then ((g . x) - (f . x)) <= a by ABSVALUE: 5;

        then

         A7: b <= (a + (f . x)) by A6, XREAL_1: 20;

        (f . x) in ( rng f) by A4, FUNCT_1: 3;

        then (f . x) <= ( upper_bound ( rng f)) by A1, SEQ_4:def 1;

        then (a + (f . x)) <= (a + ( upper_bound ( rng f))) by XREAL_1: 6;

        hence thesis by A7, XXREAL_0: 2;

      end;

      

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

      

       A9: ( upper_bound ( rng g)) <= (( upper_bound ( rng f)) + a) by A5, SEQ_4: 45;

      

       A10: for b st b in ( rng f) holds b <= (( upper_bound ( rng g)) + a)

      proof

        let b;

        assume b in ( rng f);

        then

        consider x be Element of A such that x in ( dom f) and

         A11: b = (f . x) by PARTFUN1: 3;

        (g . x) in ( rng g) by A8, FUNCT_1: 3;

        then (g . x) <= ( upper_bound ( rng g)) by A2, SEQ_4:def 1;

        then

         A12: (a + (g . x)) <= (a + ( upper_bound ( rng g))) by XREAL_1: 6;

         |.((f . x) - (g . x)).| <= a by A3;

        then ((f . x) - (g . x)) <= a by ABSVALUE: 5;

        then b <= (a + (g . x)) by A11, XREAL_1: 20;

        hence thesis by A12, XXREAL_0: 2;

      end;

      ( upper_bound ( rng f)) <= (( upper_bound ( rng g)) + a) by A10, SEQ_4: 45;

      hence thesis by A9, XREAL_1: 20;

    end;

    theorem :: INTEGRA7:2

    

     Th2: for f,g be Function of A, REAL st ( rng f) is bounded_below & ( rng g) is bounded_below & (for x be set st x in A holds |.((f . x) - (g . x)).| <= a) holds (( lower_bound ( rng f)) - ( lower_bound ( rng g))) <= a & (( lower_bound ( rng g)) - ( lower_bound ( rng f))) <= a

    proof

      let f,g be Function of A, REAL ;

      assume that

       A1: ( rng f) is bounded_below and

       A2: ( rng g) is bounded_below and

       A3: for x be set st x in A holds |.((f . x) - (g . x)).| <= a;

      

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

      

       A5: for b st b in ( rng g) holds (( lower_bound ( rng f)) - a) <= b

      proof

        let b;

        assume b in ( rng g);

        then

        consider x be Element of A such that x in ( dom g) and

         A6: b = (g . x) by PARTFUN1: 3;

        (f . x) in ( rng f) by A4, FUNCT_1: 3;

        then ( lower_bound ( rng f)) <= (f . x) by A1, SEQ_4:def 2;

        then

         A7: (( lower_bound ( rng f)) - a) <= ((f . x) - a) by XREAL_1: 9;

         |.((f . x) - (g . x)).| <= a by A3;

        then ((f . x) - (g . x)) <= a by ABSVALUE: 5;

        then ((f . x) - a) <= b by A6, XREAL_1: 12;

        hence thesis by A7, XXREAL_0: 2;

      end;

      

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

      

       A9: (( lower_bound ( rng f)) - a) <= ( lower_bound ( rng g)) by A5, SEQ_4: 43;

      

       A10: for b st b in ( rng f) holds (( lower_bound ( rng g)) - a) <= b

      proof

        let b;

        assume b in ( rng f);

        then

        consider x be Element of A such that x in ( dom f) and

         A11: b = (f . x) by PARTFUN1: 3;

         |.((f . x) - (g . x)).| <= a by A3;

        then |.((g . x) - (f . x)).| <= a by COMPLEX1: 60;

        then ((g . x) - (f . x)) <= a by ABSVALUE: 5;

        then

         A12: ((g . x) - a) <= b by A11, XREAL_1: 12;

        (g . x) in ( rng g) by A8, FUNCT_1: 3;

        then ( lower_bound ( rng g)) <= (g . x) by A2, SEQ_4:def 2;

        then (( lower_bound ( rng g)) - a) <= ((g . x) - a) by XREAL_1: 9;

        hence thesis by A12, XXREAL_0: 2;

      end;

      (( lower_bound ( rng g)) - a) <= ( lower_bound ( rng f)) by A10, SEQ_4: 43;

      hence thesis by A9, XREAL_1: 12;

    end;

    theorem :: INTEGRA7:3

    ((f | X) | X) is bounded implies (f | X) is bounded;

    theorem :: INTEGRA7:4

    

     Th4: for x be Real st x in X & (f | X) is_differentiable_in x holds f is_differentiable_in x

    proof

      let x be Real;

      assume that

       A1: x in X and

       A2: (f | X) is_differentiable_in x;

      consider N be Neighbourhood of x such that

       A3: N c= ( dom (f | X)) and

       A4: ex L be LinearFunc, R be RestFunc st for x1 be Real st x1 in N holds (((f | X) . x1) - ((f | X) . x)) = ((L . (x1 - x)) + (R . (x1 - x))) by A2;

      

       A5: ((f | X) . x) = (f . x) by A1, FUNCT_1: 49;

      take N;

      N c= (( dom f) /\ X) by A3, RELAT_1: 61;

      hence N c= ( dom f) by XBOOLE_1: 18;

      consider L be LinearFunc, R be RestFunc such that

       A6: for x1 be Real st x1 in N holds (((f | X) . x1) - ((f | X) . x)) = ((L . (x1 - x)) + (R . (x1 - x))) by A4;

      take L, R;

      let x1 be Real;

      assume

       A7: x1 in N;

      then ((f | X) . x1) = (f . x1) by A3, FUNCT_1: 47;

      hence thesis by A6, A7, A5;

    end;

    theorem :: INTEGRA7:5

    (f | X) is_differentiable_on X implies f is_differentiable_on X

    proof

      assume

       A1: (f | X) is_differentiable_on X;

      then

       A2: for x be Real st x in X holds (f | X) is_differentiable_in x;

      X c= ( dom (f | X)) by A1;

      then X c= (( dom f) /\ X) by RELAT_1: 61;

      then X c= ( dom f) by XBOOLE_1: 18;

      hence thesis by A2;

    end;

    theorem :: INTEGRA7:6

    

     Th6: f is_differentiable_on X & g is_differentiable_on X implies (f + g) is_differentiable_on X & (f - g) is_differentiable_on X & (f (#) g) is_differentiable_on X

    proof

      assume that

       A1: f is_differentiable_on X and

       A2: g is_differentiable_on X;

      reconsider Z = X as Subset of REAL by A1, FDIFF_1: 8;

      reconsider Z as open Subset of REAL by A1, FDIFF_1: 10;

      X c= ( dom f) & X c= ( dom g) by A1, A2;

      then

       A3: Z c= (( dom f) /\ ( dom g)) by XBOOLE_1: 19;

      then

       A4: Z c= ( dom (f (#) g)) by VALUED_1:def 4;

      Z c= ( dom (f + g)) & Z c= ( dom (f - g)) by A3, VALUED_1: 12, VALUED_1:def 1;

      hence thesis by A1, A2, A4, FDIFF_1: 18, FDIFF_1: 19, FDIFF_1: 21;

    end;

    theorem :: INTEGRA7:7

    

     Th7: f is_differentiable_on X implies (r (#) f) is_differentiable_on X

    proof

      reconsider r1 = r as Real;

      assume

       A1: f is_differentiable_on X;

      then

      reconsider Z = X as Subset of REAL by FDIFF_1: 8;

      reconsider Z as open Subset of REAL by A1, FDIFF_1: 10;

      X c= ( dom f) by A1;

      then Z c= ( dom (r (#) f)) by VALUED_1:def 5;

      then (r1 (#) f) is_differentiable_on X by A1, FDIFF_1: 20;

      hence thesis;

    end;

    theorem :: INTEGRA7:8

    

     Th8: (for x be set st x in X holds (g . x) <> 0 ) & f is_differentiable_on X & g is_differentiable_on X implies (f / g) is_differentiable_on X

    proof

      assume that

       A1: for x be set st x in X holds (g . x) <> 0 and

       A2: f is_differentiable_on X and

       A3: g is_differentiable_on X;

      reconsider Z = X as Subset of REAL by A2, FDIFF_1: 8;

      reconsider Z as open Subset of REAL by A2, FDIFF_1: 10;

      for x be Real st x in Z holds (g . x) <> 0 by A1;

      hence thesis by A2, A3, FDIFF_2: 21;

    end;

    theorem :: INTEGRA7:9

    (for x be set st x in X holds (f . x) <> 0 ) & f is_differentiable_on X implies (f ^ ) is_differentiable_on X

    proof

      assume that

       A1: for x be set st x in X holds (f . x) <> 0 and

       A2: f is_differentiable_on X;

      reconsider Z = X as Subset of REAL by A2, FDIFF_1: 8;

      reconsider Z as open Subset of REAL by A2, FDIFF_1: 10;

      for x be Real st x in Z holds (f . x) <> 0 by A1;

      hence thesis by A2, FDIFF_2: 22;

    end;

    theorem :: INTEGRA7:10

    

     Th10: a <= b & ['a, b'] c= X & F is_differentiable_on X & (F `| X) is_integrable_on ['a, b'] & ((F `| X) | ['a, b']) is bounded implies (F . b) = (( integral ((F `| X),a,b)) + (F . a))

    proof

      assume that

       A1: a <= b and

       A2: ['a, b'] c= X & F is_differentiable_on X & (F `| X) is_integrable_on ['a, b'] & ((F `| X) | ['a, b']) is bounded;

      ( integral ((F `| X),a,b)) = ( integral ((F `| X), ['a, b'])) by A1, INTEGRA5:def 4;

      then

       A3: ( integral ((F `| X),a,b)) = ((F . ( upper_bound ['a, b'])) - (F . ( lower_bound ['a, b']))) by A2, INTEGRA5: 13;

      

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

      then

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

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

      hence thesis by A4, A5, A3, INTEGRA1: 5;

    end;

    begin

    definition

      let X be set, f be PartFunc of REAL , REAL ;

      :: INTEGRA7:def1

      func IntegralFuncs (f,X) -> set means

      : Def1: x in it iff ex F be PartFunc of REAL , REAL st x = F & F is_differentiable_on X & (F `| X) = (f | X);

      existence

      proof

        defpred P[ object] means ex F be PartFunc of REAL , REAL st $1 = F & F is_differentiable_on X & (F `| X) = (f | X);

        consider Z be set such that

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

        take Z;

        let x;

        thus x in Z implies ex F be PartFunc of REAL , REAL st x = F & F is_differentiable_on X & (F `| X) = (f | X) by A1;

        given F be PartFunc of REAL , REAL such that

         A2: x = F & F is_differentiable_on X & (F `| X) = (f | X);

        F in ( PFuncs ( REAL , REAL )) by PARTFUN1: 45;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        let Z1,Z2 be set such that

         A3: x in Z1 iff ex F be PartFunc of REAL , REAL st x = F & F is_differentiable_on X & (F `| X) = (f | X) and

         A4: x in Z2 iff ex F be PartFunc of REAL , REAL st x = F & F is_differentiable_on X & (F `| X) = (f | X);

        for x be object holds x in Z1 iff x in Z2

        proof

          let x be object;

          x in Z1 iff ex F be PartFunc of REAL , REAL st x = F & F is_differentiable_on X & (F `| X) = (f | X) by A3;

          hence thesis by A4;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    definition

      let X be set, F,f be PartFunc of REAL , REAL ;

      :: INTEGRA7:def2

      pred F is_integral_of f,X means F in ( IntegralFuncs (f,X));

    end

    

     Lm1: F is_integral_of (f,X) iff F is_differentiable_on X & (F `| X) = (f | X)

    proof

      hereby

        assume F is_integral_of (f,X);

        then F in ( IntegralFuncs (f,X));

        then ex F9 be PartFunc of REAL , REAL st F = F9 & F9 is_differentiable_on X & (F9 `| X) = (f | X) by Def1;

        hence F is_differentiable_on X & (F `| X) = (f | X);

      end;

      assume F is_differentiable_on X & (F `| X) = (f | X);

      then F in ( IntegralFuncs (f,X)) by Def1;

      hence thesis;

    end;

    theorem :: INTEGRA7:11

    

     Th11: F is_integral_of (f,X) implies X c= ( dom F)

    proof

      assume F is_integral_of (f,X);

      then F in ( IntegralFuncs (f,X));

      then ex G be PartFunc of REAL , REAL st F = G & G is_differentiable_on X & (G `| X) = (f | X) by Def1;

      hence thesis;

    end;

    theorem :: INTEGRA7:12

    F is_integral_of (f,X) & G is_integral_of (g,X) implies (F + G) is_integral_of ((f + g),X) & (F - G) is_integral_of ((f - g),X)

    proof

      assume that

       A1: F is_integral_of (f,X) and

       A2: G is_integral_of (g,X);

      

       A3: G is_differentiable_on X by A2, Lm1;

      

       A4: (G `| X) = (g | X) by A2, Lm1;

      then ( dom (g | X)) = X by A3, FDIFF_1:def 7;

      then (( dom g) /\ X) = X by RELAT_1: 61;

      then

       A5: X c= ( dom g) by XBOOLE_1: 18;

      

       A6: F is_differentiable_on X by A1, Lm1;

      then

       A7: (F + G) is_differentiable_on X by A3, Th6;

      

       A8: (F `| X) = (f | X) by A1, Lm1;

      then ( dom (f | X)) = X by A6, FDIFF_1:def 7;

      then (( dom f) /\ X) = X by RELAT_1: 61;

      then X c= ( dom f) by XBOOLE_1: 18;

      then

       A9: X c= (( dom f) /\ ( dom g)) by A5, XBOOLE_1: 19;

      then

       A10: X c= ( dom (f + g)) by VALUED_1:def 1;

       A11:

      now

        let x be Element of REAL ;

        assume x in ( dom ((F + G) `| X));

        then

         A12: x in X by A7, FDIFF_1:def 7;

        then (F | X) is_differentiable_in x by A6;

        then

         A13: F is_differentiable_in x by A12, Th4;

        ((G `| X) . x) = ( diff (G,x)) by A3, A12, FDIFF_1:def 7;

        then

         A14: (g . x) = ( diff (G,x)) by A4, A12, FUNCT_1: 49;

        ((F `| X) . x) = ( diff (F,x)) by A6, A12, FDIFF_1:def 7;

        then

         A15: (f . x) = ( diff (F,x)) by A8, A12, FUNCT_1: 49;

        (G | X) is_differentiable_in x by A3, A12;

        then

         A16: G is_differentiable_in x by A12, Th4;

        (((F + G) `| X) . x) = ( diff ((F + G),x)) by A7, A12, FDIFF_1:def 7;

        then (((F + G) `| X) . x) = (( diff (F,x)) + ( diff (G,x))) by A13, A16, FDIFF_1: 13;

        then (((F + G) `| X) . x) = ((f + g) . x) by A10, A12, A15, A14, VALUED_1:def 1;

        hence (((F + G) `| X) . x) = (((f + g) | X) . x) by A12, FUNCT_1: 49;

      end;

      

       A17: (F - G) is_differentiable_on X by A6, A3, Th6;

      

       A18: X c= ( dom (f - g)) by A9, VALUED_1: 12;

       A19:

      now

        let x be Element of REAL ;

        assume x in ( dom ((F - G) `| X));

        then

         A20: x in X by A17, FDIFF_1:def 7;

        then (F | X) is_differentiable_in x by A6;

        then

         A21: F is_differentiable_in x by A20, Th4;

        ((G `| X) . x) = ( diff (G,x)) by A3, A20, FDIFF_1:def 7;

        then

         A22: (g . x) = ( diff (G,x)) by A4, A20, FUNCT_1: 49;

        ((F `| X) . x) = ( diff (F,x)) by A6, A20, FDIFF_1:def 7;

        then

         A23: (f . x) = ( diff (F,x)) by A8, A20, FUNCT_1: 49;

        (G | X) is_differentiable_in x by A3, A20;

        then

         A24: G is_differentiable_in x by A20, Th4;

        (((F - G) `| X) . x) = ( diff ((F - G),x)) by A17, A20, FDIFF_1:def 7;

        then (((F - G) `| X) . x) = (( diff (F,x)) - ( diff (G,x))) by A21, A24, FDIFF_1: 14;

        then (((F - G) `| X) . x) = ((f - g) . x) by A18, A20, A23, A22, VALUED_1: 13;

        hence (((F - G) `| X) . x) = (((f - g) | X) . x) by A20, FUNCT_1: 49;

      end;

      X = ( dom ((f + g) | X)) by A10, RELAT_1: 62;

      then ( dom ((F + G) `| X)) = ( dom ((f + g) | X)) by A7, FDIFF_1:def 7;

      then ((F + G) `| X) = ((f + g) | X) by A11, PARTFUN1: 5;

      hence (F + G) is_integral_of ((f + g),X) by A7, Lm1;

      X = ( dom ((f - g) | X)) by A18, RELAT_1: 62;

      then ( dom ((F - G) `| X)) = ( dom ((f - g) | X)) by A17, FDIFF_1:def 7;

      then ((F - G) `| X) = ((f - g) | X) by A19, PARTFUN1: 5;

      hence thesis by A17, Lm1;

    end;

    theorem :: INTEGRA7:13

    F is_integral_of (f,X) implies (r (#) F) is_integral_of ((r (#) f),X)

    proof

      assume

       A1: F is_integral_of (f,X);

      then

       A2: F is_differentiable_on X by Lm1;

      then

       A3: (r (#) F) is_differentiable_on X by Th7;

      

       A4: (F `| X) = (f | X) by A1, Lm1;

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

      then (( dom f) /\ X) = X by RELAT_1: 61;

      then X c= ( dom f) by XBOOLE_1: 18;

      then

       A5: X c= ( dom (r (#) f)) by VALUED_1:def 5;

       A6:

      now

        reconsider r1 = r as Real;

        let x be Element of REAL ;

        assume x in ( dom ((r (#) F) `| X));

        then

         A7: x in X by A3, FDIFF_1:def 7;

        then (F | X) is_differentiable_in x by A2;

        then

         A8: F is_differentiable_in x by A7, Th4;

        (((r (#) F) `| X) . x) = ( diff ((r (#) F),x)) by A3, A7, FDIFF_1:def 7;

        then

         A9: (((r1 (#) F) `| X) . x) = (r1 * ( diff (F,x))) by A8, FDIFF_1: 15;

        ((F `| X) . x) = ( diff (F,x)) by A2, A7, FDIFF_1:def 7;

        then (f . x) = ( diff (F,x)) by A4, A7, FUNCT_1: 49;

        then (((r (#) F) `| X) . x) = ((r (#) f) . x) by A5, A7, A9, VALUED_1:def 5;

        hence (((r (#) F) `| X) . x) = (((r (#) f) | X) . x) by A7, FUNCT_1: 49;

      end;

      X = ( dom ((r (#) f) | X)) by A5, RELAT_1: 62;

      then ( dom ((r (#) F) `| X)) = ( dom ((r (#) f) | X)) by A3, FDIFF_1:def 7;

      then ((r (#) F) `| X) = ((r (#) f) | X) by A6, PARTFUN1: 5;

      hence thesis by A3, Lm1;

    end;

    theorem :: INTEGRA7:14

    F is_integral_of (f,X) & G is_integral_of (g,X) implies (F (#) G) is_integral_of (((f (#) G) + (F (#) g)),X)

    proof

      assume that

       A1: F is_integral_of (f,X) and

       A2: G is_integral_of (g,X);

      

       A3: G is_differentiable_on X by A2, Lm1;

      

       A4: X c= ( dom F) by A1, Th11;

      

       A5: (G `| X) = (g | X) by A2, Lm1;

      then ( dom (g | X)) = X by A3, FDIFF_1:def 7;

      then (( dom g) /\ X) = X by RELAT_1: 61;

      then X c= ( dom g) by XBOOLE_1: 18;

      then X c= (( dom F) /\ ( dom g)) by A4, XBOOLE_1: 19;

      then

       A6: X c= ( dom (F (#) g)) by VALUED_1:def 4;

      

       A7: X c= ( dom G) by A2, Th11;

      

       A8: F is_differentiable_on X by A1, Lm1;

      then

       A9: (F (#) G) is_differentiable_on X by A3, Th6;

      

       A10: (F `| X) = (f | X) by A1, Lm1;

      then ( dom (f | X)) = X by A8, FDIFF_1:def 7;

      then (( dom f) /\ X) = X by RELAT_1: 61;

      then X c= ( dom f) by XBOOLE_1: 18;

      then X c= (( dom f) /\ ( dom G)) by A7, XBOOLE_1: 19;

      then X c= ( dom (f (#) G)) by VALUED_1:def 4;

      then X c= (( dom (f (#) G)) /\ ( dom (F (#) g))) by A6, XBOOLE_1: 19;

      then

       A11: X c= ( dom ((f (#) G) + (F (#) g))) by VALUED_1:def 1;

       A12:

      now

        let x be Element of REAL ;

        assume x in ( dom ((F (#) G) `| X));

        then

         A13: x in X by A9, FDIFF_1:def 7;

        then (F | X) is_differentiable_in x by A8;

        then

         A14: F is_differentiable_in x by A13, Th4;

        ((G `| X) . x) = ( diff (G,x)) by A3, A13, FDIFF_1:def 7;

        then (g . x) = ( diff (G,x)) by A5, A13, FUNCT_1: 49;

        then

         A15: ((F (#) g) . x) = ((F . x) * ( diff (G,x))) by VALUED_1: 5;

        ((F `| X) . x) = ( diff (F,x)) by A8, A13, FDIFF_1:def 7;

        then (f . x) = ( diff (F,x)) by A10, A13, FUNCT_1: 49;

        then

         A16: ((f (#) G) . x) = ((G . x) * ( diff (F,x))) by VALUED_1: 5;

        (G | X) is_differentiable_in x by A3, A13;

        then

         A17: G is_differentiable_in x by A13, Th4;

        (((F (#) G) `| X) . x) = ( diff ((F (#) G),x)) by A9, A13, FDIFF_1:def 7;

        then (((F (#) G) `| X) . x) = (((G . x) * ( diff (F,x))) + ((F . x) * ( diff (G,x)))) by A14, A17, FDIFF_1: 16;

        then (((F (#) G) `| X) . x) = (((F (#) g) + (f (#) G)) . x) by A11, A13, A15, A16, VALUED_1:def 1;

        hence (((F (#) G) `| X) . x) = ((((F (#) g) + (f (#) G)) | X) . x) by A13, FUNCT_1: 49;

      end;

      X = ( dom (((f (#) G) + (F (#) g)) | X)) by A11, RELAT_1: 62;

      then ( dom ((F (#) G) `| X)) = ( dom (((f (#) G) + (F (#) g)) | X)) by A9, FDIFF_1:def 7;

      then ((F (#) G) `| X) = (((F (#) g) + (f (#) G)) | X) by A12, PARTFUN1: 5;

      hence thesis by A9, Lm1;

    end;

    theorem :: INTEGRA7:15

    (for x be set st x in X holds (G . x) <> 0 ) & F is_integral_of (f,X) & G is_integral_of (g,X) implies (F / G) is_integral_of ((((f (#) G) - (F (#) g)) / (G (#) G)),X)

    proof

      assume that

       A1: for x be set st x in X holds (G . x) <> 0 and

       A2: F is_integral_of (f,X) and

       A3: G is_integral_of (g,X);

      

       A4: G is_differentiable_on X by A3, Lm1;

      

       A5: X c= ( dom F) by A2, Th11;

      

       A6: (G `| X) = (g | X) by A3, Lm1;

      then ( dom (g | X)) = X by A4, FDIFF_1:def 7;

      then (( dom g) /\ X) = X by RELAT_1: 61;

      then X c= ( dom g) by XBOOLE_1: 18;

      then X c= (( dom F) /\ ( dom g)) by A5, XBOOLE_1: 19;

      then

       A7: X c= ( dom (F (#) g)) by VALUED_1:def 4;

      

       A8: X c= ( dom G) by A3, Th11;

      

       A9: F is_differentiable_on X by A2, Lm1;

      then

       A10: (F / G) is_differentiable_on X by A1, A4, Th8;

      

       A11: (F `| X) = (f | X) by A2, Lm1;

      then ( dom (f | X)) = X by A9, FDIFF_1:def 7;

      then (( dom f) /\ X) = X by RELAT_1: 61;

      then X c= ( dom f) by XBOOLE_1: 18;

      then X c= (( dom f) /\ ( dom G)) by A8, XBOOLE_1: 19;

      then X c= ( dom (f (#) G)) by VALUED_1:def 4;

      then X c= (( dom (f (#) G)) /\ ( dom (F (#) g))) by A7, XBOOLE_1: 19;

      then

       A12: X c= ( dom ((f (#) G) - (F (#) g))) by VALUED_1: 12;

       A13:

      now

        let x be Element of REAL ;

        X = (( dom G) /\ X) by A3, Th11, XBOOLE_1: 28;

        then

         A14: X = ( dom (G | X)) by RELAT_1: 61;

        assume x in ( dom ((F / G) `| X));

        then

         A15: x in X by A10, FDIFF_1:def 7;

        then (F | X) is_differentiable_in x by A9;

        then

         A16: F is_differentiable_in x by A15, Th4;

        (G | X) is_differentiable_in x by A4, A15;

        then

         A17: G is_differentiable_in x by A15, Th4;

        (G . x) = ((G | X) . x) by A15, FUNCT_1: 49;

        then

         A18: ((G . x) ^2 ) = (((G | X) (#) (G | X)) . x) by VALUED_1: 5;

        now

          let y be set;

          assume

           A19: y in ( dom (G | X));

          then y in (( dom G) /\ X) by RELAT_1: 61;

          then y in X by XBOOLE_0:def 4;

          then

           A20: (G . y) <> 0 by A1;

          ((G | X) . y) = (G . y) by A19, FUNCT_1: 47;

          then not ((G | X) . y) in { 0 } by A20, TARSKI:def 1;

          hence not y in ((G | X) " { 0 }) by FUNCT_1:def 7;

        end;

        then not x in ((G | X) " { 0 }) by A15, A14;

        then x in ((( dom (G | X)) \ ((G | X) " { 0 })) /\ (( dom (G | X)) \ ((G | X) " { 0 }))) by A15, A14, XBOOLE_0:def 5;

        then x in (( dom ((G | X) (#) (G | X))) \ (((G | X) (#) (G | X)) " { 0 })) by RFUNCT_1: 2;

        then x in (( dom ((f (#) G) - (F (#) g))) /\ (( dom ((G | X) (#) (G | X))) \ (((G | X) (#) (G | X)) " { 0 }))) by A12, A15, XBOOLE_0:def 4;

        then

         A21: x in ( dom (((f (#) G) - (F (#) g)) / ((G | X) (#) (G | X)))) by RFUNCT_1:def 1;

        ((G `| X) . x) = ( diff (G,x)) by A4, A15, FDIFF_1:def 7;

        then (g . x) = ( diff (G,x)) by A6, A15, FUNCT_1: 49;

        then

         A22: ((F (#) g) . x) = ((F . x) * ( diff (G,x))) by VALUED_1: 5;

        ((F `| X) . x) = ( diff (F,x)) by A9, A15, FDIFF_1:def 7;

        then (f . x) = ( diff (F,x)) by A11, A15, FUNCT_1: 49;

        then ((f (#) G) . x) = ((G . x) * ( diff (F,x))) by VALUED_1: 5;

        then

         A23: (((f (#) G) - (F (#) g)) . x) = ((( diff (F,x)) * (G . x)) - (( diff (G,x)) * (F . x))) by A12, A15, A22, VALUED_1: 13;

        (((F / G) `| X) . x) = ( diff ((F / G),x)) & (G . x) <> 0 by A1, A10, A15, FDIFF_1:def 7;

        then (((F / G) `| X) . x) = (((( diff (F,x)) * (G . x)) - (( diff (G,x)) * (F . x))) / ((G . x) ^2 )) by A16, A17, FDIFF_2: 14;

        then (((F / G) `| X) . x) = ((((f (#) G) - (F (#) g)) / ((G | X) (#) (G | X))) . x) by A21, A23, A18, RFUNCT_1:def 1;

        then (((F / G) `| X) . x) = ((((f (#) G) - (F (#) g)) / ((G (#) G) | X)) . x) by RFUNCT_1: 45;

        hence (((F / G) `| X) . x) = (((((f (#) G) - (F (#) g)) / (G (#) G)) | X) . x) by RFUNCT_1: 48;

      end;

      now

        assume ((G | X) " { 0 }) <> {} ;

        then

        consider y be object such that

         A24: y in ((G | X) " { 0 }) by XBOOLE_0:def 1;

        

         A25: y in ( dom (G | X)) by A24, FUNCT_1:def 7;

        then

         A26: ((G | X) . y) = (G . y) by FUNCT_1: 47;

        y in (( dom G) /\ X) by A25, RELAT_1: 61;

        then y in X by XBOOLE_0:def 4;

        then

         A27: (G . y) <> 0 by A1;

        ((G | X) . y) in { 0 } by A24, FUNCT_1:def 7;

        hence contradiction by A27, A26, TARSKI:def 1;

      end;

      then ((( dom (G | X)) \ ((G | X) " { 0 })) /\ (( dom (G | X)) \ ((G | X) " { 0 }))) = ( dom (G | X));

      then (( dom ((G | X) (#) (G | X))) \ (((G | X) (#) (G | X)) " { 0 })) = ( dom (G | X)) by RFUNCT_1: 2;

      then (( dom ((G | X) (#) (G | X))) \ (((G | X) (#) (G | X)) " { 0 })) = (( dom G) /\ X) by RELAT_1: 61;

      then

       A28: (( dom ((G | X) (#) (G | X))) \ (((G | X) (#) (G | X)) " { 0 })) = X by A3, Th11, XBOOLE_1: 28;

      X = ( dom (((f (#) G) - (F (#) g)) | X)) by A12, RELAT_1: 62;

      then (( dom (((f (#) G) - (F (#) g)) | X)) /\ (( dom ((G | X) (#) (G | X))) \ (((G | X) (#) (G | X)) " { 0 }))) = X by A28;

      then ( dom ((((f (#) G) - (F (#) g)) | X) / ((G | X) (#) (G | X)))) = X by RFUNCT_1:def 1;

      then ( dom ((((f (#) G) - (F (#) g)) | X) / ((G (#) G) | X))) = X by RFUNCT_1: 45;

      then ( dom ((((f (#) G) - (F (#) g)) / (G (#) G)) | X)) = X by RFUNCT_1: 48;

      then ( dom ((F / G) `| X)) = ( dom ((((f (#) G) - (F (#) g)) / (G (#) G)) | X)) by A10, FDIFF_1:def 7;

      then ((F / G) `| X) = ((((f (#) G) - (F (#) g)) / (G (#) G)) | X) by A13, PARTFUN1: 5;

      hence thesis by A10, Lm1;

    end;

    theorem :: INTEGRA7:16

    a <= b & ['a, b'] c= ( dom f) & (f | ['a, b']) is continuous & ].a, b.[ c= ( dom F) & (for x be Real st x in ].a, b.[ holds (F . x) = (( integral (f,a,x)) + (F . a))) implies F is_integral_of (f, ].a, b.[)

    proof

      set O = ].a, b.[;

      assume that

       A1: a <= b and

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

       A3: (f | ['a, b']) is continuous and

       A4: ].a, b.[ c= ( dom F) and

       A5: for x be Real st x in ].a, b.[ holds (F . x) = (( integral (f,a,x)) + (F . a));

      ( dom (F | O)) = (( dom F) /\ O) by PARTFUN2: 15;

      then

       A6: ( dom (F | O)) = O by A4, XBOOLE_1: 28;

      reconsider Fa = (F . a) as Element of REAL by XREAL_0:def 1;

      set H1 = ( REAL --> Fa);

      deffunc G0( Real) = ( In (( integral (f,a,$1)), REAL ));

      consider G1 be Function of REAL , REAL such that

       A7: for h be Element of REAL holds (G1 . h) = G0(h) from FUNCT_2:sch 4;

      reconsider H = (H1 | O) as PartFunc of REAL , REAL ;

      reconsider G = (G1 | O) as PartFunc of REAL , REAL ;

      ( dom H) = (( dom H1) /\ O) by RELAT_1: 61;

      then

       A8: ( dom H) = ( REAL /\ O) by FUNCT_2:def 1;

      then

       A9: ( dom H) = O by XBOOLE_1: 28;

      now

        let x be Element of REAL ;

        reconsider z = x as Real;

        assume

         A10: x in (O /\ ( dom H));

        then (H . x) = (H1 . z) by A9, FUNCT_1: 47;

        then (H . x) = (F . a) by FUNCOP_1: 7;

        hence (H /. x) = (F . a) by A9, A10, PARTFUN1:def 6;

      end;

      then

       A11: (H | O) is constant by PARTFUN2: 35;

      then

       A12: H is_differentiable_on O by A9, FDIFF_1: 22;

      ( dom G) = (( dom G1) /\ O) by RELAT_1: 61;

      then

       A13: ( dom G) = ( REAL /\ O) by FUNCT_2:def 1;

      then

       A14: O = ( dom G) by XBOOLE_1: 28;

       A15:

      now

        let x be Real;

        reconsider z = x as Element of REAL by XREAL_0:def 1;

        assume x in ].a, b.[;

        then (G . x) = (G1 . x) by A14, FUNCT_1: 47;

        then (G . x) = G0(z) by A7;

        hence (G . x) = ( integral (f,a,x));

      end;

       A16:

      now

        let x be object;

        assume

         A17: x in ( dom (F | O));

        then

        reconsider z = x as Real;

        reconsider z1 = z as Element of REAL by XREAL_0:def 1;

        (H . x) = (H1 . z1) by A9, A6, A17, FUNCT_1: 47;

        then

         A18: (H . x) = (F . a) by FUNCOP_1: 7;

        ((F | O) . x) = (F . z) by A17, FUNCT_1: 47;

        then ((F | O) . x) = (( integral (f,a,z)) + (F . a)) by A5, A6, A17;

        hence ((F | O) . x) = ((G . x) + (H . x)) by A15, A6, A17, A18;

      end;

      

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

      then

       A20: O c= ['a, b'] by XXREAL_1: 25;

      then

       A21: O c= ( dom f) by A2, XBOOLE_1: 1;

      

       A22: for x be Real st x in O holds G is_differentiable_in x & ( diff (G,x)) = (f . x)

      proof

        let x be Real;

        reconsider z = x as Real;

        

         A23: (f | O) is continuous by A3, A19, FCONT_1: 16, XXREAL_1: 25;

        assume

         A24: x in ].a, b.[;

        then x in ( dom (f | O)) by A21, RELAT_1: 57;

        then

         A25: (f | O) is_continuous_in z by A23, FCONT_1:def 2;

        for r be Real st 0 < r holds ex s be Real st 0 < s & for x1 be Real st x1 in ( dom f) & |.(x1 - z).| < s holds |.((f . x1) - (f . z)).| < r

        proof

          let r be Real;

          consider ss1 be Real such that

           A26: 0 < ss1 and

           A27: ].(z - ss1), (z + ss1).[ c= O by A24, RCOMP_1: 19;

          assume 0 < r;

          then

          consider s be Real such that

           A28: 0 < s and

           A29: for x1 be Real st x1 in ( dom (f | O)) & |.(x1 - z).| < s holds |.(((f | O) . x1) - ((f | O) . z)).| < r by A25, FCONT_1: 3;

          set s1 = ( min (ss1,s));

          take s1;

          now

            let x1 be Real;

            assume that x1 in ( dom f) and

             A30: |.(x1 - z).| < s1;

            s1 <= s by XXREAL_0: 17;

            then

             A31: |.(x1 - z).| < s by A30, XXREAL_0: 2;

            O = (O /\ ( dom f)) by A2, A20, XBOOLE_1: 1, XBOOLE_1: 28;

            then

             A32: O = ( dom (f | O)) by PARTFUN2: 15;

            s1 <= ss1 by XXREAL_0: 17;

            then |.(x1 - z).| < ss1 by A30, XXREAL_0: 2;

            then

             A33: x1 in ].(z - ss1), (z + ss1).[ by RCOMP_1: 1;

            then |.((f . x1) - (f . z)).| = |.(((f | O) . x1) - (f . z)).| by A27, A32, FUNCT_1: 47;

            then |.((f . x1) - (f . z)).| = |.(((f | O) . x1) - ((f | O) . z)).| by A24, A32, FUNCT_1: 47;

            hence |.((f . x1) - (f . z)).| < r by A29, A27, A31, A33, A32;

          end;

          hence thesis by A28, A26, XXREAL_0: 15;

        end;

        then

         A34: f is_continuous_in z by FCONT_1: 3;

        (f | ['a, b']) is bounded & f is_integrable_on ['a, b'] by A2, A3, INTEGRA5: 10, INTEGRA5: 11;

        hence thesis by A1, A2, A14, A15, A24, A34, INTEGRA6: 28;

      end;

      then for x be Real st x in O holds G is_differentiable_in x;

      then

       A35: G is_differentiable_on O by A14;

      ( dom (F | O)) = (( dom G) /\ ( dom H)) by A13, A8, A6, XBOOLE_1: 28;

      then

       A36: (F | O) = (G + H) by A16, VALUED_1:def 1;

      then (F | O) is_differentiable_on O by A35, A12, A6, FDIFF_1: 18;

      then for x be Real st x in O holds (F | O) is_differentiable_in x;

      then

       A37: F is_differentiable_on O by A4;

       A38:

      now

        let x be Element of REAL ;

        assume x in ( dom (F `| O));

        then

         A39: x in O by A37, FDIFF_1:def 7;

        then x in (( dom f) /\ O) by A21, XBOOLE_0:def 4;

        then

         A40: x in ( dom (f | O)) by PARTFUN2: 15;

        ((F `| O) . x) = (((F | O) `| O) . x) by A37, FDIFF_2: 16;

        then ((F `| O) . x) = (( diff (G,x)) + ( diff (H,x))) by A35, A12, A6, A36, A39, FDIFF_1: 18;

        then

         A41: ((F `| O) . x) = ((f . x) + ( diff (H,x))) by A22, A39;

        ((H `| O) . x) = 0 by A9, A11, A39, FDIFF_1: 22;

        then ( diff (H,x)) = 0 by A12, A39, FDIFF_1:def 7;

        hence ((F `| O) . x) = ((f | O) . x) by A40, A41, FUNCT_1: 47;

      end;

      ( dom (F `| O)) = O by A37, FDIFF_1:def 7;

      then ( dom (F `| O)) = (O /\ ( dom f)) by A2, A20, XBOOLE_1: 1, XBOOLE_1: 28;

      then ( dom (F `| O)) = ( dom (f | O)) by PARTFUN2: 15;

      then (F `| O) = (f | O) by A38, PARTFUN1: 5;

      hence thesis by A37, Lm1;

    end;

    theorem :: INTEGRA7:17

    for x,x0 be Real st (f | [.a, b.]) is continuous & [.a, b.] c= ( dom f) & x in ].a, b.[ & x0 in ].a, b.[ & F is_integral_of (f, ].a, b.[) holds (F . x) = (( integral (f,x0,x)) + (F . x0))

    proof

      let x,x0 be Real;

      set O = ].a, b.[;

      assume that

       A1: (f | [.a, b.]) is continuous and

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

       A3: x in ].a, b.[ & x0 in ].a, b.[ and

       A4: F is_integral_of (f, ].a, b.[);

      

       A5: F is_differentiable_on O & (F `| O) = (f | O) by A4, Lm1;

      

       A6: O c= [.a, b.] by XXREAL_1: 25;

      

       A7: [.x, x0.] c= ].a, b.[ by A3, XXREAL_2:def 12;

       A8:

      now

        assume

         A9: x < x0;

        then

         A10: ['x, x0'] c= ].a, b.[ by A7, INTEGRA5:def 3;

        then

         A11: (f | ['x, x0']) is continuous by A1, A6, FCONT_1: 16, XBOOLE_1: 1;

        ((F `| ].a, b.[) || ['x, x0']) = ((f | ].a, b.[) | ['x, x0']) by A4, Lm1;

        then

         A12: ((F `| ].a, b.[) || ['x, x0']) = (f || ['x, x0']) by A10, FUNCT_1: 51;

        

         A13: ['x, x0'] c= [.a, b.] by A6, A10, XBOOLE_1: 1;

        then ['x, x0'] c= ( dom f) by A2, XBOOLE_1: 1;

        then f is_integrable_on ['x, x0'] by A11, INTEGRA5: 17;

        then (f || ['x, x0']) is integrable;

        then

         A14: (F `| ].a, b.[) is_integrable_on ['x, x0'] by A12;

        ((F `| ].a, b.[) | ['x, x0']) is bounded by A2, A12, A13, A11, INTEGRA5: 10, XBOOLE_1: 1;

        then (F . x0) = (( integral ((f | ].a, b.[),x,x0)) + (F . x)) by A5, A9, A10, A14, Th10;

        then (F . x0) = (( integral ((f | ].a, b.[), ['x, x0'])) + (F . x)) by A9, INTEGRA5:def 4;

        then (F . x0) = (( integral (f, ['x, x0'])) + (F . x)) by A10, FUNCT_1: 51;

        then

         A15: (F . x0) = (( integral (f,x,x0)) + (F . x)) by A9, INTEGRA5:def 4;

        ( integral (f,x0,x)) = ( - ( integral (f, ['x, x0']))) by A9, INTEGRA5:def 4;

        then ( integral (f,x0,x)) = ( - ( integral (f,x,x0))) by A9, INTEGRA5:def 4;

        hence thesis by A15;

      end;

      

       A16: [.x0, x.] c= ].a, b.[ by A3, XXREAL_2:def 12;

      now

        assume

         A17: x0 <= x;

        then

         A18: ['x0, x'] c= ].a, b.[ by A16, INTEGRA5:def 3;

        then

         A19: (f | ['x0, x']) is continuous by A1, A6, FCONT_1: 16, XBOOLE_1: 1;

        ((F `| ].a, b.[) || ['x0, x']) = ((f | ].a, b.[) | ['x0, x']) by A4, Lm1;

        then

         A20: ((F `| ].a, b.[) || ['x0, x']) = (f || ['x0, x']) by A18, FUNCT_1: 51;

         ['x0, x'] c= [.a, b.] by A6, A18, XBOOLE_1: 1;

        then

         A21: ['x0, x'] c= ( dom f) by A2, XBOOLE_1: 1;

        (f | ['x0, x']) is continuous by A1, A6, A18, FCONT_1: 16, XBOOLE_1: 1;

        then f is_integrable_on ['x0, x'] by A21, INTEGRA5: 17;

        then (f || ['x0, x']) is integrable;

        then (F `| ].a, b.[) is_integrable_on ['x0, x'] by A20;

        then (F . x) = (( integral ((f | ].a, b.[),x0,x)) + (F . x0)) by A5, A17, A18, A20, A21, A19, Th10, INTEGRA5: 10;

        then (F . x) = (( integral ((f | ].a, b.[), ['x0, x'])) + (F . x0)) by A17, INTEGRA5:def 4;

        then (F . x) = (( integral (f, ['x0, x'])) + (F . x0)) by A18, FUNCT_1: 51;

        hence thesis by A17, INTEGRA5:def 4;

      end;

      hence thesis by A8;

    end;

    theorem :: INTEGRA7:18

    

     Th18: a <= b & ['a, b'] c= X & F is_integral_of (f,X) & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded implies (F . b) = (( integral (f,a,b)) + (F . a))

    proof

      assume that

       A1: a <= b and

       A2: ['a, b'] c= X;

      assume

       A3: F is_integral_of (f,X);

      then

       A4: F is_differentiable_on X & (F `| X) = (f | X) by Lm1;

      assume f is_integrable_on ['a, b'];

      then

       A5: (f || ['a, b']) is integrable;

      assume

       A6: (f | ['a, b']) is bounded;

      ((F `| X) || ['a, b']) = ((f | X) | ['a, b']) by A3, Lm1;

      then

       A7: ((F `| X) || ['a, b']) = (f || ['a, b']) by A2, FUNCT_1: 51;

      then (F `| X) is_integrable_on ['a, b'] by A5;

      then (F . b) = (( integral ((f | X),a,b)) + (F . a)) by A1, A2, A4, A7, A6, Th10;

      then (F . b) = (( integral ((f | X), ['a, b'])) + (F . a)) by A1, INTEGRA5:def 4;

      then (F . b) = (( integral (f, ['a, b'])) + (F . a)) by A2, FUNCT_1: 51;

      hence thesis by A1, INTEGRA5:def 4;

    end;

    theorem :: INTEGRA7:19

    

     Th19: a <= b & [.a, b.] c= X & X c= ( dom f) & (f | X) is continuous implies (f | ['a, b']) is continuous & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded

    proof

      assume a <= b;

      then

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

      assume that

       A2: [.a, b.] c= X and

       A3: X c= ( dom f) and

       A4: (f | X) is continuous;

      thus

       A5: (f | ['a, b']) is continuous by A1, A2, A4, FCONT_1: 16;

       [.a, b.] c= ( dom f) by A2, A3, XBOOLE_1: 1;

      hence thesis by A1, A5, INTEGRA5: 10, INTEGRA5: 17;

    end;

    theorem :: INTEGRA7:20

    

     Th20: a <= b & [.a, b.] c= X & X c= ( dom f) & (f | X) is continuous & F is_integral_of (f,X) implies (F . b) = (( integral (f,a,b)) + (F . a))

    proof

      assume that

       A1: a <= b and

       A2: [.a, b.] c= X and

       A3: X c= ( dom f);

      assume (f | X) is continuous;

      then

       A4: f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded by A1, A2, A3, Th19;

      

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

      assume F is_integral_of (f,X);

      hence thesis by A1, A2, A5, A4, Th18;

    end;

    theorem :: INTEGRA7:21

    

     Th21: b <= a & ['b, a'] c= X & f is_integrable_on ['b, a'] & g is_integrable_on ['b, a'] & (f | ['b, a']) is bounded & (g | ['b, a']) is bounded & X c= ( dom f) & X c= ( dom g) & F is_integral_of (f,X) & G is_integral_of (g,X) implies (((F . a) * (G . a)) - ((F . b) * (G . b))) = (( integral ((f (#) G),b,a)) + ( integral ((F (#) g),b,a)))

    proof

      assume that

       A1: b <= a and

       A2: ['b, a'] c= X and

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

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

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

       A6: (g | ['b, a']) is bounded;

      set I = ['b, a'];

      assume that

       A7: X c= ( dom f) and

       A8: X c= ( dom g) and

       A9: F is_integral_of (f,X) and

       A10: G is_integral_of (g,X);

      

       A11: X c= ( dom G) by A10, Th11;

      then

       A12: I c= ( dom G) by A2, XBOOLE_1: 1;

      

       A13: G is_differentiable_on X by A10, Lm1;

      then

       A14: (G | X) is continuous by FDIFF_1: 25;

      then

       A15: (G | I) is bounded by A2, A12, FCONT_1: 16, INTEGRA5: 10;

      then

       A16: ((f (#) G) | (I /\ I)) is bounded by A5, RFUNCT_1: 84;

      

       A17: X c= ( dom F) by A9, Th11;

      then

       A18: I c= ( dom F) by A2, XBOOLE_1: 1;

      

       A19: F is_differentiable_on X by A9, Lm1;

      then

       A20: X is open Subset of REAL by FDIFF_1: 8, FDIFF_1: 10;

      

       A21: (F | X) is continuous by A19, FDIFF_1: 25;

      then

       A22: (F | I) is bounded by A2, A18, FCONT_1: 16, INTEGRA5: 10;

      then

       A23: ((F (#) g) | (I /\ I)) is bounded by A6, RFUNCT_1: 84;

      then

       A24: (((f (#) G) + (F (#) g)) | (I /\ I)) is bounded by A16, RFUNCT_1: 83;

      (F | I) is continuous by A2, A21, FCONT_1: 16;

      then

       A25: F is_integrable_on I by A18, INTEGRA5: 17;

      I c= ( dom g) by A2, A8, XBOOLE_1: 1;

      then

       A26: (F (#) g) is_integrable_on I by A4, A6, A18, A25, A22, INTEGRA6: 14;

      (F `| X) = (f | X) & (G `| X) = (g | X) by A9, A10, Lm1;

      then ((F (#) G) `| X) = (((f | X) (#) G) + (F (#) (g | X))) by A19, A13, A20, FDIFF_2: 20;

      then ((F (#) G) `| X) = (((f (#) G) | X) + (F (#) (g | X))) by RFUNCT_1: 45;

      then ((F (#) G) `| X) = (((f (#) G) | X) + ((F (#) g) | X)) by RFUNCT_1: 45;

      then

       A27: ((F (#) G) `| X) = (((f (#) G) + (F (#) g)) | X) by RFUNCT_1: 44;

      (F (#) G) is_differentiable_on X by A19, A13, A20, FDIFF_2: 20;

      then

       A28: (F (#) G) is_integral_of (((f (#) G) + (F (#) g)),X) by A27, Lm1;

      ( min (b,a)) = b by A1, XXREAL_0:def 9;

      then

       A29: ( max (b,a)) = a by XXREAL_0: 36;

      b <= ( max (b,a)) & [.b, a.] = I by A1, INTEGRA5:def 3, XXREAL_0: 25;

      then

       A30: b in I & a in I by A29, XXREAL_1: 1;

      X c= (( dom F) /\ ( dom g)) by A8, A17, XBOOLE_1: 19;

      then X c= ( dom (F (#) g)) by VALUED_1:def 4;

      then

       A31: I c= ( dom (F (#) g)) by A2, XBOOLE_1: 1;

      (G | I) is continuous by A2, A14, FCONT_1: 16;

      then

       A32: G is_integrable_on I by A12, INTEGRA5: 17;

      X c= (( dom f) /\ ( dom G)) by A7, A11, XBOOLE_1: 19;

      then X c= ( dom (f (#) G)) by VALUED_1:def 4;

      then

       A33: I c= ( dom (f (#) G)) by A2, XBOOLE_1: 1;

      I c= ( dom f) by A2, A7, XBOOLE_1: 1;

      then

       A34: (f (#) G) is_integrable_on I by A3, A5, A12, A32, A15, INTEGRA6: 14;

      then ((f (#) G) + (F (#) g)) is_integrable_on I by A33, A31, A26, A16, A23, INTEGRA6: 11;

      then ((F (#) G) . a) = (( integral (((f (#) G) + (F (#) g)),b,a)) + ((F (#) G) . b)) by A1, A2, A24, A28, Th18;

      then ((F (#) G) . b) = ((F . b) * (G . b)) & (((F (#) G) . a) - ((F (#) G) . b)) = (( integral ((f (#) G),b,a)) + ( integral ((F (#) g),b,a))) by A1, A33, A31, A34, A26, A16, A23, A30, INTEGRA6: 24, VALUED_1: 5;

      hence thesis by VALUED_1: 5;

    end;

    theorem :: INTEGRA7:22

    b <= a & [.b, a.] c= X & X c= ( dom f) & X c= ( dom g) & (f | X) is continuous & (g | X) is continuous & F is_integral_of (f,X) & G is_integral_of (g,X) implies (((F . a) * (G . a)) - ((F . b) * (G . b))) = (( integral ((f (#) G),b,a)) + ( integral ((F (#) g),b,a)))

    proof

      assume that

       A1: b <= a and

       A2: [.b, a.] c= X;

      assume that

       A3: X c= ( dom f) and

       A4: X c= ( dom g) and

       A5: (f | X) is continuous and

       A6: (g | X) is continuous and

       A7: F is_integral_of (f,X) & G is_integral_of (g,X);

      

       A8: [.b, a.] c= ( dom f) by A2, A3, XBOOLE_1: 1;

      

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

      then (f | ['b, a']) is continuous by A2, A5, FCONT_1: 16;

      then

       A10: f is_integrable_on ['b, a'] by A8, A9, INTEGRA5: 17;

      

       A11: [.b, a.] c= ( dom g) by A2, A4, XBOOLE_1: 1;

      then

       A12: (g | ['b, a']) is bounded by A2, A6, A9, FCONT_1: 16, INTEGRA5: 10;

      (g | ['b, a']) is continuous by A2, A6, A9, FCONT_1: 16;

      then

       A13: g is_integrable_on ['b, a'] by A11, A9, INTEGRA5: 17;

      (f | ['b, a']) is bounded by A2, A5, A8, A9, FCONT_1: 16, INTEGRA5: 10;

      hence thesis by A1, A2, A3, A4, A7, A9, A10, A13, A12, Th21;

    end;

    begin

    theorem :: INTEGRA7:23

    

     Th23: sin is_integral_of ( cos , REAL )

    proof

      

       A1: ( dom ( cos | REAL )) = ( REAL /\ REAL ) by SIN_COS: 24;

       A2:

      now

        let x be object;

        assume

         A3: x in ( dom ( sin `| REAL ));

        then

        reconsider z = x as Real;

        (( sin `| REAL ) . x) = ( diff ( sin ,z)) by A3, FDIFF_1:def 7, SIN_COS: 68;

        then (( sin `| REAL ) . x) = ( cos . z) by SIN_COS: 64;

        hence (( sin `| REAL ) . x) = (( cos | REAL ) . x);

      end;

      ( dom ( sin `| REAL )) = REAL by FDIFF_1:def 7, SIN_COS: 68;

      then ( sin `| REAL ) = ( cos | REAL ) by A1, A2, FUNCT_1: 2;

      hence thesis by Lm1, SIN_COS: 68;

    end;

    theorem :: INTEGRA7:24

    (( sin . b) - ( sin . a)) = ( integral ( cos ,a,b))

    proof

      

       A1: ( min (a,b)) <= a by XXREAL_0: 17;

      

       A2: REAL = ( dom cos ) & [.( min (a,b)), ( max (a,b)).] c= REAL by FUNCT_2:def 1;

      ( cos | REAL ) is continuous & a <= ( max (a,b)) by FDIFF_1: 25, SIN_COS: 67, XXREAL_0: 25;

      then

       A3: ( sin . ( max (a,b))) = (( integral ( cos ,( min (a,b)),( max (a,b)))) + ( sin . ( min (a,b)))) by A1, A2, Th20, Th23, XXREAL_0: 2;

       A4:

      now

        assume

         A5: ( min (a,b)) = a;

        then ( max (a,b)) = b by XXREAL_0: 36;

        hence thesis by A3, A5;

      end;

      now

        assume

         A6: ( min (a,b)) = b;

        then

         A7: ( max (a,b)) = a by XXREAL_0: 36;

        now

          assume b < a;

          then ( integral ( cos ,a,b)) = ( - ( integral ( cos , ['b, a']))) by INTEGRA5:def 4;

          then ( sin . a) = (( - ( integral ( cos ,a,b))) + ( sin . b)) by A1, A3, A6, A7, INTEGRA5:def 4;

          hence thesis;

        end;

        hence thesis by A1, A4, A6, XXREAL_0: 1;

      end;

      hence thesis by A4, XXREAL_0: 15;

    end;

    theorem :: INTEGRA7:25

    

     Th25: (( - 1) (#) cos ) is_integral_of ( sin , REAL )

    proof

      

       A1: ( dom ( sin | REAL )) = ( REAL /\ REAL ) by SIN_COS: 24;

      

       A2: ( dom (( - 1) (#) cos )) = ( [#] REAL ) by SIN_COS: 24, VALUED_1:def 5;

       A3:

      now

        let x be object;

        assume

         A4: x in ( dom ((( - 1) (#) cos ) `| REAL ));

        then

        reconsider z = x as Real;

        (((( - 1) (#) cos ) `| REAL ) . x) = (( - 1) * ( diff ( cos ,z))) by A2, A4, FDIFF_1: 20, SIN_COS: 67;

        then (((( - 1) (#) cos ) `| REAL ) . x) = (( - 1) * ( - ( sin . z))) by SIN_COS: 63;

        hence (((( - 1) (#) cos ) `| REAL ) . x) = (( sin | REAL ) . x);

      end;

      

       A5: (( - 1) (#) cos ) is_differentiable_on REAL by A2, FDIFF_1: 20, SIN_COS: 67;

      then ( dom ((( - 1) (#) cos ) `| REAL )) = REAL by FDIFF_1:def 7;

      then ((( - 1) (#) cos ) `| REAL ) = ( sin | REAL ) by A1, A3, FUNCT_1: 2;

      hence thesis by A5, Lm1;

    end;

    theorem :: INTEGRA7:26

    (( cos . a) - ( cos . b)) = ( integral ( sin ,a,b))

    proof

      

       A1: ( min (a,b)) <= a by XXREAL_0: 17;

      ( max (a,b)) in REAL by XREAL_0:def 1;

      then

       A2: ( max (a,b)) in ( dom (( - 1) (#) cos )) by SIN_COS: 24, VALUED_1:def 5;

      ( min (a,b)) in REAL by XREAL_0:def 1;

      then

       A3: ( min (a,b)) in ( dom (( - 1) (#) cos )) by SIN_COS: 24, VALUED_1:def 5;

      

       A4: a <= ( max (a,b)) & [.( min (a,b)), ( max (a,b)).] c= REAL by XXREAL_0: 25;

      ( sin | REAL ) is continuous & REAL c= ( dom sin ) by FDIFF_1: 25, FUNCT_2:def 1, SIN_COS: 68;

      then ((( - 1) (#) cos ) . ( max (a,b))) = (( integral ( sin ,( min (a,b)),( max (a,b)))) + ((( - 1) (#) cos ) . ( min (a,b)))) by A1, A4, Th20, Th25, XXREAL_0: 2;

      then (( - 1) * ( cos . ( max (a,b)))) = (( integral ( sin ,( min (a,b)),( max (a,b)))) + ((( - 1) (#) cos ) . ( min (a,b)))) by A2, VALUED_1:def 5;

      then (( - 1) * ( cos . ( max (a,b)))) = (( integral ( sin ,( min (a,b)),( max (a,b)))) + (( - 1) * ( cos . ( min (a,b))))) by A3, VALUED_1:def 5;

      then

       A5: (( cos . ( min (a,b))) - ( cos . ( max (a,b)))) = ( integral ( sin ,( min (a,b)),( max (a,b))));

       A6:

      now

        assume

         A7: ( min (a,b)) = a;

        then ( max (a,b)) = b by XXREAL_0: 36;

        hence thesis by A5, A7;

      end;

      now

        assume

         A8: ( min (a,b)) = b;

        then

         A9: ( max (a,b)) = a by XXREAL_0: 36;

        b < a implies (( cos . a) - ( cos . b)) = ( integral ( sin ,a,b))

        proof

          assume

           A10: b < a;

          then ( integral ( sin ,a,b)) = ( - ( integral ( sin , ['b, a']))) by INTEGRA5:def 4;

          then ( integral ( sin ,a,b)) = ( - ( integral ( sin ,b,a))) by A10, INTEGRA5:def 4;

          hence thesis by A5, A8, A9;

        end;

        hence thesis by A1, A6, A8, XXREAL_0: 1;

      end;

      hence thesis by A6, XXREAL_0: 15;

    end;

    theorem :: INTEGRA7:27

    

     Th27: exp_R is_integral_of ( exp_R , REAL )

    proof

      

       A1: ( dom ( exp_R | REAL )) = ( REAL /\ REAL ) by TAYLOR_1: 16;

       A2:

      now

        let x be object;

        assume

         A3: x in ( dom ( exp_R `| REAL ));

        then

        reconsider z = x as Real;

        reconsider z1 = z as Element of REAL by XREAL_0:def 1;

        (( exp_R `| REAL ) . x) = ( diff ( exp_R ,z)) by A3, FDIFF_1:def 7, TAYLOR_1: 16;

        then (( exp_R `| REAL ) . x) = ( exp_R . z1) by TAYLOR_1: 16;

        hence (( exp_R `| REAL ) . x) = (( exp_R | REAL ) . x);

      end;

      ( dom ( exp_R `| REAL )) = REAL by FDIFF_1:def 7, TAYLOR_1: 16;

      then ( exp_R `| REAL ) = ( exp_R | REAL ) by A1, A2, FUNCT_1: 2;

      hence thesis by Lm1, TAYLOR_1: 16;

    end;

    theorem :: INTEGRA7:28

    (( exp_R . b) - ( exp_R . a)) = ( integral ( exp_R ,a,b))

    proof

      

       A1: ( min (a,b)) <= a by XXREAL_0: 17;

      

       A2: [.( min (a,b)), ( max (a,b)).] c= REAL ;

      ( exp_R | REAL ) is continuous & a <= ( max (a,b)) by FDIFF_1: 25, TAYLOR_1: 16, XXREAL_0: 25;

      then

       A3: ( exp_R . ( max (a,b))) = (( integral ( exp_R ,( min (a,b)),( max (a,b)))) + ( exp_R . ( min (a,b)))) by A1, A2, Th20, Th27, SIN_COS: 47, XXREAL_0: 2;

      

       A4: ( min (a,b)) = a implies (( exp_R . b) - ( exp_R . a)) = ( integral ( exp_R ,a,b))

      proof

        assume

         A5: ( min (a,b)) = a;

        then ( max (a,b)) = b by XXREAL_0: 36;

        hence thesis by A3, A5;

      end;

      ( min (a,b)) = b implies (( exp_R . b) - ( exp_R . a)) = ( integral ( exp_R ,a,b))

      proof

        assume

         A6: ( min (a,b)) = b;

        then

         A7: ( max (a,b)) = a by XXREAL_0: 36;

        b < a implies (( exp_R . b) - ( exp_R . a)) = ( integral ( exp_R ,a,b))

        proof

          assume b < a;

          then ( integral ( exp_R ,a,b)) = ( - ( integral ( exp_R , ['b, a']))) by INTEGRA5:def 4;

          then ( exp_R . a) = (( - ( integral ( exp_R ,a,b))) + ( exp_R . b)) by A1, A3, A6, A7, INTEGRA5:def 4;

          hence thesis;

        end;

        hence thesis by A1, A4, A6, XXREAL_0: 1;

      end;

      hence thesis by A4, XXREAL_0: 15;

    end;

    theorem :: INTEGRA7:29

    

     Th29: ( #Z (n + 1)) is_integral_of (((n + 1) (#) ( #Z n)), REAL )

    proof

      reconsider m = (n + 1) as Nat;

      

       A1: ( dom (((n + 1) (#) ( #Z n)) | REAL )) = ( REAL /\ REAL ) by FUNCT_2:def 1;

      

       A2: ( dom ( #Z (n + 1))) = REAL by FUNCT_2:def 1;

      for x be Real st x in REAL holds (( #Z (n + 1)) | REAL ) is_differentiable_in x by TAYLOR_1: 2;

      then

       A3: ( #Z (n + 1)) is_differentiable_on REAL by A2;

      

       A4: ( dom ( #Z n)) = REAL by FUNCT_2:def 1;

       A5:

      now

        let x be object;

        assume

         A6: x in ( dom (( #Z (n + 1)) `| REAL ));

        then

        reconsider z = x as Real;

        ((( #Z (n + 1)) `| REAL ) . x) = ( diff (( #Z (n + 1)),z)) by A3, A6, FDIFF_1:def 7;

        then ((( #Z (n + 1)) `| REAL ) . x) = (m * (z #Z (m - 1))) by TAYLOR_1: 2;

        then

         A7: ((( #Z (n + 1)) `| REAL ) . x) = ((n + 1) * (( #Z n) . x)) by TAYLOR_1:def 1;

        x in ( dom ( #Z n)) by A4, A6;

        then x in ( dom ((n + 1) (#) ( #Z n))) by VALUED_1:def 5;

        then ((( #Z (n + 1)) `| REAL ) . x) = (((n + 1) (#) ( #Z n)) . x) by A7, VALUED_1:def 5;

        hence ((( #Z (n + 1)) `| REAL ) . x) = ((((n + 1) (#) ( #Z n)) | REAL ) . x);

      end;

      ( dom (( #Z (n + 1)) `| REAL )) = REAL by A3, FDIFF_1:def 7;

      then (( #Z (n + 1)) `| REAL ) = (((n + 1) (#) ( #Z n)) | REAL ) by A1, A5, FUNCT_1: 2;

      hence thesis by A3, Lm1;

    end;

    theorem :: INTEGRA7:30

    ((( #Z (n + 1)) . b) - (( #Z (n + 1)) . a)) = ( integral (((n + 1) (#) ( #Z n)),a,b))

    proof

      

       A1: ( [#] REAL ) c= ( dom ((n + 1) (#) ( #Z n))) by FUNCT_2:def 1;

      

       A2: ( dom ( #Z n)) = REAL by FUNCT_2:def 1;

      for x be Real st x in REAL holds (( #Z n) | REAL ) is_differentiable_in x by TAYLOR_1: 2;

      then ( #Z n) is_differentiable_on REAL by A2;

      then

       A3: (((n + 1) (#) ( #Z n)) | REAL ) is continuous by A1, FDIFF_1: 20, FDIFF_1: 25;

      

       A4: ( min (a,b)) <= a by XXREAL_0: 17;

      

       A5: [.( min (a,b)), ( max (a,b)).] c= REAL ;

      a <= ( max (a,b)) by XXREAL_0: 25;

      then ( min (a,b)) <= ( max (a,b)) by A4, XXREAL_0: 2;

      then

       A6: (( #Z (n + 1)) . ( max (a,b))) = (( integral (((n + 1) (#) ( #Z n)),( min (a,b)),( max (a,b)))) + (( #Z (n + 1)) . ( min (a,b)))) by A1, A3, A5, Th20, Th29;

      

       A7: ( min (a,b)) = a implies ((( #Z (n + 1)) . b) - (( #Z (n + 1)) . a)) = ( integral (((n + 1) (#) ( #Z n)),a,b))

      proof

        assume

         A8: ( min (a,b)) = a;

        then ( max (a,b)) = b by XXREAL_0: 36;

        hence thesis by A6, A8;

      end;

      ( min (a,b)) = b implies ((( #Z (n + 1)) . b) - (( #Z (n + 1)) . a)) = ( integral (((n + 1) (#) ( #Z n)),a,b))

      proof

        assume

         A9: ( min (a,b)) = b;

        then

         A10: ( max (a,b)) = a by XXREAL_0: 36;

        b < a implies ((( #Z (n + 1)) . b) - (( #Z (n + 1)) . a)) = ( integral (((n + 1) (#) ( #Z n)),a,b))

        proof

          assume b < a;

          then ( integral (((n + 1) (#) ( #Z n)),a,b)) = ( - ( integral (((n + 1) (#) ( #Z n)), ['b, a']))) by INTEGRA5:def 4;

          then (( #Z (n + 1)) . a) = (( - ( integral (((n + 1) (#) ( #Z n)),a,b))) + (( #Z (n + 1)) . b)) by A4, A6, A9, A10, INTEGRA5:def 4;

          hence thesis;

        end;

        hence thesis by A4, A7, A9, XXREAL_0: 1;

      end;

      hence thesis by A7, XXREAL_0: 15;

    end;

    begin

    theorem :: INTEGRA7:31

    for H be Functional_Sequence of REAL , REAL , rseq be Real_Sequence st a < b & (for n be Element of NAT holds (H . n) is_integrable_on ['a, b'] & ((H . n) | ['a, b']) is bounded & (rseq . n) = ( integral ((H . n),a,b))) & H is_unif_conv_on ['a, b'] holds (( lim (H, ['a, b'])) | ['a, b']) is bounded & ( lim (H, ['a, b'])) is_integrable_on ['a, b'] & rseq is convergent & ( lim rseq) = ( integral (( lim (H, ['a, b'])),a,b))

    proof

      let H be Functional_Sequence of REAL , REAL , rseq be Real_Sequence;

      set AB = ['a, b'];

      assume that

       A1: a < b and

       A2: for n be Element of NAT holds (H . n) is_integrable_on AB & ((H . n) | AB) is bounded & (rseq . n) = ( integral ((H . n),a,b)) and

       A3: H is_unif_conv_on AB;

      consider T be DivSequence of AB such that

       A4: ( delta T) is convergent & ( lim ( delta T)) = 0 by INTEGRA4: 11;

      

       A5: for n be Nat holds (H . n) is_integrable_on AB & ((H . n) | AB) is bounded & (rseq . n) = ( integral ((H . n),a,b))

      proof

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A2;

      end;

      

       A6: AB common_on_dom H by A3, SEQFUNC: 43;

      

       A7: for n be Element of NAT holds ((H . n) || AB) is Function of AB, REAL & (((H . n) || AB) | AB) is bounded & ( lower_sum (((H . n) || AB),T)) is convergent & ( lim ( lower_sum (((H . n) || AB),T))) = ( lower_integral ((H . n) || AB)) & ( upper_sum (((H . n) || AB),T)) is convergent & ( lim ( upper_sum (((H . n) || AB),T))) = ( upper_integral ((H . n) || AB)) & ( lower_integral ((H . n) || AB)) = ( upper_integral ((H . n) || AB)) & (rseq . n) = ( integral ((H . n) || AB))

      proof

        let n be Element of NAT ;

        AB c= ( dom (H . n)) by A6, SEQFUNC:def 9;

        hence

         A8: ((H . n) || AB) is Function of AB, REAL by FUNCT_2: 68, INTEGRA5: 6;

        thus (((H . n) || AB) | AB) is bounded by A2;

        hence ( lower_sum (((H . n) || AB),T)) is convergent & ( lim ( lower_sum (((H . n) || AB),T))) = ( lower_integral ((H . n) || AB)) & ( upper_sum (((H . n) || AB),T)) is convergent & ( lim ( upper_sum (((H . n) || AB),T))) = ( upper_integral ((H . n) || AB)) by A4, A8, INTEGRA4: 8, INTEGRA4: 9;

        (H . n) is_integrable_on AB by A2;

        then ((H . n) || AB) is integrable;

        hence ( lower_integral ((H . n) || AB)) = ( upper_integral ((H . n) || AB));

        (rseq . n) = ( integral ((H . n),a,b)) by A2;

        then (rseq . n) = ( integral ((H . n),AB)) by A1, INTEGRA5:def 4;

        hence thesis;

      end;

      set L1 = ( lower_integral (( lim (H,AB)) || AB));

      set K1 = ( upper_integral (( lim (H,AB)) || AB));

      

       A9: 0 < (b - a) by A1, XREAL_1: 50;

      reconsider jj = 1 as Real;

      consider K be Nat such that

       A10: for n be Nat, x be Element of REAL st n >= K & x in AB holds |.(((H . n) . x) - (( lim (H,AB)) . x)).| < jj by A3, SEQFUNC: 43;

      ((H . K) | AB) is bounded by A5;

      then

      consider r be Real such that

       A11: for c be object st c in (AB /\ ( dom (H . K))) holds |.((H . K) . c).| <= r by RFUNCT_1: 73;

      set H0 = (( lim (H,AB)) || AB);

      H is_point_conv_on AB by A3, SEQFUNC: 22;

      then

       A12: ( dom ( lim (H,AB))) = AB by SEQFUNC: 21;

      then

       A13: H0 is Function of AB, REAL by FUNCT_2: 68, INTEGRA5: 6;

      ( dom ( lim (H,AB))) c= ( dom (H . K)) by A6, A12, SEQFUNC:def 9;

      then

       A14: (AB /\ ( dom ( lim (H,AB)))) c= (AB /\ ( dom (H . K))) by XBOOLE_1: 26;

      now

        let c be object;

        (( lim (H,AB)) . c) = (((H . K) . c) - (((H . K) . c) - (( lim (H,AB)) . c)));

        then

         A15: |.(( lim (H,AB)) . c).| <= ( |.((H . K) . c).| + |.(((H . K) . c) - (( lim (H,AB)) . c)).|) by COMPLEX1: 57;

        assume

         A16: c in (AB /\ ( dom ( lim (H,AB))));

        then c in AB by XBOOLE_0:def 4;

        then

         A17: |.(((H . K) . c) - (( lim (H,AB)) . c)).| < 1 by A10;

         |.((H . K) . c).| <= r by A11, A14, A16;

        then ( |.((H . K) . c).| + |.(((H . K) . c) - (( lim (H,AB)) . c)).|) <= (r + 1) by A17, XREAL_1: 7;

        hence |.(( lim (H,AB)) . c).| <= (r + 1) by A15, XXREAL_0: 2;

      end;

      hence

       A18: (( lim (H,AB)) | AB) is bounded by RFUNCT_1: 73;

      then

       A19: (H0 | AB) is bounded_above;

      

       A20: (H0 | AB) is bounded_below by A18;

      then

       A21: ( upper_sum (H0,T)) is convergent by A4, A19, A13, INTEGRA4: 9;

      

       A22: for e be Real st 0 < e holds ex N be Element of NAT st for n,k be Element of NAT st N <= n holds |.((( upper_sum (((H . n) || AB),T)) . k) - (( upper_sum (H0,T)) . k)).| <= (e * (b - a))

      proof

        let e be Real;

        assume 0 < e;

        then

        consider N be Nat such that

         A23: for n be Nat, x be Element of REAL st n >= N & x in AB holds |.(((H . n) . x) - (( lim (H,AB)) . x)).| < e by A3, SEQFUNC: 43;

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

        take N;

        let n,k be Element of NAT ;

        reconsider Tk = (T . k) as Division of AB;

        set l0 = ( len Tk);

        

         A24: ( dom Tk) = ( Seg l0) by FINSEQ_1:def 3;

        set Hn = ((H . n) || AB);

        ( len ( upper_volume (Hn,(T . k)))) = l0 by INTEGRA1:def 6;

        then

        reconsider R1 = ( upper_volume (Hn,(T . k))) as Element of (l0 -tuples_on REAL ) by FINSEQ_2: 92;

        ( len ( upper_volume (H0,(T . k)))) = l0 by INTEGRA1:def 6;

        then

        reconsider R2 = ( upper_volume (H0,(T . k))) as Element of (l0 -tuples_on REAL ) by FINSEQ_2: 92;

        ((( upper_sum (H0,T)) . k) - (( upper_sum (Hn,T)) . k)) = (( upper_sum (H0,(T . k))) - (( upper_sum (Hn,T)) . k)) by INTEGRA2:def 2;

        then ((( upper_sum (H0,T)) . k) - (( upper_sum (Hn,T)) . k)) = (( upper_sum (H0,(T . k))) - ( upper_sum (Hn,(T . k)))) by INTEGRA2:def 2;

        then

         A25: ((( upper_sum (H0,T)) . k) - (( upper_sum (Hn,T)) . k)) = ( Sum (R2 - R1)) by RVSUM_1: 90;

        consider H1 be Function of AB, REAL such that

         A26: ( rng H1) = {e} and

         A27: (H1 | AB) is bounded by INTEGRA4: 5;

        ( len ( upper_volume (H1,(T . k)))) = l0 by INTEGRA1:def 6;

        then

        reconsider R3 = ( upper_volume (H1,(T . k))) as Element of (l0 -tuples_on REAL ) by FINSEQ_2: 92;

        

         A28: ( vol AB) = (b - a) by A1, INTEGRA6: 5;

        ( upper_bound ( rng H1)) = e by A26, SEQ_4: 9;

        then

         A29: ( upper_sum (H1,(T . k))) <= (e * (b - a)) by A27, A28, INTEGRA1: 27;

        assume

         A30: N <= n;

        

         A31: for i be Element of NAT st i in ( dom Tk) holds ((R1 - R2) . i) <= (R3 . i) & ((R2 - R1) . i) <= (R3 . i)

        proof

          let i be Element of NAT ;

          

           A32: 0 <= ( vol ( divset ((T . k),i))) by INTEGRA1: 9;

          assume

           A33: i in ( dom Tk);

          

           A34: (( upper_bound ( rng (Hn | ( divset ((T . k),i))))) - ( upper_bound ( rng (H0 | ( divset ((T . k),i)))))) <= ( upper_bound ( rng (H1 | ( divset ((T . k),i))))) & (( upper_bound ( rng (H0 | ( divset ((T . k),i))))) - ( upper_bound ( rng (Hn | ( divset ((T . k),i)))))) <= ( upper_bound ( rng (H1 | ( divset ((T . k),i)))))

          proof

            

             A35: ( divset ((T . k),i)) c= AB by A33, INTEGRA1: 8;

            then

            reconsider g = (H0 | ( divset ((T . k),i))) as Function of ( divset ((T . k),i)), REAL by A13, FUNCT_2: 32;

            consider x0 be object such that

             A36: x0 in ( divset ((T . k),i)) by XBOOLE_0:def 1;

            Hn is Function of AB, REAL by A7;

            then

            reconsider f = (Hn | ( divset ((T . k),i))) as Function of ( divset ((T . k),i)), REAL by A35, FUNCT_2: 32;

            

             A37: for x be set st x in ( divset ((T . k),i)) holds |.((f . x) - (g . x)).| <= e

            proof

              let x be set;

              assume

               A38: x in ( divset ((T . k),i));

              then |.((f . x) - (g . x)).| = |.((Hn . x) - (g . x)).| by FUNCT_1: 49;

              then |.((f . x) - (g . x)).| = |.((Hn . x) - (H0 . x)).| by A38, FUNCT_1: 49;

              then |.((f . x) - (g . x)).| = |.(((H . n) . x) - (H0 . x)).| by A35, A38, FUNCT_1: 49;

              then |.((f . x) - (g . x)).| = |.(((H . n) . x) - (( lim (H,AB)) . x)).| by A35, A38, FUNCT_1: 49;

              hence thesis by A23, A30, A35, A38;

            end;

            (Hn | AB) is bounded by A7;

            then (f | ( divset ((T . k),i))) is bounded_above by A33, INTEGRA1: 8, INTEGRA2: 5;

            then

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

            (H1 . x0) in {e} by A26, A35, A36, FUNCT_2: 4;

            then (H1 . x0) = e by TARSKI:def 1;

            then

             A40: ((H1 | ( divset ((T . k),i))) . x0) = e by A36, FUNCT_1: 49;

            (H1 | ( divset ((T . k),i))) is Function of ( divset ((T . k),i)), REAL by A35, FUNCT_2: 32;

            then e in ( rng (H1 | ( divset ((T . k),i)))) by A36, A40, FUNCT_2: 4;

            then

             A41: {e} c= ( rng (H1 | ( divset ((T . k),i)))) by ZFMISC_1: 31;

            ( rng (H1 | ( divset ((T . k),i)))) c= {e} by A26, RELAT_1: 70;

            then ( rng (H1 | ( divset ((T . k),i)))) = {e} by A41, XBOOLE_0:def 10;

            then

             A42: e = ( upper_bound ( rng (H1 | ( divset ((T . k),i))))) by SEQ_4: 9;

            (g | ( divset ((T . k),i))) is bounded_above by A19, A33, INTEGRA1: 8, INTEGRA2: 5;

            then

             A43: ( rng g) is bounded_above by INTEGRA1: 13;

            hence (( upper_bound ( rng (Hn | ( divset ((T . k),i))))) - ( upper_bound ( rng (H0 | ( divset ((T . k),i)))))) <= ( upper_bound ( rng (H1 | ( divset ((T . k),i))))) by A39, A42, A37, Th1;

            for x be set st x in ( divset ((T . k),i)) holds |.((g . x) - (f . x)).| <= ( upper_bound ( rng (H1 | ( divset ((T . k),i)))))

            proof

              let x be set;

              assume x in ( divset ((T . k),i));

              then |.((f . x) - (g . x)).| <= ( upper_bound ( rng (H1 | ( divset ((T . k),i))))) by A42, A37;

              hence thesis by COMPLEX1: 60;

            end;

            hence thesis by A39, A43, Th1;

          end;

          ((R1 - R2) . i) = ((R1 . i) - (R2 . i)) by RVSUM_1: 27;

          then ((R1 - R2) . i) = ((( upper_bound ( rng (Hn | ( divset ((T . k),i))))) * ( vol ( divset ((T . k),i)))) - (( upper_volume (H0,(T . k))) . i)) by A33, INTEGRA1:def 6;

          then ((R1 - R2) . i) = ((( upper_bound ( rng (Hn | ( divset ((T . k),i))))) * ( vol ( divset ((T . k),i)))) - (( upper_bound ( rng (H0 | ( divset ((T . k),i))))) * ( vol ( divset ((T . k),i))))) by A33, INTEGRA1:def 6;

          then ((R1 - R2) . i) = ((( upper_bound ( rng (Hn | ( divset ((T . k),i))))) - ( upper_bound ( rng (H0 | ( divset ((T . k),i)))))) * ( vol ( divset ((T . k),i))));

          then ((R1 - R2) . i) <= (( upper_bound ( rng (H1 | ( divset ((T . k),i))))) * ( vol ( divset ((T . k),i)))) by A34, A32, XREAL_1: 64;

          hence ((R1 - R2) . i) <= (R3 . i) by A33, INTEGRA1:def 6;

          ((R2 - R1) . i) = ((R2 . i) - (R1 . i)) by RVSUM_1: 27;

          then ((R2 - R1) . i) = ((( upper_bound ( rng (H0 | ( divset ((T . k),i))))) * ( vol ( divset ((T . k),i)))) - (( upper_volume (Hn,(T . k))) . i)) by A33, INTEGRA1:def 6;

          then ((R2 - R1) . i) = ((( upper_bound ( rng (H0 | ( divset ((T . k),i))))) * ( vol ( divset ((T . k),i)))) - (( upper_bound ( rng (Hn | ( divset ((T . k),i))))) * ( vol ( divset ((T . k),i))))) by A33, INTEGRA1:def 6;

          then ((R2 - R1) . i) = ((( upper_bound ( rng (H0 | ( divset ((T . k),i))))) - ( upper_bound ( rng (Hn | ( divset ((T . k),i)))))) * ( vol ( divset ((T . k),i))));

          then ((R2 - R1) . i) <= (( upper_bound ( rng (H1 | ( divset ((T . k),i))))) * ( vol ( divset ((T . k),i)))) by A34, A32, XREAL_1: 64;

          hence thesis by A33, INTEGRA1:def 6;

        end;

        then for i be Nat st i in ( dom Tk) holds ((R2 - R1) . i) <= (R3 . i);

        then ((( upper_sum (H0,T)) . k) - (( upper_sum (Hn,T)) . k)) <= ( Sum R3) by A24, A25, RVSUM_1: 82;

        then ((( upper_sum (H0,T)) . k) - (( upper_sum (Hn,T)) . k)) <= (e * (b - a)) by A29, XXREAL_0: 2;

        then

         A44: ( - (e * (b - a))) <= ( - ((( upper_sum (H0,T)) . k) - (( upper_sum (((H . n) || AB),T)) . k))) by XREAL_1: 24;

        ((( upper_sum (Hn,T)) . k) - (( upper_sum (H0,T)) . k)) = (( upper_sum (Hn,(T . k))) - (( upper_sum (H0,T)) . k)) by INTEGRA2:def 2;

        then ((( upper_sum (Hn,T)) . k) - (( upper_sum (H0,T)) . k)) = (( upper_sum (Hn,(T . k))) - ( upper_sum (H0,(T . k)))) by INTEGRA2:def 2;

        then

         A45: ((( upper_sum (Hn,T)) . k) - (( upper_sum (H0,T)) . k)) = ( Sum (R1 - R2)) by RVSUM_1: 90;

        for i be Nat st i in ( Seg l0) holds ((R1 - R2) . i) <= (R3 . i) by A24, A31;

        then ((( upper_sum (Hn,T)) . k) - (( upper_sum (H0,T)) . k)) <= ( Sum R3) by A45, RVSUM_1: 82;

        then ((( upper_sum (((H . n) || AB),T)) . k) - (( upper_sum (H0,T)) . k)) <= (e * (b - a)) by A29, XXREAL_0: 2;

        hence |.((( upper_sum (((H . n) || AB),T)) . k) - (( upper_sum (H0,T)) . k)).| <= (e * (b - a)) by A44, ABSVALUE: 5;

      end;

      

       A46: for e be Real st 0 < e holds ex N be Element of NAT st for n be Element of NAT st N <= n holds |.(( upper_integral ((H . n) || AB)) - ( upper_integral (( lim (H,AB)) || AB))).| <= e

      proof

        let e be Real;

        reconsider ee = e as Real;

        assume 0 < e;

        then

        consider N be Element of NAT such that

         A47: for n,k be Element of NAT st N <= n holds |.((( upper_sum (((H . n) || AB),T)) . k) - (( upper_sum (H0,T)) . k)).| <= ((ee / (b - a)) * (b - a)) by A22, A9, XREAL_1: 139;

        take N;

         A48:

        now

          let n,k be Element of NAT ;

          assume N <= n;

          then |.((( upper_sum (((H . n) || AB),T)) . k) - (( upper_sum (H0,T)) . k)).| <= ((e / (b - a)) * (b - a)) by A47;

          hence |.((( upper_sum (((H . n) || AB),T)) . k) - (( upper_sum (H0,T)) . k)).| <= e by A9, XCMPLX_1: 87;

        end;

        hereby

          let n be Element of NAT ;

          assume

           A49: N <= n;

           A50:

          now

            let k be Nat;

            k in NAT by ORDINAL1:def 12;

            then |.((( upper_sum (((H . n) || AB),T)) . k) - (( upper_sum (H0,T)) . k)).| <= e by A48, A49;

            then |.((( upper_sum (((H . n) || AB),T)) . k) + (( - ( upper_sum (H0,T))) . k)).| <= e by SEQ_1: 10;

            then |.((( upper_sum (((H . n) || AB),T)) + ( - ( upper_sum (H0,T)))) . k).| <= e by SEQ_1: 7;

            hence ( |.(( upper_sum (((H . n) || AB),T)) - ( upper_sum (H0,T))).| . k) <= e by SEQ_1: 12;

          end;

          

           A51: ( upper_sum (((H . n) || AB),T)) is convergent by A7;

          then ( lim (( upper_sum (((H . n) || AB),T)) - ( upper_sum (H0,T)))) = (( lim ( upper_sum (((H . n) || AB),T))) - ( lim ( upper_sum (H0,T)))) by A21, SEQ_2: 12;

          then ( lim (( upper_sum (((H . n) || AB),T)) - ( upper_sum (H0,T)))) = (( upper_integral ((H . n) || AB)) - ( lim ( upper_sum (H0,T)))) by A7;

          then

           A52: ( lim (( upper_sum (((H . n) || AB),T)) - ( upper_sum (H0,T)))) = (( upper_integral ((H . n) || AB)) - ( upper_integral (( lim (H,AB)) || AB))) by A4, A19, A20, A13, INTEGRA4: 9;

          

           A53: (( upper_sum (((H . n) || AB),T)) - ( upper_sum (H0,T))) is convergent by A21, A51;

          then ( abs (( upper_sum (((H . n) || AB),T)) - ( upper_sum (H0,T)))) is convergent by SEQ_4: 13;

          then ( lim |.(( upper_sum (((H . n) || AB),T)) - ( upper_sum (H0,T))).|) <= e by A50, PREPOWER: 2;

          hence |.(( upper_integral ((H . n) || AB)) - ( upper_integral (( lim (H,AB)) || AB))).| <= e by A53, A52, SEQ_4: 14;

        end;

      end;

      

       A54: ( lower_sum (H0,T)) is convergent by A4, A19, A20, A13, INTEGRA4: 8;

      

       A55: for e be Real st 0 < e holds ex N be Element of NAT st for n,k be Element of NAT st N <= n holds |.((( lower_sum (((H . n) || AB),T)) . k) - (( lower_sum (H0,T)) . k)).| <= (e * (b - a))

      proof

        let e be Real;

        assume 0 < e;

        then

        consider N be Nat such that

         A56: for n be Nat, x be Element of REAL st n >= N & x in AB holds |.(((H . n) . x) - (( lim (H,AB)) . x)).| < e by A3, SEQFUNC: 43;

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

        take N;

        hereby

          let n,k be Element of NAT ;

          set Hn = ((H . n) || AB);

          reconsider Tk = (T . k) as Division of AB;

          set l0 = ( len Tk);

          consider H1 be Function of AB, REAL such that

           A57: ( rng H1) = {e} and

           A58: (H1 | AB) is bounded by INTEGRA4: 5;

          

           A59: ( lower_sum (H1,(T . k))) <= ( upper_sum (H1,(T . k))) by A58, INTEGRA1: 28;

          ( len ( lower_volume (H0,(T . k)))) = l0 by INTEGRA1:def 7;

          then

          reconsider R2 = ( lower_volume (H0,(T . k))) as Element of (l0 -tuples_on REAL ) by FINSEQ_2: 92;

          ( len ( lower_volume (Hn,(T . k)))) = l0 by INTEGRA1:def 7;

          then

          reconsider R1 = ( lower_volume (Hn,(T . k))) as Element of (l0 -tuples_on REAL ) by FINSEQ_2: 92;

          ( len ( lower_volume (H1,(T . k)))) = l0 by INTEGRA1:def 7;

          then

          reconsider R3 = ( lower_volume (H1,(T . k))) as Element of (l0 -tuples_on REAL ) by FINSEQ_2: 92;

          assume

           A60: N <= n;

          

           A61: for i be Element of NAT st i in ( dom Tk) holds ((R1 - R2) . i) <= (R3 . i) & ((R2 - R1) . i) <= (R3 . i)

          proof

            let i be Element of NAT ;

            consider x0 be object such that

             A62: x0 in ( divset ((T . k),i)) by XBOOLE_0:def 1;

            

             A63: ( rng (H1 | ( divset ((T . k),i)))) c= {e} by A57, RELAT_1: 70;

            assume

             A64: i in ( dom Tk);

            then

             A65: ( divset ((T . k),i)) c= AB by INTEGRA1: 8;

            then

            reconsider g = (H0 | ( divset ((T . k),i))) as Function of ( divset ((T . k),i)), REAL by A13, FUNCT_2: 32;

            Hn is Function of AB, REAL by A7;

            then

            reconsider f = (Hn | ( divset ((T . k),i))) as Function of ( divset ((T . k),i)), REAL by A65, FUNCT_2: 32;

            

             A66: 0 <= ( vol ( divset ((T . k),i))) by INTEGRA1: 9;

            (H1 . x0) in {e} by A57, A65, A62, FUNCT_2: 4;

            then (H1 . x0) = e by TARSKI:def 1;

            then

             A67: ((H1 | ( divset ((T . k),i))) . x0) = e by A62, FUNCT_1: 49;

            (H1 | ( divset ((T . k),i))) is Function of ( divset ((T . k),i)), REAL by A65, FUNCT_2: 32;

            then e in ( rng (H1 | ( divset ((T . k),i)))) by A62, A67, FUNCT_2: 4;

            then {e} c= ( rng (H1 | ( divset ((T . k),i)))) by ZFMISC_1: 31;

            then ( rng (H1 | ( divset ((T . k),i)))) = {e} by A63, XBOOLE_0:def 10;

            then

             A68: e = ( lower_bound ( rng (H1 | ( divset ((T . k),i))))) by SEQ_4: 9;

             A69:

            now

              let x be set;

              assume

               A70: x in ( divset ((T . k),i));

              then |.((f . x) - (g . x)).| = |.((Hn . x) - (g . x)).| by FUNCT_1: 49;

              then |.((f . x) - (g . x)).| = |.((Hn . x) - (H0 . x)).| by A70, FUNCT_1: 49;

              then |.((f . x) - (g . x)).| = |.(((H . n) . x) - (H0 . x)).| by A65, A70, FUNCT_1: 49;

              then |.((f . x) - (g . x)).| = |.(((H . n) . x) - (( lim (H,AB)) . x)).| by A65, A70, FUNCT_1: 49;

              hence |.((f . x) - (g . x)).| <= e by A56, A60, A65, A70;

            end;

            ((R2 - R1) . i) = ((R2 . i) - (R1 . i)) by RVSUM_1: 27;

            then ((R2 - R1) . i) = ((( lower_bound ( rng (H0 | ( divset ((T . k),i))))) * ( vol ( divset ((T . k),i)))) - (( lower_volume (Hn,(T . k))) . i)) by A64, INTEGRA1:def 7;

            then ((R2 - R1) . i) = ((( lower_bound ( rng (H0 | ( divset ((T . k),i))))) * ( vol ( divset ((T . k),i)))) - (( lower_bound ( rng (Hn | ( divset ((T . k),i))))) * ( vol ( divset ((T . k),i))))) by A64, INTEGRA1:def 7;

            then

             A71: ((R2 - R1) . i) = ((( lower_bound ( rng (H0 | ( divset ((T . k),i))))) - ( lower_bound ( rng (Hn | ( divset ((T . k),i)))))) * ( vol ( divset ((T . k),i))));

            ((R1 - R2) . i) = ((R1 . i) - (R2 . i)) by RVSUM_1: 27;

            then ((R1 - R2) . i) = ((( lower_bound ( rng (Hn | ( divset ((T . k),i))))) * ( vol ( divset ((T . k),i)))) - (( lower_volume (H0,(T . k))) . i)) by A64, INTEGRA1:def 7;

            then ((R1 - R2) . i) = ((( lower_bound ( rng (Hn | ( divset ((T . k),i))))) * ( vol ( divset ((T . k),i)))) - (( lower_bound ( rng (H0 | ( divset ((T . k),i))))) * ( vol ( divset ((T . k),i))))) by A64, INTEGRA1:def 7;

            then

             A72: ((R1 - R2) . i) = ((( lower_bound ( rng (Hn | ( divset ((T . k),i))))) - ( lower_bound ( rng (H0 | ( divset ((T . k),i)))))) * ( vol ( divset ((T . k),i))));

            (Hn | AB) is bounded by A7;

            then (f | ( divset ((T . k),i))) is bounded_below by A64, INTEGRA1: 8, INTEGRA2: 6;

            then

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

            (g | ( divset ((T . k),i))) is bounded_below by A20, A64, INTEGRA1: 8, INTEGRA2: 6;

            then

             A74: ( rng g) is bounded_below by INTEGRA1: 11;

            then (( lower_bound ( rng (Hn | ( divset ((T . k),i))))) - ( lower_bound ( rng (H0 | ( divset ((T . k),i)))))) <= ( lower_bound ( rng (H1 | ( divset ((T . k),i))))) by A73, A68, A69, Th2;

            then ((R1 - R2) . i) <= (( lower_bound ( rng (H1 | ( divset ((T . k),i))))) * ( vol ( divset ((T . k),i)))) by A72, A66, XREAL_1: 64;

            hence ((R1 - R2) . i) <= (R3 . i) by A64, INTEGRA1:def 7;

            now

              let x be set;

              assume x in ( divset ((T . k),i));

              then |.((f . x) - (g . x)).| <= ( lower_bound ( rng (H1 | ( divset ((T . k),i))))) by A68, A69;

              hence |.((g . x) - (f . x)).| <= ( lower_bound ( rng (H1 | ( divset ((T . k),i))))) by COMPLEX1: 60;

            end;

            then (( lower_bound ( rng (H0 | ( divset ((T . k),i))))) - ( lower_bound ( rng (Hn | ( divset ((T . k),i)))))) <= ( lower_bound ( rng (H1 | ( divset ((T . k),i))))) by A73, A74, Th2;

            then ((R2 - R1) . i) <= (( lower_bound ( rng (H1 | ( divset ((T . k),i))))) * ( vol ( divset ((T . k),i)))) by A71, A66, XREAL_1: 64;

            hence thesis by A64, INTEGRA1:def 7;

          end;

          ((( lower_sum (Hn,T)) . k) - (( lower_sum (H0,T)) . k)) = (( lower_sum (Hn,(T . k))) - (( lower_sum (H0,T)) . k)) by INTEGRA2:def 3;

          then ((( lower_sum (Hn,T)) . k) - (( lower_sum (H0,T)) . k)) = (( lower_sum (Hn,(T . k))) - ( lower_sum (H0,(T . k)))) by INTEGRA2:def 3;

          then

           A75: ((( lower_sum (Hn,T)) . k) - (( lower_sum (H0,T)) . k)) = ( Sum (R1 - R2)) by RVSUM_1: 90;

          

           A76: ( vol AB) = (b - a) by A1, INTEGRA6: 5;

          ( upper_bound ( rng H1)) = e by A57, SEQ_4: 9;

          then ( upper_sum (H1,(T . k))) <= (e * (b - a)) by A58, A76, INTEGRA1: 27;

          then

           A77: ( lower_sum (H1,(T . k))) <= (e * (b - a)) by A59, XXREAL_0: 2;

          ((( lower_sum (H0,T)) . k) - (( lower_sum (Hn,T)) . k)) = (( lower_sum (H0,(T . k))) - (( lower_sum (Hn,T)) . k)) by INTEGRA2:def 3;

          then ((( lower_sum (H0,T)) . k) - (( lower_sum (Hn,T)) . k)) = (( lower_sum (H0,(T . k))) - ( lower_sum (Hn,(T . k)))) by INTEGRA2:def 3;

          then

           A78: ((( lower_sum (H0,T)) . k) - (( lower_sum (Hn,T)) . k)) = ( Sum (R2 - R1)) by RVSUM_1: 90;

          

           A79: ( Seg l0) = ( dom Tk) by FINSEQ_1:def 3;

          then for i be Nat st i in ( Seg l0) holds ((R2 - R1) . i) <= (R3 . i) by A61;

          then ((( lower_sum (H0,T)) . k) - (( lower_sum (Hn,T)) . k)) <= ( Sum R3) by A78, RVSUM_1: 82;

          then ((( lower_sum (H0,T)) . k) - (( lower_sum (Hn,T)) . k)) <= (e * (b - a)) by A77, XXREAL_0: 2;

          then

           A80: ( - (e * (b - a))) <= ( - ((( lower_sum (H0,T)) . k) - (( lower_sum (((H . n) || AB),T)) . k))) by XREAL_1: 24;

          for i be Nat st i in ( Seg l0) holds ((R1 - R2) . i) <= (R3 . i) by A79, A61;

          then ((( lower_sum (Hn,T)) . k) - (( lower_sum (H0,T)) . k)) <= ( lower_sum (H1,(T . k))) by A75, RVSUM_1: 82;

          then ((( lower_sum (((H . n) || AB),T)) . k) - (( lower_sum (H0,T)) . k)) <= (e * (b - a)) by A77, XXREAL_0: 2;

          hence |.((( lower_sum (((H . n) || AB),T)) . k) - (( lower_sum (H0,T)) . k)).| <= (e * (b - a)) by A80, ABSVALUE: 5;

        end;

      end;

      

       A81: for e be Real st 0 < e holds ex N be Element of NAT st for n,k be Element of NAT st N <= n holds |.((( lower_sum (((H . n) || AB),T)) . k) - (( lower_sum (H0,T)) . k)).| <= e

      proof

        let e be Real;

        assume 0 < e;

        then

        consider N be Element of NAT such that

         A82: for n,k be Element of NAT st N <= n holds |.((( lower_sum (((H . n) || AB),T)) . k) - (( lower_sum (H0,T)) . k)).| <= ((e / (b - a)) * (b - a)) by A55, A9, XREAL_1: 139;

        take N;

        hereby

          let n,k be Element of NAT ;

          assume N <= n;

          then |.((( lower_sum (((H . n) || AB),T)) . k) - (( lower_sum (H0,T)) . k)).| <= ((e / (b - a)) * (b - a)) by A82;

          hence |.((( lower_sum (((H . n) || AB),T)) . k) - (( lower_sum (H0,T)) . k)).| <= e by A9, XCMPLX_1: 87;

        end;

      end;

      

       A83: for e be Real st 0 < e holds ex N be Element of NAT st for n be Element of NAT st N <= n holds |.(( lower_integral ((H . n) || AB)) - ( lower_integral (( lim (H,AB)) || AB))).| <= e

      proof

        let e be Real;

        assume 0 < e;

        then

        consider N be Element of NAT such that

         A84: for n,k be Element of NAT st N <= n holds |.((( lower_sum (((H . n) || AB),T)) . k) - (( lower_sum (H0,T)) . k)).| <= e by A81;

        take N;

        hereby

          let n be Element of NAT ;

          set LHT = ( lower_sum (((H . n) || AB),T));

          assume

           A85: N <= n;

           A86:

          now

            let k be Nat;

            k in NAT by ORDINAL1:def 12;

            then |.((LHT . k) - (( lower_sum (H0,T)) . k)).| <= e by A84, A85;

            then |.((LHT . k) + (( - ( lower_sum (H0,T))) . k)).| <= e by SEQ_1: 10;

            then |.((LHT + ( - ( lower_sum (H0,T)))) . k).| <= e by SEQ_1: 7;

            hence (( abs (LHT - ( lower_sum (H0,T)))) . k) <= e by SEQ_1: 12;

          end;

          

           A87: LHT is convergent by A7;

          then ( lim (LHT - ( lower_sum (H0,T)))) = (( lim LHT) - ( lim ( lower_sum (H0,T)))) by A54, SEQ_2: 12;

          then ( lim (LHT - ( lower_sum (H0,T)))) = (( lower_integral ((H . n) || AB)) - ( lim ( lower_sum (H0,T)))) by A7;

          then

           A88: ( lim (LHT - ( lower_sum (H0,T)))) = (( lower_integral ((H . n) || AB)) - ( lower_integral (( lim (H,AB)) || AB))) by A4, A19, A20, A13, INTEGRA4: 8;

          

           A89: (LHT - ( lower_sum (H0,T))) is convergent by A54, A87;

          then |.(LHT - ( lower_sum (H0,T))).| is convergent by SEQ_4: 13;

          then ( lim |.(LHT - ( lower_sum (H0,T))).|) <= e by A86, PREPOWER: 2;

          hence |.(( lower_integral ((H . n) || AB)) - ( lower_integral (( lim (H,AB)) || AB))).| <= e by A88, A89, SEQ_4: 14;

        end;

      end;

       A90:

      now

        let e1 be Real;

        set e = (e1 / 2);

        assume

         A91: 0 < e1;

        then

         A92: 0 < (e1 / 2) by XREAL_1: 215;

        then

        consider N1 be Element of NAT such that

         A93: for n be Element of NAT st N1 <= n holds |.(( upper_integral ((H . n) || AB)) - ( upper_integral (( lim (H,AB)) || AB))).| <= (e / 2) by A46, XREAL_1: 215;

        consider N2 be Element of NAT such that

         A94: for n be Element of NAT st N2 <= n holds |.(( lower_integral ((H . n) || AB)) - ( lower_integral (( lim (H,AB)) || AB))).| <= (e / 2) by A83, A92, XREAL_1: 215;

        reconsider n = ( max (N1,N2)) as Element of NAT ;

        set K = ( upper_integral ((H . n) || AB));

        set L = ( lower_integral ((H . n) || AB));

         |.(L - L1).| <= (e / 2) by A94, XXREAL_0: 25;

        then

         A95: |.(K - L1).| <= (e / 2) by A7;

        ((K - K1) - (K - L1)) = (L1 - K1);

        then

         A96: |.(L1 - K1).| <= ( |.(K - K1).| + |.(K - L1).|) by COMPLEX1: 57;

         |.(K - K1).| <= (e / 2) by A93, XXREAL_0: 25;

        then ( |.(K - K1).| + |.(K - L1).|) <= ((e / 2) + (e / 2)) by A95, XREAL_1: 7;

        then

         A97: |.(L1 - K1).| <= e by A96, XXREAL_0: 2;

        (e1 / 2) < e1 by A91, XREAL_1: 216;

        hence |.(L1 - K1).| < e1 by A97, XXREAL_0: 2;

      end;

      

       A98: K1 = L1 by COMPLEX1: 62, A90;

      H0 is upper_integrable & H0 is lower_integrable by A19, A20, A13, INTEGRA4: 10;

      then (( lim (H,AB)) || AB) is integrable by A98;

      hence ( lim (H,AB)) is_integrable_on AB;

      

       A99: for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.((rseq . m) - ( integral (( lim (H,AB)),a,b))).| < p

      proof

        let p be Real;

        set e = (p / 2);

        assume

         A100: 0 < p;

        then

        consider N be Element of NAT such that

         A101: for n be Element of NAT st N <= n holds |.(( upper_integral ((H . n) || AB)) - ( upper_integral (( lim (H,AB)) || AB))).| <= e by A46, XREAL_1: 215;

        take N;

        

         A102: (p / 2) < p by A100, XREAL_1: 216;

        hereby

          let n be Nat;

          

           A103: n in NAT by ORDINAL1:def 12;

          ( upper_integral ((H . n) || AB)) = ( integral ((H . n) || AB));

          then

           A104: ( upper_integral ((H . n) || AB)) = (rseq . n) by A7, A103;

          ( upper_integral (( lim (H,AB)) || AB)) = ( integral (( lim (H,AB)),AB));

          then

           A105: ( upper_integral (( lim (H,AB)) || AB)) = ( integral (( lim (H,AB)),a,b)) by A1, INTEGRA5:def 4;

          assume N <= n;

          then |.(( upper_integral ((H . n) || AB)) - ( upper_integral (( lim (H,AB)) || AB))).| <= e by A101, A103;

          hence |.((rseq . n) - ( integral (( lim (H,AB)),a,b))).| < p by A102, A104, A105, XXREAL_0: 2;

        end;

      end;

      hence rseq is convergent by SEQ_2:def 6;

      hence thesis by A99, SEQ_2:def 7;

    end;