integr21.miz



    begin

    reserve Z for RealNormSpace;

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

    reserve A,B for non empty closed_interval Subset of REAL ;

    

     Lm2: a <= b & c in ['a, b'] & d in ['a, b'] implies ['( min (c,d)), ( max (c,d))'] c= ['a, b']

    proof

      assume

       A1: a <= b & c in ['a, b'] & d in ['a, b'];

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

      then

       A2: a <= c & d <= b & a <= d & c <= b by A1, XXREAL_1: 1;

      per cases ;

        suppose

         A3: c <= d;

        then

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

         ['c, b'] c= ['a, b'] & ['c, d'] c= ['c, b'] by A2, A3, INTEGR19: 1;

        hence ['( min (c,d)), ( max (c,d))'] c= ['a, b'] by A4;

      end;

        suppose

         A6: not c <= d;

        then

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

         ['d, b'] c= ['a, b'] & ['d, c'] c= ['d, b'] by A2, A6, INTEGR19: 1;

        hence ['( min (c,d)), ( max (c,d))'] c= ['a, b'] by A7;

      end;

    end;

    

     Lm3: for X,Y,Z be non empty set, f be PartFunc of X, Y st Z c= ( dom f) holds (f | Z) is Function of Z, Y

    proof

      let X,Y,Z be non empty set, f be PartFunc of X, Y;

      ( rng f) c= Y;

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

      hence thesis by FUNCT_2: 32;

    end;

    theorem :: INTEGR21:1

    

     Th1915: for f be PartFunc of REAL , the carrier of Z st f is bounded & A c= ( dom f) holds (f | A) is bounded

    proof

      let f be PartFunc of REAL , the carrier of Z;

      assume that

       A1: f is bounded and

       A2: A c= ( dom f);

      consider r be Real such that

       A3: for x be set st x in ( dom f) holds ||.(f /. x).|| < r by A1;

      now

        let x be set;

        assume x in ( dom (f | A));

        then ||.(f /. x).|| < r & x in (( dom f) /\ A) by A3, A2, RELAT_1: 61;

        hence ||.((f | A) /. x).|| < r by PARTFUN2: 16;

      end;

      hence (f | A) is bounded;

    end;

    theorem :: INTEGR21:2

    

     Th1915a: for f be PartFunc of REAL , the carrier of Z st (f | A) is bounded & B c= A & B c= ( dom (f | A)) holds (f | B) is bounded

    proof

      let f be PartFunc of REAL , the carrier of Z;

      assume

       A1: (f | A) is bounded & B c= A & B c= ( dom (f | A));

      set g = (f | A);

      

       A4: (g | B) is bounded by Th1915, A1;

      consider r be Real such that

       A5: for x be set st x in ( dom (g | B)) holds ||.((g | B) /. x).|| < r by A4;

      (g | B) = (f | B) by A1, RELAT_1: 74;

      hence (f | B) is bounded by A5;

    end;

    theorem :: INTEGR21:3

    

     Th1915b: for f be PartFunc of REAL , the carrier of Z st a <= c & c <= d & d <= b & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) holds (f | ['c, d']) is bounded

    proof

      let f be PartFunc of REAL , the carrier of Z;

      assume

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

      

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

      then

       A4: c in ['a, b'] & d in ['a, b'] by A1, INTEGR19: 1;

      reconsider A = ['a, b'], B = ['c, d'] as non empty closed_interval Subset of REAL ;

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

      then

       A5: B c= A by A2, A1, XXREAL_0: 2, A4, Lm2;

      then B c= ( dom (f | A)) by A1, RELAT_1: 62;

      hence (f | ['c, d']) is bounded by A1, A5, Th1915a;

    end;

    theorem :: INTEGR21:4

    

     Th1935: for X,Y be set, f1,f2 be PartFunc of REAL , the carrier of Z st (f1 | X) is bounded & (f2 | Y) is bounded holds ((f1 + f2) | (X /\ Y)) is bounded & ((f1 - f2) | (X /\ Y)) is bounded

    proof

      let X,Y be set, f1,f2 be PartFunc of REAL , the carrier of Z;

      assume

       A1: (f1 | X) is bounded & (f2 | Y) is bounded;

      consider r1 be Real such that

       A2: for x be set st x in ( dom (f1 | X)) holds ||.((f1 | X) /. x).|| < r1 by A1;

      consider r2 be Real such that

       A3: for x be set st x in ( dom (f2 | Y)) holds ||.((f2 | Y) /. x).|| < r2 by A1;

      now

        let x be set;

        assume

         A41: x in ( dom ((f1 + f2) | (X /\ Y)));

        then

         A4: x in ( dom (f1 + f2)) & x in (X /\ Y) by RELAT_1: 57;

        then x in (( dom f1) /\ ( dom f2)) by VFUNCT_1:def 1;

        then

         A5: x in ( dom f1) & x in ( dom f2) & x in X & x in Y by A41, XBOOLE_0:def 4;

        then

         A6: x in ( dom (f2 | Y)) by RELAT_1: 57;

        (((f1 + f2) | (X /\ Y)) /. x) = ((f1 + f2) /. x) by A4, PARTFUN2: 17

        .= ((f1 /. x) + (f2 /. x)) by A4, VFUNCT_1:def 1

        .= (((f1 | X) /. x) + (f2 /. x)) by A5, PARTFUN2: 17

        .= (((f1 | X) /. x) + ((f2 | Y) /. x)) by A5, PARTFUN2: 17;

        then

         A7: ||.(((f1 + f2) | (X /\ Y)) /. x).|| <= ( ||.((f1 | X) /. x).|| + ||.((f2 | Y) /. x).||) by NORMSP_1:def 1;

         ||.((f1 | X) /. x).|| < r1 by A2, A5, RELAT_1: 57;

        then ( ||.((f1 | X) /. x).|| + ||.((f2 | Y) /. x).||) < (r1 + r2) by A3, A6, XREAL_1: 8;

        hence ||.(((f1 + f2) | (X /\ Y)) /. x).|| < (r1 + r2) by A7, XXREAL_0: 2;

      end;

      hence ((f1 + f2) | (X /\ Y)) is bounded;

      take (r1 + r2);

      let x be set;

      assume

       A8: x in ( dom ((f1 - f2) | (X /\ Y)));

      then

       A9: x in ( dom (f1 - f2)) & x in (X /\ Y) by RELAT_1: 57;

      then x in (( dom f1) /\ ( dom f2)) by VFUNCT_1:def 2;

      then

       A10: x in ( dom f1) & x in ( dom f2) & x in X & x in Y by A8, XBOOLE_0:def 4;

      then

       A11: x in ( dom (f2 | Y)) by RELAT_1: 57;

      (((f1 - f2) | (X /\ Y)) /. x) = ((f1 - f2) /. x) by A9, PARTFUN2: 17

      .= ((f1 /. x) - (f2 /. x)) by A9, VFUNCT_1:def 2

      .= (((f1 | X) /. x) - (f2 /. x)) by A10, PARTFUN2: 17

      .= (((f1 | X) /. x) - ((f2 | Y) /. x)) by A10, PARTFUN2: 17;

      then

       A12: ||.(((f1 - f2) | (X /\ Y)) /. x).|| <= ( ||.((f1 | X) /. x).|| + ||.((f2 | Y) /. x).||) by NORMSP_1: 3;

       ||.((f1 | X) /. x).|| < r1 by A2, A10, RELAT_1: 57;

      then ( ||.((f1 | X) /. x).|| + ||.((f2 | Y) /. x).||) < (r1 + r2) by A11, A3, XREAL_1: 8;

      hence ||.(((f1 - f2) | (X /\ Y)) /. x).|| < (r1 + r2) by A12, XXREAL_0: 2;

    end;

    theorem :: INTEGR21:5

    

     Th1935a: for X be set, f be PartFunc of REAL , the carrier of Z st (f | X) is bounded holds ((r (#) f) | X) is bounded

    proof

      let X be set, f be PartFunc of REAL , the carrier of Z;

      assume (f | X) is bounded;

      then

      consider s be Real such that

       A2: for x be set st x in ( dom (f | X)) holds ||.((f | X) /. x).|| < s;

      reconsider p = (( |.r.| * |.s.|) + 1) as Real;

      take p;

      now

        let x be set;

        assume

         A3: x in ( dom ((r (#) f) | X));

        then

         A4: x in (( dom (r (#) f)) /\ X) by RELAT_1: 61;

        

         A5: x in X & x in ( dom (r (#) f)) by A3, RELAT_1: 57;

        then

         A6: x in X & x in ( dom f) by VFUNCT_1:def 4;

        then

         A7: x in (( dom f) /\ X) by XBOOLE_0:def 4;

        

         A8: ||.((f | X) /. x).|| < s by A2, A6, RELAT_1: 57;

        ((r (#) f) /. x) = (r * (f /. x)) by VFUNCT_1:def 4, A5;

        then (((r (#) f) | X) /. x) = (r * (f /. x)) by A4, PARTFUN2: 16;

        

        then

         A11: ||.(((r (#) f) | X) /. x).|| = ||.(r * ((f | X) /. x)).|| by A7, PARTFUN2: 16

        .= ( |.r.| * ||.((f | X) /. x).||) by NORMSP_1:def 1;

         0 <= |.r.| by COMPLEX1: 46;

        then ( |.r.| * s) <= ( |.r.| * |.s.|) & ( |.r.| * ||.((f | X) /. x).||) <= ( |.r.| * s) by A8, ABSVALUE: 4, XREAL_1: 64;

        then ( |.r.| * ||.((f | X) /. x).||) <= ( |.r.| * |.s.|) by XXREAL_0: 2;

        hence ||.(((r (#) f) | X) /. x).|| < p by A11, XREAL_1: 145;

      end;

      hence thesis;

    end;

    theorem :: INTEGR21:6

    

     Th1935b: for X be set, f be PartFunc of REAL , the carrier of Z st (f | X) is bounded holds (( - f) | X) is bounded

    proof

      let X be set, f be PartFunc of REAL , the carrier of Z;

      assume (f | X) is bounded;

      then

      consider s be Real such that

       A2: for x be set st x in ( dom (f | X)) holds ||.((f | X) /. x).|| < s;

      now

        let x be set;

        assume x in ( dom (( - f) | X));

        then

         A4: x in ( dom ( - (f | X))) by VFUNCT_1: 29;

        then x in ( dom (f | X)) by VFUNCT_1:def 5;

        then

         A5: ||.((f | X) /. x).|| < s by A2;

        ((( - f) | X) /. x) = (( - (f | X)) /. x) by VFUNCT_1: 29

        .= ( - ((f | X) /. x)) by A4, VFUNCT_1:def 5;

        hence ||.((( - f) | X) /. x).|| < s by A5, NORMSP_1: 2;

      end;

      hence (( - f) | X) is bounded;

    end;

    theorem :: INTEGR21:7

    

     Th1914: for f be Function of A, the carrier of Z holds f is bounded iff ||.f.|| is bounded

    proof

      let f be Function of A, the carrier of Z;

      hereby

        assume

         A1: f is bounded;

        consider r be Real such that

         A2: for x be set st x in ( dom f) holds ||.(f /. x).|| < r by A1;

        now

          let x be set;

          assume

           A3: x in ( dom ||.f.||);

          then x in ( dom f) by NORMSP_0:def 2;

          then

           A4: ||.(f /. x).|| < r by A2;

           ||.(f /. x).|| = ( ||.f.|| . x) by A3, NORMSP_0:def 2;

          hence |.( ||.f.|| . x).| < r by A4, ABSVALUE:def 1;

        end;

        hence ||.f.|| is bounded by COMSEQ_2:def 3;

      end;

      assume ||.f.|| is bounded;

      then

      consider r be Real such that

       B2: for x be set st x in ( dom ||.f.||) holds |.( ||.f.|| . x).| < r by COMSEQ_2:def 3;

      now

        let x be set;

        assume x in ( dom f);

        then

         B3: x in ( dom ||.f.||) by NORMSP_0:def 2;

        then

         B4: |.( ||.f.|| . x).| < r by B2;

        ( ||.f.|| . x) = ||.(f /. x).|| by B3, NORMSP_0:def 2;

        hence ||.(f /. x).|| < r by B4, ABSVALUE:def 1;

      end;

      hence f is bounded;

    end;

    theorem :: INTEGR21:8

    

     Th1918: for f be PartFunc of REAL , the carrier of Z st A c= ( dom f) holds ||.(f | A).|| = ( ||.f.|| | A)

    proof

      let f be PartFunc of REAL , the carrier of Z;

      assume

       A1: A c= ( dom f);

      then

       A2: ( dom (f | A)) = A by RELAT_1: 62;

      

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

      then

       A6: ( dom ( ||.f.|| | A)) = (( dom f) /\ A) by NORMSP_0:def 3;

      then ( dom ( ||.f.|| | A)) = A by A1, XBOOLE_1: 28;

      then

       A4: ( dom ||.(f | A).||) = ( dom ( ||.f.|| | A)) by A2, NORMSP_0:def 3;

      now

        let x be object;

        assume

         A5: x in ( dom ( ||.f.|| | A));

        then

         A9: x in ( dom ||.f.||) & x in ( dom f) by A3, A6, XBOOLE_0:def 4;

        

        then

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

        .= ((f | A) . x) by FUNCT_1: 49, A5

        .= ((f | A) /. x) by A2, PARTFUN1:def 6, A5;

        

        thus (( ||.f.|| | A) . x) = ( ||.f.|| . x) by FUNCT_1: 49, A5

        .= ||.(f /. x).|| by A9, NORMSP_0:def 3

        .= ( ||.(f | A).|| . x) by A11, A4, A5, NORMSP_0:def 3;

      end;

      hence thesis by A4, FUNCT_1: 2;

    end;

    theorem :: INTEGR21:9

    

     Th1919: for g be PartFunc of REAL , the carrier of Z st A c= ( dom g) & (g | A) is bounded holds ( ||.g.|| | A) is bounded

    proof

      let g be PartFunc of REAL , the carrier of Z;

      assume

       A1: A c= ( dom g) & (g | A) is bounded;

      then

       A2: ||.(g | A).|| = ( ||.g.|| | A) by Th1918;

      reconsider h = (g | A) as Function of A, the carrier of Z by A1, Lm3;

      h is bounded by A1;

      hence thesis by A2, Th1914;

    end;

    begin

    reserve X,Y for RealBanachSpace;

    reserve E for Point of Y;

    theorem :: INTEGR21:10

    

     Th3: for Y be RealNormSpace, f be continuous PartFunc of REAL , the carrier of Y st a <= b & ['a, b'] c= ( dom f) holds ( ||.f.|| | ['a, b']) is bounded

    proof

      let Y be RealNormSpace, f be continuous PartFunc of REAL , the carrier of Y;

      assume

       A1: a <= b & ['a, b'] c= ( dom f);

      

       P11: (f | ['a, b']) is continuous;

       ['a, b'] c= ( dom ||.f.||) by NORMSP_0:def 3, A1;

      hence thesis by P11, A1, NFCONT_3: 22, INTEGRA5: 10;

    end;

    theorem :: INTEGR21:11

    

     Th1: for Y be RealNormSpace, f be continuous PartFunc of REAL , the carrier of Y st a <= b & ['a, b'] c= ( dom f) holds (f | ['a, b']) is bounded

    proof

      let Y be RealNormSpace, f be continuous PartFunc of REAL , the carrier of Y;

      set h = ( ||.f.|| | ['a, b']);

      set g = (f | ['a, b']);

      assume

       A1: a <= b & ['a, b'] c= ( dom f);

      then h is bounded by Th3;

      then

      consider r be Real such that

       P2: for y be set st y in ( dom h) holds |.(h . y).| < r by COMSEQ_2:def 3;

      

       D1: ( dom ||.f.||) = ( dom f) by NORMSP_0:def 3;

      for y be set st y in ( dom g) holds ||.(g /. y).|| < r

      proof

        let y be set;

        assume

         P3: y in ( dom g);

        then

         P5: y in ['a, b'] by A1, RELAT_1: 62;

        then

         P6: y in ( dom h) by A1, D1, RELAT_1: 62;

        

         P81: (h . y) = ( ||.f.|| . y) by P5, FUNCT_1: 49

        .= ||.(f /. y).|| by NORMSP_0:def 2, D1, P5, A1;

        (f /. y) = (f . y) by PARTFUN1:def 6, P5, A1

        .= (g . y) by P5, FUNCT_1: 49

        .= (g /. y) by PARTFUN1:def 6, P3;

        then |.(h . y).| = ||.(g /. y).|| by P81, ABSVALUE:def 1;

        hence thesis by P2, P6;

      end;

      hence thesis;

    end;

    theorem :: INTEGR21:12

    

     Th4: for Y be RealNormSpace, f be continuous PartFunc of REAL , the carrier of Y st a <= b & ['a, b'] c= ( dom f) holds ||.f.|| is_integrable_on ['a, b']

    proof

      let Y be RealNormSpace, f be continuous PartFunc of REAL , the carrier of Y;

      assume

       A1: a <= b & ['a, b'] c= ( dom f);

      

       P11: (f | ['a, b']) is continuous;

       ['a, b'] c= ( dom ||.f.||) by NORMSP_0:def 3, A1;

      hence ||.f.|| is_integrable_on ['a, b'] by P11, A1, NFCONT_3: 22, INTEGRA5: 11;

    end;

    theorem :: INTEGR21:13

    

     Th1909: for f be continuous PartFunc of REAL , the carrier of Y st a <= c & c <= d & d <= b & ['a, b'] c= ( dom f) holds f is_integrable_on ['c, d']

    proof

      let f be continuous PartFunc of REAL , the carrier of Y;

      assume

       A1: a <= c & c <= d & d <= b & ['a, b'] c= ( dom f);

      then

       A2: c <= b & a <= d by XXREAL_0: 2;

      then

       A4: c in ['a, b'] & d in ['a, b'] by A1, INTEGR19: 1;

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

      then ['c, d'] c= ['a, b'] by A2, A1, XXREAL_0: 2, A4, Lm2;

      then ['c, d'] c= ( dom f) by A1;

      hence f is_integrable_on ['c, d'] by A1, INTEGR20: 19;

    end;

    theorem :: INTEGR21:14

    

     Th1947: for f be PartFunc of REAL , the carrier of Y st a <= b & ['a, b'] c= ( dom f) holds ( integral (f,b,a)) = ( - ( integral (f,a,b)))

    proof

      let f be PartFunc of REAL , the carrier of Y;

      assume

       A1: a <= b & ['a, b'] c= ( dom f);

      then

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

      ( integral (f, ['a, b'])) = ( integral (f,a,b)) by A2, INTEGR18: 16;

      hence thesis by A2, A1, INTEGR18: 18;

    end;

    

     Lm62: for f be continuous PartFunc of REAL , the carrier of X st a <= b & ['a, b'] c= ( dom f) & c in ['a, b'] & b <> c holds ( integral (f,a,b)) = (( integral (f,a,c)) + ( integral (f,c,b)))

    proof

      let f be continuous PartFunc of REAL , the carrier of X;

      assume that

       A1: a <= b and

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

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

       A6: b <> c;

      reconsider AB = ['a, b'], AC = ['a, c'], CB = ['c, b'] as non empty closed_interval Subset of REAL ;

      

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

      then

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

      then

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

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

      then

       A11: ( upper_bound CB) = b & ( lower_bound CB) = c & ( upper_bound AC) = c & ( lower_bound AC) = a & ( upper_bound AB) = b & ( lower_bound AB) = a by A7, A9, INTEGRA1: 5;

      

       C1: f is_integrable_on AB & f is_integrable_on AC & f is_integrable_on CB by A1, A2, A8, Th1909;

      consider FAB be Function of AB, the carrier of X such that

       C3: FAB = (f | AB) & FAB is integrable by C1;

      consider FAC be Function of AC, the carrier of X such that

       C4: FAC = (f | AC) & FAC is integrable by C1;

      consider FCB be Function of CB, the carrier of X such that

       C5: FCB = (f | CB) & FCB is integrable by C1;

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

      then ( vol CB) > 0 by A11, XREAL_1: 50;

      then

      consider PS2 be DivSequence of CB such that

       A25: ( delta PS2) is convergent & ( lim ( delta PS2)) = 0 & for n be Element of NAT holds ex Tn be Division of CB st Tn divide_into_equal (n + 1) & (PS2 . n) = Tn by INTEGRA6: 16;

      

       A27: for i be Element of NAT st 2 <= i holds ex S2i be Division of CB st S2i = (PS2 . i) & 2 <= ( len S2i)

      proof

        let i be Element of NAT ;

        assume

         A22: 2 <= i;

        consider Tn be Division of CB such that

         A23: Tn divide_into_equal (i + 1) & (PS2 . i) = Tn by A25;

        take Tn;

        thus Tn = (PS2 . i) by A23;

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

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

      end;

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

      

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

      proof

        let n be Element of NAT ;

        reconsider D = (PS2 . (n + 2)) as Element of ( divs CB) by INTEGRA1:def 3;

        take D;

        thus thesis;

      end;

      consider S2 be sequence of ( divs CB) such that

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

      reconsider S2 as DivSequence of CB;

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

       A30:

      now

        let i be Element of NAT ;

        ex n be Nat, e be Division of CB st n = i & e = (S2 . i) & e = (PS2 . (n + 2)) by A29;

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

      end;

      

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

      proof

        let i be Element of NAT ;

        consider S be Division of CB such that

         A32: S = (S2 . i) & 2 <= ( len S) by A30;

        set T = (S /^ 1);

        

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

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

        then

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

        then

        reconsider T as non empty increasing FinSequence of REAL by A32, INTEGRA1: 34, XXREAL_0: 2;

        ( len T) in ( dom T) by A35, FINSEQ_3: 25;

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

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

        then

         A36: (T . ( len T)) = ( upper_bound CB) by INTEGRA1:def 2;

        ( rng S) c= CB & ( rng T) c= ( rng S) by FINSEQ_5: 33, INTEGRA1:def 2;

        then ( rng T) c= CB;

        then T is Division of CB by A36, INTEGRA1:def 2;

        then T is Element of ( divs CB) by INTEGRA1:def 3;

        hence thesis by A32;

      end;

      consider T2 be DivSequence of CB such that

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

      

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

      proof

        let n be Element of NAT ;

        reconsider D = (T2 . n) as Division of CB;

        take D;

        consider E be Division of CB such that

         A40: E = (S2 . n) & (T2 . n) = (E /^ 1) by A38;

        

         A42: ex E1 be Division of CB st E1 = (S2 . n) & 2 <= ( len E1) by A30;

        then

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

        

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

        then

         A45: 1 in ( dom E) by FINSEQ_3: 25;

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

        then

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

        2 in ( dom E) by A40, A42, FINSEQ_3: 25;

        then

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

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

        then

         A48: 1 in ( dom D) by A43, FINSEQ_3: 25;

        then

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

        then

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

        now

          let i be Element of NAT ;

          assume

           A51: i in ( dom D);

          then

           A52: 1 <= i by FINSEQ_3: 25;

          now

            assume i <> 1;

            then 1 < i by A52, XXREAL_0: 1;

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

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

          end;

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

        end;

        hence thesis;

      end;

      consider T1 be DivSequence of AC such that

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

      

       A54: for n be Element of NAT holds ex D be Division of CB st D = (T2 . n) & 1 <= ( len D)

      proof

        let n be Element of NAT ;

        reconsider D = (T2 . n) as Division of CB;

        take D;

        consider E be Division of CB such that

         A55: E = (S2 . n) & (T2 . n) = (E /^ 1) by A38;

        ex E1 be Division of CB st E1 = (S2 . n) & 2 <= ( len E1) by A30;

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

        hence thesis by A55, RFINSEQ:def 1;

      end;

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

      

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

      proof

        let i0 be Element of NAT ;

        reconsider S1 = (T1 . i0) as Division of AC;

        reconsider S2 = (T2 . i0) as Division of CB;

        set T = (S1 ^ S2);

        ex D be Division of CB st D = (T2 . i0) & 1 <= ( len D) by A54;

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

        then

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

        

         A63: ( rng S1) c= AC by INTEGRA1:def 2;

        now

          let i,j be Nat;

          assume that

           A64: i in ( dom T) & j in ( dom T) and

           A66: i < j;

          

           A67: 1 <= i & i <= ( len T) & 1 <= j & j <= ( len T) by A64, FINSEQ_3: 25;

          then i <= (( len S1) + ( len S2)) & j <= (( len S1) + ( len S2)) by FINSEQ_1: 22;

          then

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

          

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

           A70:

          now

            assume

             A72: j > ( len S1);

            then

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

            

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

            then

            consider m be Nat such that

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

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

            then

             A76: (j - ( len S1)) in ( dom S2) by A71, A74, XREAL_1: 19, FINSEQ_3: 25;

             A77:

            now

              assume

               A80: i > ( len S1);

              then

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

              then

              consider m be Nat such that

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

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

              then

               A83: (i - ( len S1)) in ( dom S2) by A71, A81, XREAL_1: 19, FINSEQ_3: 25;

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

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

            end;

            now

              assume i <= ( len S1);

              then

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

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

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

              then

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

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

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

            end;

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

          end;

          now

            assume

             A87: j <= ( len S1);

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

            then

             A88: j in ( dom S1) & i in ( dom S1) by A67, A87, FINSEQ_3: 25;

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

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

          end;

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

        end;

        then

        reconsider T as non empty increasing FinSequence of REAL by SEQM_3:def 1;

        ( rng S2) c= CB by INTEGRA1:def 2;

        then (( rng S1) \/ ( rng S2)) c= (AC \/ CB) by A63, XBOOLE_1: 13;

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

        then

         A92: ( rng T) c= AB by A7, FINSEQ_1: 31;

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

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

        .= ( upper_bound AB) by A11, INTEGRA1:def 2;

        then

        reconsider T as Division of AB by A92, INTEGRA1:def 2;

        T is Element of ( divs AB) by INTEGRA1:def 3;

        hence thesis;

      end;

      consider T be DivSequence of AB such that

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

      reconsider T as DivSequence of AB;

      reconsider T1 as DivSequence of AC;

      reconsider T2 as DivSequence of CB;

      set h1 = FAB, g1 = FAC, g2 = FCB;

      set F1 = the middle_volume_Sequence of FAC, T1;

      set F2 = the middle_volume_Sequence of FCB, T2;

      

       B57: ( integral (f,c,b)) = ( integral (f,CB)) & ( integral (f,a,c)) = ( integral (f,AC)) by A9, INTEGR18: 16;

      

       A17: CB c= AB & AC c= AB by A7, A8, A9, XXREAL_1: 34;

      then CB c= ( dom f) & AC c= ( dom f) by A2;

      then

       A57: ( integral (f,c,b)) = ( integral FCB) & ( integral (f,a,c)) = ( integral FAC) by B57, C4, C5, INTEGR18: 9;

      

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

      proof

        let i,k be Element of NAT , S0 be Division of AC;

        assume

         A96: S0 = (T1 . i);

        reconsider S = (T . i) as Division of AB;

        

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

        consider S1 be Division of AC, S2 be Division of CB such that

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

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

        assume

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

        then

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

        then

         A102: k in ( dom S) by A99, FINSEQ_3: 22;

        

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

         A104:

        now

          assume

           A106: k <> 1;

          1 <= k by A100, FINSEQ_1: 1;

          then 1 < k by A106, XXREAL_0: 1;

          then (k - 1) in ( Seg ( len S1)) by A96, A98, A100, FINSEQ_3: 12;

          then

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

          

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

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

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

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

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

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

        end;

        now

          assume

           A110: k = 1;

          

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

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

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

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

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

        end;

        hence thesis by A104;

      end;

      

       A112: for i,k be Element of NAT , S01 be Division of AC, S02 be Division of CB st S01 = (T1 . i) & S02 = (T2 . i) & k in ( Seg ( len S02)) holds ( divset ((T . i),(( len S01) + k))) = ( divset ((T2 . i),k))

      proof

        let i,k be Element of NAT , S01 be Division of AC, S02 be Division of CB;

        assume

         A113: S01 = (T1 . i) & S02 = (T2 . i);

        reconsider S = (T . i) as Division of AB;

        consider S1 be Division of AC, S2 be Division of CB such that

         A115: S1 = (T1 . i) & S2 = (T2 . i) and

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

        assume

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

        then

         A119: k in ( dom S2) by A113, A115, FINSEQ_1:def 3;

        then

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

        

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

        

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

         A123:

        now

          assume

           A125: k <> 1;

          

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

          then 1 < k by A125, XXREAL_0: 1;

          then (k - 1) in ( Seg ( len S2)) by A113, A115, A118, FINSEQ_3: 12;

          then

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

          

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

          

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

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

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

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

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

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

        end;

        now

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

          then

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

          assume

           A132: k = 1;

          ( len S1) <> 0 ;

          then

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

          

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

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

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

          .= [.( lower_bound CB), (S . (( len S1) + k)).] by A11, A120, A133, INTEGRA1:def 4

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

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

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

        end;

        hence thesis by A113, A115, A123;

      end;

      

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

      proof

        let i,k be Element of NAT , S0 be Division of CB;

        assume

         A135: S0 = (T2 . i) & k in ( Seg ( len S0));

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

        hence thesis by A135, INTEGRA1: 8;

      end;

      

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

      proof

        let i,k be Element of NAT , S0 be Division of AC;

        assume

         A140: S0 = (T1 . i) & k in ( Seg ( len S0));

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

        hence thesis by A140, INTEGRA1: 8;

      end;

      defpred P1[ Nat, set] means ex q,q1,q2 be FinSequence of the carrier of X st q = $2 & q1 = (F1 . $1) & q2 = (F2 . $1) & q = (q1 ^ q2);

      

       B12: for k be Element of NAT holds ex y be Element of (the carrier of X * ) st P1[k, y]

      proof

        let k be Element of NAT ;

        reconsider p1 = (F1 . k) as FinSequence of the carrier of X;

        reconsider p2 = (F2 . k) as FinSequence of X;

        (p1 ^ p2) in (the carrier of X * ) by FINSEQ_1:def 11;

        hence ex p be Element of (the carrier of X * ) st P1[k, p];

      end;

      consider Sh1 be sequence of (the carrier of X * ) such that

       B22: for x be Element of NAT holds P1[x, (Sh1 . x)] from FUNCT_2:sch 3( B12);

      now

        let k be Element of NAT ;

        consider q,q1,q2 be FinSequence of the carrier of X such that

         B221: q = (Sh1 . k) & q1 = (F1 . k) & q2 = (F2 . k) & q = (q1 ^ q2) by B22;

        consider S1 be Division of AC, S2 be Division of CB such that

         U1: S1 = (T1 . k) & S2 = (T2 . k) & (T . k) = (S1 ^ S2) by A93;

        

         X1: ( len (F1 . k)) = ( len (T1 . k)) & ( len (F2 . k)) = ( len (T2 . k)) by INTEGR18:def 1;

        then

         B226: ( len (Sh1 . k)) = (( len (T1 . k)) + ( len (T2 . k))) & ( len (T . k)) = (( len (T1 . k)) + ( len (T2 . k))) by U1, B221, FINSEQ_1: 22;

        for i be Nat st i in ( dom (T . k)) holds ex c be Point of X st c in ( rng (h1 | ( divset ((T . k),i)))) & ((Sh1 . k) . i) = (( vol ( divset ((T . k),i))) * c)

        proof

          let i be Nat;

          assume i in ( dom (T . k));

          per cases by U1, FINSEQ_1: 25;

            suppose

             VC1: i in ( dom S1);

            then

             VC3: ex c be Point of X st c in ( rng (g1 | ( divset ((T1 . k),i)))) & ((F1 . k) . i) = (( vol ( divset ((T1 . k),i))) * c) by INTEGR18:def 1, U1;

            

             VC41: i in ( dom (F1 . k)) by VC1, U1, X1, FINSEQ_3: 29;

            

             V1: i in ( Seg ( len S1)) by VC1, FINSEQ_1:def 3;

            

             V6: ( divset ((T1 . k),i)) = ( divset ((T . k),i)) by V1, A95, U1;

            ( divset ((T1 . k),i)) c= AC by V1, U1, A139;

            then

             V4: ( divset ((T1 . k),i)) c= AB by A17;

            ((f | AC) | ( divset ((T1 . k),i))) = (f | ( divset ((T1 . k),i))) by RELAT_1: 74, V1, U1, A139;

            then (g1 | ( divset ((T1 . k),i))) = (h1 | ( divset ((T . k),i))) by C3, C4, V6, RELAT_1: 74, V4;

            hence thesis by VC3, VC41, B221, FINSEQ_1:def 7, V6;

          end;

            suppose ex n be Nat st n in ( dom S2) & i = (( len S1) + n);

            then

            consider n be Nat such that

             C20: n in ( dom S2) & i = (( len S1) + n);

            

             VC3: i = (( len (F1 . k)) + n) & ex c be Point of X st c in ( rng (g2 | ( divset ((T2 . k),n)))) & ((F2 . k) . n) = (( vol ( divset ((T2 . k),n))) * c) by INTEGR18:def 1, U1, C20;

            

             V1: n in ( dom (F2 . k)) & n in ( Seg ( len S2)) by C20, U1, X1, FINSEQ_1:def 3, FINSEQ_3: 29;

            

             VC5: ( divset ((T2 . k),n)) = ( divset ((T . k),i)) by C20, V1, A112, U1;

            ( divset ((T2 . k),n)) c= CB by V1, U1, A134;

            then

             V4: ( divset ((T2 . k),n)) c= AB by A17;

            ((f | CB) | ( divset ((T2 . k),n))) = (f | ( divset ((T2 . k),n))) by RELAT_1: 74, V1, U1, A134;

            then (g2 | ( divset ((T2 . k),n))) = (h1 | ( divset ((T . k),i))) by C3, C5, VC5, RELAT_1: 74, V4;

            hence thesis by VC3, V1, B221, FINSEQ_1:def 7, VC5;

          end;

        end;

        hence (Sh1 . k) is middle_volume of h1, (T . k) by B226, INTEGR18:def 1;

      end;

      then

      reconsider F = Sh1 as middle_volume_Sequence of h1, T by INTEGR18:def 3;

      

       A164: for i be Nat holds ( middle_sum (FAB,(F . i))) = (( middle_sum (FAC,(F1 . i))) + ( middle_sum (FCB,(F2 . i))))

      proof

        let i be Nat;

        i is Element of NAT by ORDINAL1:def 12;

        then ex q,q1,q2 be FinSequence of the carrier of X st q = (Sh1 . i) & q1 = (F1 . i) & q2 = (F2 . i) & q = (q1 ^ q2) by B22;

        hence ( middle_sum (FAB,(F . i))) = (( middle_sum (FAC,(F1 . i))) + ( middle_sum (FCB,(F2 . i)))) by RLVECT_1: 41;

      end;

      now

        let i be Nat;

        

        thus (( middle_sum (FAB,F)) . i) = ( middle_sum (FAB,(F . i))) by INTEGR18:def 4

        .= (( middle_sum (FAC,(F1 . i))) + ( middle_sum (FCB,(F2 . i)))) by A164

        .= ((( middle_sum (FAC,F1)) . i) + ( middle_sum (FCB,(F2 . i)))) by INTEGR18:def 4

        .= ((( middle_sum (FAC,F1)) . i) + (( middle_sum (FCB,F2)) . i)) by INTEGR18:def 4;

      end;

      then

       A165: ( middle_sum (FAB,F)) = (( middle_sum (FAC,F1)) + ( middle_sum (FCB,F2))) by NORMSP_1:def 2;

      reconsider XAB = ( chi (AB,AB)) as PartFunc of AB, REAL ;

      reconsider XAC = ( chi (AC,AC)) as PartFunc of AC, REAL ;

      reconsider XCB = ( chi (CB,CB)) as PartFunc of CB, REAL ;

       A168:

      now

        let e be Real;

        assume 0 < e;

        then

        consider m be Nat such that

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

        take m;

        hereby

          let n be Nat;

          assume m <= n;

          then |.((( delta PS2) . (n + 2)) - 0 ).| < e by A169, NAT_1: 12;

          then

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

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

          ex k be Nat, e1 be Division of CB st k = n1 & e1 = (S2 . n1) & e1 = (PS2 . (k + 2)) by A29;

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

        end;

      end;

       A172:

      now

        let e be Real;

        assume

         A173: e > 0 ;

        then

        consider m be Nat such that

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

        take m;

        

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

        let n be Nat;

        

         X1: n in NAT by ORDINAL1:def 12;

        assume m <= n;

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

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

        then

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

        reconsider S2n = (S2 . n) as Division of CB;

        

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

        proof

          reconsider D = (T2 . n) as Division of CB;

          let y be Real;

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

          then

          consider x be object such that

           A179: x in ( dom ( upper_volume (XCB,(T2 . n)))) & y = (( upper_volume (XCB,(T2 . n))) . x) by FUNCT_1:def 3;

          reconsider i = x as Nat by A179;

          

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

          

           X1: n in NAT by ORDINAL1:def 12;

          then

          consider E1 be Division of CB such that

           A182: E1 = (S2 . n) & 2 <= ( len E1) by A30;

          set i1 = (i + 1);

          consider E be Division of CB such that

           A184: E = (S2 . n) and

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

          

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

          then

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

          

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

          then

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

          then

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

          

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

          

           A196: 1 in ( dom E) & 2 in ( dom E) by A184, A182, A186, FINSEQ_3: 25;

          then

           XX2: (E . 2) = ( upper_bound ( divset ((S2 . n),2))) & (E . (2 - 1)) = ( lower_bound ( divset ((S2 . n),2))) & ( lower_bound CB) = ( lower_bound ( divset ((S2 . n),1))) & (E . 1) = ( upper_bound ( divset ((S2 . n),1))) by A184, INTEGRA1:def 4;

          

           XX6: ( vol ( divset ((S2 . n),1))) = (( upper_volume (XCB,(S2 . n))) . 1) & ( vol ( divset ((S2 . n),2))) = (( upper_volume (XCB,(S2 . n))) . 2) by A184, A196, INTEGRA1: 20;

          

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

          then 1 <= ( len ( upper_volume (XCB,(S2 . n)))) by NAT_1: 11;

          then 1 in ( dom ( upper_volume (XCB,(S2 . n)))) & 2 in ( dom ( upper_volume (XCB,(S2 . n)))) by XX1, A184, A182, FINSEQ_3: 25;

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

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

          then

           A191: ( vol ( divset ((S2 . n),1))) < (e / 2) & ( vol ( divset ((S2 . n),2))) < (e / 2) by XX6, A177, XXREAL_0: 2;

          

           XX4: ( divset ((S2 . n),2)) = [.( lower_bound ( divset ((S2 . n),2))), ( upper_bound ( divset ((S2 . n),2))).] & ( divset ((T2 . n),i)) = [.( lower_bound ( divset ((T2 . n),i))), ( upper_bound ( divset ((T2 . n),i))).] & ( divset ((S2 . n),i1)) = [.( lower_bound ( divset ((S2 . n),i1))), ( upper_bound ( divset ((S2 . n),i1))).] by INTEGRA1: 4;

          

           XX5: (D . i) = (E . (i + 1)) by A184, A185, A182, A186, A207, RFINSEQ:def 1;

          

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

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

          then

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

           A190:

          now

            assume

             A192: i = 1;

            then

             XX3: ( lower_bound CB) = ( lower_bound ( divset ((T2 . n),1))) & (D . 1) = ( upper_bound ( divset ((T2 . n),1))) by A207, INTEGRA1:def 4;

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

            then y = (( vol ( divset ((S2 . n),2))) + ( vol ( divset ((S2 . n),1)))) by A192, XX3, XX5, XX2;

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

            hence thesis;

          end;

          now

            assume

             A210: i <> 1;

            then

             XX7: (D . (i - 1)) = ( lower_bound ( divset ((T2 . n),i))) & (D . i) = ( upper_bound ( divset ((T2 . n),i))) by A207, INTEGRA1:def 4;

            

             B211: 1 <= i by A179, FINSEQ_3: 25;

            then

            reconsider i9 = (i - 1) as Nat;

            

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

            then i9 in ( Seg ( len D)) by A181, A188, FINSEQ_3: 12;

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

            then

             XX9: (D . (i - 1)) = (E . (i9 + 1)) by A184, A185, A182, A186, RFINSEQ:def 1;

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

            then i1 <> 1;

            then (E . (i1 - 1)) = ( lower_bound ( divset ((S2 . n),i1))) & (E . i1) = ( upper_bound ( divset ((S2 . n),i1))) by A184, A205, A209, INTEGRA1:def 4;

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

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

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

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

            hence thesis by A175, XXREAL_0: 2;

          end;

          hence thesis by A190;

        end;

        

         X1: n in NAT by ORDINAL1:def 12;

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

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

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

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

      end;

      then

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

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

      then

       A217: ( middle_sum (FCB,F2)) is convergent & ( lim ( middle_sum (FCB,F2))) = ( integral FCB) by A215, C5, INTEGR18:def 6;

       A218:

      now

        let e be Real;

        assume

         A219: 0 < e;

        then

        consider n1 be Nat such that

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

        consider n2 be Nat such that

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

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

        take n;

        let m be Nat;

        assume

         A222: n <= m;

        

         X1: m in NAT by ORDINAL1:def 12;

        n1 <= n & n2 <= n by XXREAL_0: 25;

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

        then |.((( delta T1) . m) - 0 ).| < e & |.((( delta T2) . m) - 0 ).| < e by A220, A221;

        then |.( delta (T1 . m)).| < e & |.( delta (T2 . m)).| < e by X1, INTEGRA3:def 2;

        then

         A224: ( max ( rng ( upper_volume (XCB,(T2 . m))))) < e & ( max ( rng ( upper_volume (XAC,(T1 . m))))) < e by ABSVALUE:def 1, INTEGRA3: 9;

        

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

        proof

          reconsider Tm = (T . m) as Division of AB;

          let y be Real;

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

          then

          consider x be object such that

           A228: x in ( dom ( upper_volume (XAB,(T . m)))) & y = (( upper_volume (XAB,(T . m))) . x) by FUNCT_1:def 3;

          reconsider i = x as Nat by A228;

          

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

          then

           A231: 1 <= i by FINSEQ_1: 1;

          

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

          then

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

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

          then

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

          consider S1 be Division of AC, S2 be Division of CB such that

           A235: S1 = (T1 . m) & S2 = (T2 . m) and

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

          

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

          per cases ;

            suppose i <= ( len S1);

            then

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

            then

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

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

            then

             A241: ( dom ( upper_volume (XAC,(T1 . m)))) = ( dom S1) by FINSEQ_3: 29;

            

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

            

             A243: ( divset ((T1 . m),i)) c= AC by X1, A139, A235, A239;

            then ( divset ((T1 . m),i)) c= AB by A17;

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

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

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

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

            hence thesis by A224, XXREAL_0: 2;

          end;

            suppose i > ( len S1);

            then

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

            then

            consider k be Nat such that

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

            set i1 = (1 + k);

            

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

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

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

            then

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

            then

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

            

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

            

             A250: ( divset ((T2 . m),i1)) c= CB by X1, A134, A235, A247;

            then ( divset ((T2 . m),i1)) c= AB by A17;

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

            then

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

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

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

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

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

            hence thesis by A224, XXREAL_0: 2;

          end;

        end;

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

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

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

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

      end;

      then

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

      then

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

      

       A282: ( middle_sum (FAC,F1)) is convergent & ( lim ( middle_sum (FAC,F1))) = ( integral FAC) by A53, C4, INTEGR18:def 6;

      ( integral (f,a,b)) = ( integral (f,AB)) by A7, INTEGR18: 16

      .= ( integral FAB) by A2, C3, INTEGR18: 9

      .= ( lim ( middle_sum (FAB,F))) by B255, A253, C3, INTEGR18:def 6;

      hence ( integral (f,a,b)) = (( integral (f,a,c)) + ( integral (f,c,b))) by A57, A165, A282, A217, NORMSP_1: 25;

    end;

    theorem :: INTEGR21:15

    

     Th1908: for f be continuous PartFunc of REAL , the carrier of Y st a <= b & ['a, b'] c= ( dom f) & c in ['a, b'] holds f is_integrable_on ['a, c'] & f is_integrable_on ['c, b'] & ( integral (f,a,b)) = (( integral (f,a,c)) + ( integral (f,c,b)))

    proof

      let f be continuous PartFunc of REAL , the carrier of Y;

      assume

       A1: a <= b & ['a, b'] c= ( dom f) & c in ['a, b'];

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

      then

       A3: a <= c & c <= b by A1, XXREAL_1: 1;

      hence f is_integrable_on ['a, c'] & f is_integrable_on ['c, b'] by A1, Th1909;

       ['c, b'] c= ['a, b'] by A3, INTEGR19: 1;

      then

       A5: ['c, b'] c= ( dom f) by A1;

      per cases ;

        suppose

         A6: b = c;

        then

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

        then

         A91: ( integral (f,c,b)) = ( integral (f, ['c, b'])) by INTEGR18: 16;

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

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

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

        then ( integral (f,c,b)) = ( 0. Y) by A5, A91, INTEGR18: 17;

        hence thesis by A6;

      end;

        suppose b <> c;

        hence thesis by A1, Lm62;

      end;

    end;

    theorem :: INTEGR21:16

    for f,g be continuous PartFunc of REAL , the carrier of Y st a <= c & c <= d & d <= b & ['a, b'] c= ( dom f) & ['a, b'] c= ( dom g) holds (f + g) is_integrable_on ['c, d'] & ((f + g) | ['c, d']) is bounded

    proof

      let f,g be continuous PartFunc of REAL , the carrier of Y;

      assume

       A1: a <= c & c <= d & d <= b & ['a, b'] c= ( dom f) & ['a, b'] c= ( dom g);

      reconsider A = ['c, d'] as non empty closed_interval Subset of REAL ;

      

       A2: f is_integrable_on A & g is_integrable_on A by A1, Th1909;

      A c= ( dom f) & A c= ( dom g) by A1, INTEGR19: 2;

      hence (f + g) is_integrable_on ['c, d'] by A2, INTEGR18: 14;

      a <= d by A1, XXREAL_0: 2;

      then (f | ['a, b']) is bounded & (g | ['a, b']) is bounded by A1, Th1, XXREAL_0: 2;

      then

       A3: (f | ['c, d']) is bounded & (g | ['c, d']) is bounded by A1, Th1915b;

      ( ['c, d'] /\ ['c, d']) = ['c, d'];

      hence ((f + g) | ['c, d']) is bounded by A3, Th1935;

    end;

    theorem :: INTEGR21:17

    

     Th1911: for f be continuous PartFunc of REAL , the carrier of Y st a <= c & c <= d & d <= b & ['a, b'] c= ( dom f) holds (r (#) f) is_integrable_on ['c, d'] & ((r (#) f) | ['c, d']) is bounded

    proof

      let f be continuous PartFunc of REAL , the carrier of Y;

      assume

       A1: a <= c & c <= d & d <= b & ['a, b'] c= ( dom f);

      reconsider A = ['c, d'] as non empty closed_interval Subset of REAL ;

      

       A2: f is_integrable_on A by A1, Th1909;

      A c= ( dom f) by A1, INTEGR19: 2;

      hence (r (#) f) is_integrable_on ['c, d'] by A2, INTEGR18: 13;

      a <= d by A1, XXREAL_0: 2;

      then (f | ['a, b']) is bounded by A1, Th1, XXREAL_0: 2;

      then (f | ['c, d']) is bounded by A1, Th1915b;

      hence ((r (#) f) | ['c, d']) is bounded by Th1935a;

    end;

    theorem :: INTEGR21:18

    for f be continuous PartFunc of REAL , the carrier of Y st a <= c & c <= d & d <= b & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) holds ( - f) is_integrable_on ['c, d'] & (( - f) | ['c, d']) is bounded

    proof

      let f be continuous PartFunc of REAL , the carrier of Y;

      assume

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

      ( - f) = (( - 1) (#) f) by VFUNCT_1: 23;

      hence ( - f) is_integrable_on ['c, d'] by A1, Th1911;

      (f | ['c, d']) is bounded by A1, Th1915b;

      hence (( - f) | ['c, d']) is bounded by Th1935b;

    end;

    theorem :: INTEGR21:19

    for f,g be continuous PartFunc of REAL , the carrier of Y st a <= c & c <= d & d <= b & ['a, b'] c= ( dom f) & ['a, b'] c= ( dom g) holds (f - g) is_integrable_on ['c, d'] & ((f - g) | ['c, d']) is bounded

    proof

      let f,g be continuous PartFunc of REAL , the carrier of Y;

      assume

       A1: a <= c & c <= d & d <= b & ['a, b'] c= ( dom f) & ['a, b'] c= ( dom g);

      then a <= d by XXREAL_0: 2;

      then

       A1X: f is_integrable_on ['a, b'] & g is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & (g | ['a, b']) is bounded by A1, Th1, INTEGR20: 19, XXREAL_0: 2;

      reconsider A = ['c, d'] as non empty closed_interval Subset of REAL ;

      

       A2: f is_integrable_on A & g is_integrable_on A by A1, Th1909;

      A c= ( dom f) & A c= ( dom g) by A1, INTEGR19: 2;

      hence (f - g) is_integrable_on ['c, d'] by A2, INTEGR18: 15;

      

       A3: (f | ['c, d']) is bounded & (g | ['c, d']) is bounded by A1, A1X, Th1915b;

      ( ['c, d'] /\ ['c, d']) = ['c, d'];

      hence ((f - g) | ['c, d']) is bounded by A3, Th1935;

    end;

    

     Lm8: for h be Function of A, the carrier of Y, f be Function of A, REAL st h is bounded & h is integrable & f = ||.h.|| & f is integrable holds ||.( integral h).|| <= ( integral f)

    proof

      let h be Function of A, the carrier of Y, f be Function of A, REAL ;

      assume

       A1: h is bounded & h is integrable & f = ||.h.|| & f is integrable;

      then

       A2: f is bounded by Th1914;

      consider T be DivSequence of A such that

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

      set S = the middle_volume_Sequence of h, T;

      

       A4: ( dom f) = ( dom h) by A1, NORMSP_0:def 3;

      defpred P[ Element of NAT , set] means ex p be FinSequence of REAL st p = $2 & ( len p) = ( len (T . $1)) & for i be Nat st i in ( dom (T . $1)) holds (p . i) in ( dom (h | ( divset ((T . $1),i)))) & ex z be Point of Y st z = ((h | ( divset ((T . $1),i))) . (p . i)) & ((S . $1) . i) = (( vol ( divset ((T . $1),i))) * z);

      

       A5: for k be Element of NAT holds ex p be Element of ( REAL * ) st P[k, p]

      proof

        let k be Element of NAT ;

        defpred P1[ Nat, set] means $2 in ( dom (h | ( divset ((T . k),$1)))) & ex c be Point of Y st c = ((h | ( divset ((T . k),$1))) . $2) & ((S . k) . $1) = (( vol ( divset ((T . k),$1))) * c);

        

         A6: ( Seg ( len (T . k))) = ( dom (T . k)) by FINSEQ_1:def 3;

        

         A7: for i be Nat st i in ( Seg ( len (T . k))) holds ex x be Element of REAL st P1[i, x]

        proof

          let i be Nat;

          assume i in ( Seg ( len (T . k)));

          then i in ( dom (T . k)) by FINSEQ_1:def 3;

          then

          consider c be Point of Y such that

           A8: c in ( rng (h | ( divset ((T . k),i)))) & ((S . k) . i) = (( vol ( divset ((T . k),i))) * c) by INTEGR18:def 1;

          consider x be object such that

           A9: x in ( dom (h | ( divset ((T . k),i)))) & c = ((h | ( divset ((T . k),i))) . x) by A8, FUNCT_1:def 3;

          x in ( dom h) & x in ( divset ((T . k),i)) by A9, RELAT_1: 57;

          then

          reconsider x as Element of REAL ;

          take x;

          thus thesis by A8, A9;

        end;

        consider p be FinSequence of REAL such that

         A10: ( dom p) = ( Seg ( len (T . k))) & for i be Nat st i in ( Seg ( len (T . k))) holds P1[i, (p . i)] from FINSEQ_1:sch 5( A7);

        take p;

        ( len p) = ( len (T . k)) by A10, FINSEQ_1:def 3;

        hence thesis by A10, A6, FINSEQ_1:def 11;

      end;

      consider F be sequence of ( REAL * ) such that

       A11: for x be Element of NAT holds P[x, (F . x)] from FUNCT_2:sch 3( A5);

      defpred P1[ Element of NAT , set] means ex q be middle_volume of f, (T . $1) st q = $2 & for i be Nat st i in ( dom (T . $1)) holds ex z be Element of REAL st ((F . $1) . i) in ( dom (f | ( divset ((T . $1),i)))) & z = ((f | ( divset ((T . $1),i))) . ((F . $1) . i)) & (q . i) = (( vol ( divset ((T . $1),i))) * z);

      

       A12: for k be Element of NAT holds ex y be Element of ( REAL * ) st P1[k, y]

      proof

        let k be Element of NAT ;

        defpred P11[ Nat, set] means ex c be Element of REAL st ((F . k) . $1) in ( dom (f | ( divset ((T . k),$1)))) & c = ((f | ( divset ((T . k),$1))) . ((F . k) . $1)) & $2 = (( vol ( divset ((T . k),$1))) * c);

        

         A13: ( Seg ( len (T . k))) = ( dom (T . k)) by FINSEQ_1:def 3;

        

         A14: for i be Nat st i in ( Seg ( len (T . k))) holds ex x be Element of REAL st P11[i, x]

        proof

          let i be Nat;

          assume i in ( Seg ( len (T . k)));

          then

           A15: i in ( dom (T . k)) by FINSEQ_1:def 3;

          consider p be FinSequence of REAL such that

           A16: p = (F . k) & ( len p) = ( len (T . k)) & for i be Nat st i in ( dom (T . k)) holds (p . i) in ( dom (h | ( divset ((T . k),i)))) & ex z be Point of Y st z = ((h | ( divset ((T . k),i))) . (p . i)) & ((S . k) . i) = (( vol ( divset ((T . k),i))) * z) by A11;

          (p . i) in ( dom (h | ( divset ((T . k),i)))) by A15, A16;

          then

           A171: (p . i) in ( dom h) & (p . i) in ( divset ((T . k),i)) by RELAT_1: 57;

          (( vol ( divset ((T . k),i))) * ((f | ( divset ((T . k),i))) . (p . i))) in REAL & ((f | ( divset ((T . k),i))) . (p . i)) in REAL by XREAL_0:def 1;

          hence thesis by A16, A171, A4, RELAT_1: 57;

        end;

        consider q be FinSequence of REAL such that

         A18: ( dom q) = ( Seg ( len (T . k))) & for i be Nat st i in ( Seg ( len (T . k))) holds P11[i, (q . i)] from FINSEQ_1:sch 5( A14);

        

         A19: ( len q) = ( len (T . k)) by A18, FINSEQ_1:def 3;

        now

          let i be Nat;

          assume i in ( dom (T . k));

          then i in ( Seg ( len (T . k))) by FINSEQ_1:def 3;

          then ex c be Element of REAL st ((F . k) . i) in ( dom (f | ( divset ((T . k),i)))) & c = ((f | ( divset ((T . k),i))) . ((F . k) . i)) & (q . i) = (( vol ( divset ((T . k),i))) * c) by A18;

          hence ex c be Element of REAL st c in ( rng (f | ( divset ((T . k),i)))) & (q . i) = (c * ( vol ( divset ((T . k),i)))) by FUNCT_1: 3;

        end;

        then

        reconsider q as middle_volume of f, (T . k) by A19, INTEGR15:def 1;

        q is Element of ( REAL * ) by FINSEQ_1:def 11;

        hence thesis by A13, A18;

      end;

      consider Sf be sequence of ( REAL * ) such that

       A21: for x be Element of NAT holds P1[x, (Sf . x)] from FUNCT_2:sch 3( A12);

      now

        let k be Element of NAT ;

        ex q be middle_volume of f, (T . k) st q = (Sf . k) & for i be Nat st i in ( dom (T . k)) holds ex z be Element of REAL st ((F . k) . i) in ( dom (f | ( divset ((T . k),i)))) & z = ((f | ( divset ((T . k),i))) . ((F . k) . i)) & (q . i) = (( vol ( divset ((T . k),i))) * z) by A21;

        hence (Sf . k) is middle_volume of f, (T . k);

      end;

      then

      reconsider Sf as middle_volume_Sequence of f, T by INTEGR15:def 3;

      

       A22: ( middle_sum (f,Sf)) is convergent & ( lim ( middle_sum (f,Sf))) = ( integral f) by A1, A2, A3, INTEGR15: 9;

      

       A23: ( middle_sum (h,S)) is convergent & ( lim ( middle_sum (h,S))) = ( integral h) by A1, A3, INTEGR18:def 6;

      

       A24: for k be Element of NAT holds ||.(( middle_sum (h,S)) . k).|| <= (( middle_sum (f,Sf)) . k)

      proof

        let k be Element of NAT ;

        

         A25: (( middle_sum (f,Sf)) . k) = ( middle_sum (f,(Sf . k))) by INTEGR15:def 4;

        

         A28: ex p be FinSequence of REAL st p = (F . k) & ( len p) = ( len (T . k)) & for i be Nat st i in ( dom (T . k)) holds (p . i) in ( dom (h | ( divset ((T . k),i)))) & ex z be Point of Y st z = ((h | ( divset ((T . k),i))) . (p . i)) & ((S . k) . i) = (( vol ( divset ((T . k),i))) * z) by A11;

        

         A29: ex q be middle_volume of f, (T . k) st q = (Sf . k) & for i be Nat st i in ( dom (T . k)) holds ex z be Element of REAL st ((F . k) . i) in ( dom (f | ( divset ((T . k),i)))) & z = ((f | ( divset ((T . k),i))) . ((F . k) . i)) & (q . i) = (( vol ( divset ((T . k),i))) * z) by A21;

        

         A30: ( len (Sf . k)) = ( len (T . k)) by INTEGR15:def 1;

        

         A31: ( len (S . k)) = ( len (T . k)) by INTEGR18:def 1;

        now

          let i be Nat;

          assume

           A32: i in ( dom (S . k));

          then i in ( Seg ( len (T . k))) by A31, FINSEQ_1:def 3;

          then

           A34: i in ( dom (T . k)) by FINSEQ_1:def 3;

          then

           A36: ((F . k) . i) in ( dom (h | ( divset ((T . k),i)))) by A28;

          consider z be Point of Y such that

           A37: z = ((h | ( divset ((T . k),i))) . ((F . k) . i)) & ((S . k) . i) = (( vol ( divset ((T . k),i))) * z) by A28, A34;

          

           A38: ex w be Element of REAL st ((F . k) . i) in ( dom (f | ( divset ((T . k),i)))) & w = ((f | ( divset ((T . k),i))) . ((F . k) . i)) & ((Sf . k) . i) = (( vol ( divset ((T . k),i))) * w) by A29, A34;

          ((S . k) . i) = ((S . k) /. i) by A32, PARTFUN1:def 6;

          

          then

           A41: ||.((S . k) /. i).|| = ( |.( vol ( divset ((T . k),i))).| * ||.z.||) by A37, NORMSP_1:def 1

          .= (( vol ( divset ((T . k),i))) * ||.z.||) by INTEGRA1: 9, ABSVALUE:def 1;

          

           A42: ( dom (h | ( divset ((T . k),i)))) c= ( dom h) & ( dom (f | ( divset ((T . k),i)))) c= ( dom f) by RELAT_1: 60;

          

           A43: ((h | ( divset ((T . k),i))) . ((F . k) . i)) = (h . ((F . k) . i)) by A36, FUNCT_1: 47;

          ((f | ( divset ((T . k),i))) . ((F . k) . i)) = (f . ((F . k) . i)) by A38, FUNCT_1: 47

          .= ||.(h /. ((F . k) . i)).|| by A42, A1, A38, NORMSP_0:def 2;

          hence ||.((S . k) /. i).|| <= ((Sf . k) . i) by A41, A43, A38, A37, A42, A36, PARTFUN1:def 6;

        end;

        then ||.( middle_sum (h,(S . k))).|| <= ( Sum (Sf . k)) by A30, A31, INTEGR20: 10;

        hence thesis by A25, INTEGR18:def 4;

      end;

       A45:

      now

        let i be Nat;

        

         XX: i in NAT by ORDINAL1:def 12;

        ( ||.( middle_sum (h,S)).|| . i) = ||.(( middle_sum (h,S)) . i).|| by NORMSP_0:def 4;

        hence ( ||.( middle_sum (h,S)).|| . i) <= (( middle_sum (f,Sf)) . i) by A24, XX;

      end;

       ||.( middle_sum (h,S)).|| is convergent by A1, A3, NORMSP_1: 23;

      then ( lim ||.( middle_sum (h,S)).||) <= ( lim ( middle_sum (f,Sf))) by A45, A22, SEQ_2: 18;

      hence thesis by A22, A23, LOPBAN_1: 41;

    end;

    theorem :: INTEGR21:20

    

     Th1920: for f be PartFunc of REAL , the carrier of Y st A c= ( dom f) & (f | A) is bounded & f is_integrable_on A & ||.f.|| is_integrable_on A holds ||.( integral (f,A)).|| <= ( integral ( ||.f.||,A))

    proof

      let f be PartFunc of REAL , the carrier of Y;

      assume

       A1: A c= ( dom f) & (f | A) is bounded & f is_integrable_on A & ||.f.|| is_integrable_on A;

      set g = ||.f.||;

      reconsider fA = (f | A) as Function of A, the carrier of Y by A1;

      

       A2: ( integral (f,A)) = ( integral fA) by A1, INTEGR18: 9;

      A c= ( dom g) by A1, NORMSP_0:def 2;

      then

      reconsider gA = (g | A) as Function of A, REAL by Lm3;

      

       A3: gA is integrable by A1;

      fA is bounded & ||.fA.|| = (g | A) by Th1918, A1;

      hence thesis by A2, A3, A1, Lm8;

    end;

    theorem :: INTEGR21:21

    

     Th1921: for f be PartFunc of REAL , the carrier of Y st a <= b & ['a, b'] c= ( dom f) & f is_integrable_on ['a, b'] & ||.f.|| is_integrable_on ['a, b'] & (f | ['a, b']) is bounded holds ||.( integral (f,a,b)).|| <= ( integral ( ||.f.||,a,b))

    proof

      let f be PartFunc of REAL , the carrier of Y;

      assume

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

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

      then

       A3: ( integral (f,a,b)) = ( integral (f, ['a, b'])) by INTEGR18: 16;

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

      hence thesis by Th1920, A1, A3;

    end;

    

     Lm10: for f be continuous PartFunc of REAL , the carrier of Y st a <= b & c <= d & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'] holds f is_integrable_on ['c, d'] & ||.f.|| is_integrable_on ['c, d'] & ( ||.f.|| | ['c, d']) is bounded & ||.( integral (f,c,d)).|| <= ( integral ( ||.f.||,c,d))

    proof

      let f be continuous PartFunc of REAL , the carrier of Y;

      assume that

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

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

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

      

       A3: f is_integrable_on ['a, b'] & ||.f.|| is_integrable_on ['a, b'] & (f | ['a, b']) is bounded by Th1, INTEGR20: 19, Th4, A1, A2;

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

      then

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

      then

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

      

       A7: ['c, d'] c= ( dom f) & f is_integrable_on ['c, d'] by A1, A2, A5, Th1909, INTEGR19: 2;

      

       A8: ['a, b'] c= ( dom ||.f.||) by A2, NORMSP_0:def 2;

      ( ||.f.|| | ['a, b']) is bounded by Th3, A1, A2;

      then ['c, d'] c= ( dom ||.f.||) & ||.f.|| is_integrable_on ['c, d'] by A1, A3, A5, A8, INTEGRA6: 18;

      hence thesis by A1, A7, Th1921, A6, Th1919;

    end;

    theorem :: INTEGR21:22

    

     Th1922: for f be continuous PartFunc of REAL , the carrier of Y st a <= b & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'] holds ||.f.|| is_integrable_on ['( min (c,d)), ( max (c,d))'] & ( ||.f.|| | ['( min (c,d)), ( max (c,d))']) is bounded & ||.( integral (f,c,d)).|| <= ( integral ( ||.f.||,( min (c,d)),( max (c,d))))

    proof

      let f be continuous PartFunc of REAL , the carrier of Y;

      assume

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

      per cases ;

        suppose

         A3: not c <= d;

        then

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

        then ['d, c'] c= ( dom f) by A1, INTEGR19: 3;

        then ( integral (f,c,d)) = ( - ( integral (f,d,c))) by A3, Th1947;

        then ||.( integral (f,c,d)).|| = ||.( integral (f,d,c)).|| by NORMSP_1: 2;

        hence thesis by A1, A3, A5, Lm10;

      end;

        suppose

         A6: c <= d;

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

        hence thesis by A1, A6, Lm10;

      end;

    end;

    

     Th1925a: for f be continuous PartFunc of REAL , the carrier of Y st a <= b & c <= d & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'] holds ( integral ((r (#) f),c,d)) = (r * ( integral (f,c,d)))

    proof

      let f be continuous PartFunc of REAL , the carrier of Y;

      assume

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

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

      then

       A2: a <= c & c <= b & a <= d & d <= b by A1, XXREAL_1: 1;

      reconsider A = ['c, d'] as non empty closed_interval Subset of REAL ;

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

      then ['c, d'] c= ['a, b'] by A1, Lm2;

      then

       A4: f is_integrable_on A & A c= ( dom f) by A1, A2, Th1909;

      ( integral ((r (#) f),A)) = ( integral ((r (#) f),c,d)) & ( integral (f,A)) = ( integral (f,c,d)) by A1, INTEGR18:def 9;

      hence ( integral ((r (#) f),c,d)) = (r * ( integral (f,c,d))) by A4, INTEGR18: 13;

    end;

    theorem :: INTEGR21:23

    

     Th1925: for f be continuous PartFunc of REAL , the carrier of Y st a <= b & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'] holds ( integral ((r (#) f),c,d)) = (r * ( integral (f,c,d)))

    proof

      let f be continuous PartFunc of REAL , the carrier of Y;

      assume

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

      per cases ;

        suppose

         A2: not c <= d;

        reconsider A = ['d, c'] as non empty closed_interval Subset of REAL ;

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

        then ['d, c'] c= ['a, b'] by A1, Lm2;

        then

         A7: A c= ( dom f) by A1;

        then A c= ( dom (r (#) f)) by VFUNCT_1:def 4;

        then

         A8: ( - ( integral ((r (#) f),d,c))) = ( integral ((r (#) f),c,d)) & ( - ( integral (f,d,c))) = ( integral (f,c,d)) by A2, A7, Th1947;

        ( integral ((r (#) f),d,c)) = (r * ( integral (f,d,c))) by A1, A2, Th1925a;

        hence ( integral ((r (#) f),c,d)) = (r * ( integral (f,c,d))) by A8, RLVECT_1: 25;

      end;

        suppose c <= d;

        hence thesis by A1, Th1925a;

      end;

    end;

    theorem :: INTEGR21:24

    for f be continuous PartFunc of REAL , the carrier of Y st a <= b & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'] holds ( integral (( - f),c,d)) = ( - ( integral (f,c,d)))

    proof

      let f be continuous PartFunc of REAL , the carrier of Y;

      assume

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

      

       A2: ( - f) = (( - 1) (#) f) by VFUNCT_1: 23;

      (( - 1) * ( integral (f,c,d))) = ( - ( integral (f,c,d))) by RLVECT_1: 16;

      hence thesis by A1, A2, Th1925;

    end;

    theorem :: INTEGR21:25

    for f be continuous PartFunc of REAL , the carrier of Y st (a <= b & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'] & for x be Real st x in ['( min (c,d)), ( max (c,d))'] holds ||.(f /. x).|| <= e) holds ||.( integral (f,c,d)).|| <= (e * |.(d - c).|)

    proof

      let f be continuous PartFunc of REAL , the carrier of Y;

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

      assume that

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

       A2: for x be Real st x in A holds ||.(f /. x).|| <= e;

      ( rng ||.f.||) c= REAL ;

      then

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

      

       B1: A c= ['a, b'] by A1, Lm2;

      

       B2: ( dom ||.f.||) = ( dom f) by NORMSP_0:def 2;

      then A c= ( dom ||.f.||) by A1, B1;

      then

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

      

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

      

       A5: ||.f.|| is_integrable_on A & (g | A) is bounded & ||.( integral (f,c,d)).|| <= ( integral ( ||.f.||,( min (c,d)),( max (c,d)))) by A1, Th1922;

      consider h be Function of A, REAL such that

       A6: ( rng h) = {e} and

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

       A8:

      now

        let x be Real;

        assume

         A9: x in A;

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

        then

         A10: (g . x) = ||.(f /. x).|| by A9, B2, A1, B1, NORMSP_0:def 2;

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

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

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

      end;

      ( min (c,d)) <= c & c <= ( max (c,d)) by XXREAL_0: 17, XXREAL_0: 25;

      then

       A12: ( integral ( ||.f.||,( min (c,d)),( max (c,d)))) = ( integral ( ||.f.||,A)) by INTEGRA5:def 4, XXREAL_0: 2;

      h is integrable & ( integral h) = (e * ( vol A)) by A6, INTEGRA4: 4;

      then ( integral ( ||.f.||,( min (c,d)),( max (c,d)))) <= (e * |.(d - c).|) by A12, A7, A8, A5, A4, INTEGRA2: 34;

      hence thesis by A5, XXREAL_0: 2;

    end;

    

     Th1928: for f,g be continuous PartFunc of REAL , the carrier of Y st a <= b & c <= d & ['a, b'] c= ( dom f) & ['a, b'] c= ( dom g) & c in ['a, b'] & d in ['a, b'] holds ( integral ((f - g),c,d)) = (( integral (f,c,d)) - ( integral (g,c,d)))

    proof

      let f,g be continuous PartFunc of REAL , the carrier of Y;

      assume

       A1: a <= b & c <= d & ['a, b'] c= ( dom f) & ['a, b'] c= ( dom g) & c in ['a, b'] & d in ['a, b'];

      reconsider A = ['c, d'] as non empty closed_interval Subset of REAL ;

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

      then a <= c & c <= b & a <= d & d <= b by A1, XXREAL_1: 1;

      then

       A4: f is_integrable_on A & g is_integrable_on A by A1, Th1909;

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

      then ['c, d'] c= ['a, b'] by A1, Lm2;

      then

       A5: A c= ( dom f) & A c= ( dom g) by A1;

      ( integral ((f - g),A)) = ( integral ((f - g),c,d)) & ( integral (f,A)) = ( integral (f,c,d)) & ( integral (g,A)) = ( integral (g,c,d)) by A1, INTEGR18:def 9;

      hence thesis by A5, A4, INTEGR18: 15;

    end;

    theorem :: INTEGR21:26

    

     Th404: for Y be RealNormSpace, A be non empty closed_interval Subset of REAL , f be Function of A, the carrier of Y, E be Point of Y st ( rng f) = {E} holds f is integrable & ( integral f) = (( vol A) * E)

    proof

      let Y be RealNormSpace;

      let A be non empty closed_interval Subset of REAL ;

      let f be Function of A, the carrier of Y;

      let E be Point of Y;

      assume

       AS1: ( rng f) = {E};

      reconsider I = (( vol A) * E) as Point of Y;

      

       P1: for T be DivSequence of A, S be middle_volume_Sequence of f, T st ( delta T) is convergent & ( lim ( delta T)) = 0 holds ( middle_sum (f,S)) is convergent & ( lim ( middle_sum (f,S))) = I

      proof

        let T be DivSequence of A, S be middle_volume_Sequence of f, T;

        assume ( delta T) is convergent & ( lim ( delta T)) = 0 ;

        set s = ( middle_sum (f,S));

        

         A1: for k be Nat holds (s . k) = I

        proof

          let k be Nat;

          defpred P11[ Nat, set] means $2 = ( vol ( divset ((T . k),$1)));

          

           A14: for i be Nat st i in ( Seg ( len (T . k))) holds ex x be Element of REAL st P11[i, x]

          proof

            let i be Nat;

            assume i in ( Seg ( len (T . k)));

            ( vol ( divset ((T . k),i))) in REAL by XREAL_0:def 1;

            hence thesis;

          end;

          consider q be FinSequence of REAL such that

           A18: ( dom q) = ( Seg ( len (T . k))) & for i be Nat st i in ( Seg ( len (T . k))) holds P11[i, (q . i)] from FINSEQ_1:sch 5( A14);

          

           B7: ( Sum q) = ( vol A) by INTEGR20: 6, A18;

          ( len q) = ( len (T . k)) by A18, FINSEQ_1:def 3;

          then

           B8: ( len (S . k)) = ( len q) by INTEGR18:def 1;

          

           B40: for i be Nat st i in ( dom (S . k)) holds ex r be Real st r = (q . i) & ((S . k) . i) = (r * E)

          proof

            let i be Nat;

            assume i in ( dom (S . k));

            then i in ( Seg ( len (S . k))) by FINSEQ_1:def 3;

            then

             B44: i in ( Seg ( len (T . k))) by INTEGR18:def 1;

            then i in ( dom (T . k)) by FINSEQ_1:def 3;

            then

            consider c be Point of Y such that

             B42: c in ( rng (f | ( divset ((T . k),i)))) & ((S . k) . i) = (( vol ( divset ((T . k),i))) * c) by INTEGR18:def 1;

            c in ( rng f) by B42, TARSKI:def 3, RELAT_1: 70;

            then

             B43: c = E by AS1, TARSKI:def 1;

            (q . i) = ( vol ( divset ((T . k),i))) by A18, B44;

            hence thesis by B42, B43;

          end;

          (s . k) = ( middle_sum (f,(S . k))) by INTEGR18:def 4;

          hence thesis by B40, B7, B8, INTEGR20: 7;

        end;

         A2:

        now

          let p be Real;

          assume

           A3: 0 < p;

          reconsider k = 0 as Nat;

          take k;

          let n be Nat such that k <= n;

          thus ||.((s . n) - I).|| < p by A3, NORMSP_1: 6, A1;

        end;

        hence s is convergent;

        hence thesis by A2, NORMSP_1:def 7;

      end;

      hence f is integrable;

      hence ( integral f) = (( vol A) * E) by P1, INTEGR18:def 6;

    end;

    theorem :: INTEGR21:27

    

     Th1929: for f be PartFunc of REAL , the carrier of Y, E be Point of Y st (a <= b & ['a, b'] c= ( dom f) & for x be Real st x in ['a, b'] holds (f /. x) = E) holds f is_integrable_on ['a, b'] & ( integral (f,a,b)) = ((b - a) * E)

    proof

      let f be PartFunc of REAL , the carrier of Y, E be Point of Y;

      assume that

       A1: a <= b and

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

       A3: for x be Real st x in ['a, b'] holds (f /. x) = E;

      reconsider A = ['a, b'] as non empty closed_interval Subset of REAL ;

      f is Function of ( dom f), ( rng f) by FUNCT_2: 1;

      then f is Function of ( dom f), the carrier of Y by FUNCT_2: 2;

      then

      reconsider g = (f | A) as Function of A, the carrier of Y by A2, FUNCT_2: 32;

      

       A7: {E} c= ( rng g)

      proof

        let x be object;

        assume x in {E};

        then

         A5: x = E by TARSKI:def 1;

        consider a be Element of A such that

         A6: a in ( dom g) by SUBSET_1: 4;

        (f /. a) = E by A3;

        then (f . a) = E by A2, PARTFUN1:def 6;

        then (g . a) = E by FUNCT_1: 49;

        hence thesis by A5, A6, FUNCT_1: 3;

      end;

      ( rng g) c= {E}

      proof

        let x be object;

        assume x in ( rng g);

        then

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

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

        (f . a) = x by A9, FUNCT_1: 49;

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

        then x = E by A3;

        hence x in {E} by TARSKI:def 1;

      end;

      then

       A10: ( rng g) = {E} by A7, XBOOLE_0:def 10;

      hence f is_integrable_on ['a, b'] by Th404;

      ( integral g) = (( vol A) * E) by A10, Th404;

      then ( integral (f,A)) = (( vol A) * E) by A2, INTEGR18:def 8;

      then ( integral (f,A)) = ((b - a) * E) by A1, INTEGRA6: 5;

      hence ( integral (f,a,b)) = ((b - a) * E) by A1, INTEGR18:def 9;

    end;

    theorem :: INTEGR21:28

    for f be PartFunc of REAL , the carrier of Y st a <= b & c in ['a, b'] & d in ['a, b'] & ['a, b'] c= ( dom f) & for x be Real st x in ['a, b'] holds (f /. x) = E holds ( integral (f,c,d)) = ((d - c) * E)

    proof

      let f be PartFunc of REAL , the carrier of Y;

      assume that

       A1: a <= b & c in ['a, b'] & d in ['a, b'] and

       A3: ['a, b'] c= ( dom f) & for x be Real st x in ['a, b'] holds (f /. x) = E;

      per cases ;

        suppose

         A5: c <= d;

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

        then ['c, d'] c= ['a, b'] by A1, Lm2;

        then ['c, d'] c= ( dom f) & for x be Real st x in ['c, d'] holds (f /. x) = E by A3;

        hence ( integral (f,c,d)) = ((d - c) * E) by A5, Th1929;

      end;

        suppose

         A8: not c <= d;

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

        then ['d, c'] c= ['a, b'] by A1, Lm2;

        then

         A10: ['d, c'] c= ( dom f) & for x be Real st x in ['d, c'] holds (f /. x) = E by A3;

        then ( integral (f,c,d)) = ( - ( integral (f,d,c))) by A8, Th1947;

        then ( integral (f,c,d)) = ( - ((c - d) * E)) by A8, A10, Th1929;

        then ( integral (f,c,d)) = (( - (c - d)) * E) by RLVECT_1: 79;

        hence ( integral (f,c,d)) = ((d - c) * E);

      end;

    end;

    

     Th1931: for f be continuous PartFunc of REAL , the carrier of Y st a <= b & c <= d & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'] holds ( integral (f,a,d)) = (( integral (f,a,c)) + ( integral (f,c,d)))

    proof

      let f be continuous PartFunc of REAL , the carrier of Y;

      assume

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

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

      then

       A2: a <= c & c <= b & a <= d & d <= b by A1, XXREAL_1: 1;

      then

       A3: ['a, d'] c= ['a, b'] & c in ['a, d'] by A1, INTEGR19: 1;

      then ['a, d'] c= ( dom f) by A1;

      hence ( integral (f,a,d)) = (( integral (f,a,c)) + ( integral (f,c,d))) by A2, A3, Th1908;

    end;

    theorem :: INTEGR21:29

    for f be continuous PartFunc of REAL , the carrier of Y st a <= b & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'] holds ( integral (f,a,d)) = (( integral (f,a,c)) + ( integral (f,c,d)))

    proof

      let f be continuous PartFunc of REAL , the carrier of Y;

      assume

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

      per cases ;

        suppose

         A2: not c <= d;

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

        then c <= b & a <= d by A1, XXREAL_1: 1;

        then

         A3: ['d, c'] c= ( dom f) by A1, A2, INTEGR19: 2;

        ( integral (f,a,c)) = (( integral (f,a,d)) + ( integral (f,d,c))) by A1, A2, Th1931;

        

        then (( integral (f,a,c)) - ( integral (f,d,c))) = (( integral (f,a,d)) + (( integral (f,d,c)) - ( integral (f,d,c)))) by RLVECT_1: 28

        .= (( integral (f,a,d)) + ( 0. Y)) by RLVECT_1: 15;

        hence thesis by A3, A2, Th1947;

      end;

        suppose c <= d;

        hence thesis by A1, Th1931;

      end;

    end;

    theorem :: INTEGR21:30

    for f,g be continuous PartFunc of REAL , the carrier of Y st a <= b & ['a, b'] c= ( dom f) & ['a, b'] c= ( dom g) & c in ['a, b'] & d in ['a, b'] holds ( integral ((f - g),c,d)) = (( integral (f,c,d)) - ( integral (g,c,d)))

    proof

      let f,g be continuous PartFunc of REAL , the carrier of Y;

      assume

       A1: a <= b & ['a, b'] c= ( dom f) & ['a, b'] c= ( dom g) & c in ['a, b'] & d in ['a, b'];

      per cases ;

        suppose

         A2: not c <= d;

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

        then ['d, c'] c= ['a, b'] by A1, Lm2;

        then

         A7: ['d, c'] c= ( dom f) & ['d, c'] c= ( dom g) by A1;

        then ['d, c'] c= (( dom f) /\ ( dom g)) by XBOOLE_1: 19;

        then ['d, c'] c= ( dom (f - g)) by VFUNCT_1:def 2;

        then

         A11: ( integral ((f - g),c,d)) = ( - ( integral ((f - g),d,c))) & ( integral (f,c,d)) = ( - ( integral (f,d,c))) & ( integral (g,c,d)) = ( - ( integral (g,d,c))) by A2, A7, Th1947;

        ( integral ((f - g),d,c)) = (( integral (f,d,c)) - ( integral (g,d,c))) by A1, A2, Th1928;

        then ( integral ((f - g),c,d)) = (( integral (g,d,c)) + ( integral (f,c,d))) by A11, RLVECT_1: 33;

        hence thesis by A11;

      end;

        suppose c <= d;

        hence thesis by A1, Th1928;

      end;

    end;