integr15.miz



    begin

    reserve Z for set;

    definition

      let A be non empty closed_interval Subset of REAL ;

      let f be Function of A, REAL ;

      let D be Division of A;

      :: INTEGR15:def1

      mode middle_volume of f,D -> FinSequence of REAL means

      : Def1: ( len it ) = ( len D) & for i be Nat st i in ( dom D) holds ex r be Element of REAL st r in ( rng (f | ( divset (D,i)))) & (it . i) = (r * ( vol ( divset (D,i))));

      correctness

      proof

        defpred P1[ Nat, Real] means ex r be Element of REAL st r in ( rng (f | ( divset (D,$1)))) & $2 = (r * ( vol ( divset (D,$1))));

        

         A1: ( Seg ( len D)) = ( dom D) by FINSEQ_1:def 3;

        

         A2: for k be Nat st k in ( Seg ( len D)) holds ex x be Element of REAL st P1[k, x]

        proof

          let k be Nat;

          assume k in ( Seg ( len D));

          then

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

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

          then ( dom (f | ( divset (D,k)))) = ( divset (D,k)) by A3, INTEGRA1: 8, RELAT_1: 62;

          then ( rng (f | ( divset (D,k)))) is non empty by RELAT_1: 42;

          then

          consider r be object such that

           A4: r in ( rng (f | ( divset (D,k))));

          reconsider r as Element of REAL by A4;

          (r * ( vol ( divset (D,k)))) is Element of REAL by XREAL_0:def 1;

          hence thesis by A4;

        end;

        consider p be FinSequence of REAL such that

         A5: ( dom p) = ( Seg ( len D)) & for k be Nat st k in ( Seg ( len D)) holds P1[k, (p . k)] from FINSEQ_1:sch 5( A2);

        ( len p) = ( len D) by A5, FINSEQ_1:def 3;

        hence thesis by A5, A1;

      end;

    end

    

     Lm1: for A be non empty closed_interval Subset of REAL , f be Function of A, REAL , D be Division of A, F be middle_volume of f, D, i be Nat st (f | A) is bounded_below & i in ( dom D) holds (( lower_volume (f,D)) . i) <= (F . i)

    proof

      let A be non empty closed_interval Subset of REAL , f be Function of A, REAL , D be Division of A, F be middle_volume of f, D, i be Nat;

      assume that

       A1: (f | A) is bounded_below and

       A2: i in ( dom D);

      

       A3: (( lower_volume (f,D)) . i) = (( lower_bound ( rng (f | ( divset (D,i))))) * ( vol ( divset (D,i)))) by A2, INTEGRA1:def 7;

      consider r be Element of REAL such that

       A4: r in ( rng (f | ( divset (D,i)))) and

       A5: (F . i) = (r * ( vol ( divset (D,i)))) by A2, Def1;

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

      then ( rng (f | ( divset (D,i)))) is bounded_below by RELAT_1: 70, XXREAL_2: 44;

      then 0 <= ( vol ( divset (D,i))) & ( lower_bound ( rng (f | ( divset (D,i))))) <= r by A4, INTEGRA1: 9, SEQ_4:def 2;

      hence (( lower_volume (f,D)) . i) <= (F . i) by A5, A3, XREAL_1: 64;

    end;

    

     Lm2: for A be non empty closed_interval Subset of REAL , f be Function of A, REAL , D be Division of A, e be Real st (f | A) is bounded_below & 0 < e holds ex F be middle_volume of f, D st for i be Nat st i in ( dom D) holds (( lower_volume (f,D)) . i) <= (F . i) & (F . i) < ((( lower_volume (f,D)) . i) + e)

    proof

      let A be non empty closed_interval Subset of REAL , f be Function of A, REAL , D be Division of A, e be Real;

      assume that

       A1: (f | A) is bounded_below and

       A2: 0 < e;

      defpred P1[ Nat, Real] means ex r be Element of REAL st r in ( rng (f | ( divset (D,$1)))) & $2 = (r * ( vol ( divset (D,$1)))) & (( lower_volume (f,D)) . $1) <= $2 & $2 < ((( lower_volume (f,D)) . $1) + e);

      

       A3: for k be Nat st k in ( Seg ( len D)) holds ex x be Element of REAL st P1[k, x]

      proof

        let k be Nat;

        assume k in ( Seg ( len D));

        then

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

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

        then ( dom (f | ( divset (D,k)))) = ( divset (D,k)) by A4, INTEGRA1: 8, RELAT_1: 62;

        then

         A5: ( rng (f | ( divset (D,k)))) is non empty by RELAT_1: 42;

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

        then

         A6: ( rng (f | ( divset (D,k)))) is bounded_below by RELAT_1: 70, XXREAL_2: 44;

        per cases ;

          suppose

           A7: ( vol ( divset (D,k))) = 0 ;

          consider r be object such that

           A8: r in ( rng (f | ( divset (D,k)))) by A5;

          reconsider r as Element of REAL by A8;

          reconsider x = (r * ( vol ( divset (D,k)))) as Element of REAL by XREAL_0:def 1;

          

           A9: (( lower_volume (f,D)) . k) = (( lower_bound ( rng (f | ( divset (D,k))))) * ( vol ( divset (D,k)))) by A4, INTEGRA1:def 7

          .= 0 by A7;

          then x < ((( lower_volume (f,D)) . k) + e) by A2, A7;

          hence ex x be Element of REAL st P1[k, x] by A7, A8, A9;

        end;

          suppose

           A10: ( vol ( divset (D,k))) <> 0 ;

          set l = ( lower_bound ( rng (f | ( divset (D,k)))));

          set e1 = (e / ( vol ( divset (D,k))));

          

           A11: 0 < ( vol ( divset (D,k))) by A10, INTEGRA1: 9;

          then 0 < e1 by A2, XREAL_1: 139;

          then

          consider r be Real such that

           A12: r in ( rng (f | ( divset (D,k)))) and

           A13: r < (l + e1) by A6, A5, SEQ_4:def 2;

          

           A14: (( lower_volume (f,D)) . k) = (( lower_bound ( rng (f | ( divset (D,k))))) * ( vol ( divset (D,k)))) by A4, INTEGRA1:def 7;

          reconsider x = (r * ( vol ( divset (D,k)))) as Element of REAL by XREAL_0:def 1;

          x < ((l + e1) * ( vol ( divset (D,k)))) by A11, A13, XREAL_1: 68;

          then x < ((( lower_volume (f,D)) . k) + (e1 * ( vol ( divset (D,k))))) by A14;

          then

           A15: x < ((( lower_volume (f,D)) . k) + e) by A10, XCMPLX_1: 87;

          l <= r by A6, A12, SEQ_4:def 2;

          then (( lower_volume (f,D)) . k) <= x by A11, A14, XREAL_1: 64;

          hence ex x be Element of REAL st P1[k, x] by A12, A15;

        end;

      end;

      consider p be FinSequence of REAL such that

       A16: ( dom p) = ( Seg ( len D)) & for k be Nat st k in ( Seg ( len D)) holds P1[k, (p . k)] from FINSEQ_1:sch 5( A3);

       A17:

      now

        let i be Nat;

        assume i in ( dom D);

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

        then

        consider r be Element of REAL such that

         A18: r in ( rng (f | ( divset (D,i)))) & (p . i) = (r * ( vol ( divset (D,i)))) and (( lower_volume (f,D)) . i) <= (p . i) and (p . i) < ((( lower_volume (f,D)) . i) + e) by A16;

        take r;

        thus r in ( rng (f | ( divset (D,i)))) & (p . i) = (r * ( vol ( divset (D,i)))) by A18;

      end;

      ( len p) = ( len D) by A16, FINSEQ_1:def 3;

      then

      reconsider p as middle_volume of f, D by A17, Def1;

      now

        let i be Nat;

        assume i in ( dom D);

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

        then ex r be Element of REAL st r in ( rng (f | ( divset (D,i)))) & (p . i) = (r * ( vol ( divset (D,i)))) & (( lower_volume (f,D)) . i) <= (p . i) & (p . i) < ((( lower_volume (f,D)) . i) + e) by A16;

        hence (( lower_volume (f,D)) . i) <= (p . i) & (p . i) < ((( lower_volume (f,D)) . i) + e);

      end;

      hence thesis;

    end;

    

     Lm3: for A be non empty closed_interval Subset of REAL , f be Function of A, REAL , D be Division of A, e be Real st (f | A) is bounded_above & 0 < e holds ex F be middle_volume of f, D st for i be Nat st i in ( dom D) holds (F . i) <= (( upper_volume (f,D)) . i) & ((( upper_volume (f,D)) . i) - e) < (F . i)

    proof

      let A be non empty closed_interval Subset of REAL , f be Function of A, REAL , D be Division of A, e be Real;

      assume that

       A1: (f | A) is bounded_above and

       A2: 0 < e;

      defpred P1[ Nat, Real] means ex r be Element of REAL st r in ( rng (f | ( divset (D,$1)))) & $2 = (r * ( vol ( divset (D,$1)))) & $2 <= (( upper_volume (f,D)) . $1) & ((( upper_volume (f,D)) . $1) - e) < $2;

      

       A3: for k be Nat st k in ( Seg ( len D)) holds ex x be Element of REAL st P1[k, x]

      proof

        let k be Nat;

        assume k in ( Seg ( len D));

        then

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

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

        then ( dom (f | ( divset (D,k)))) = ( divset (D,k)) by A4, INTEGRA1: 8, RELAT_1: 62;

        then

         A5: ( rng (f | ( divset (D,k)))) is non empty by RELAT_1: 42;

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

        then

         A6: ( rng (f | ( divset (D,k)))) is bounded_above by RELAT_1: 70, XXREAL_2: 43;

        per cases ;

          suppose

           A7: ( vol ( divset (D,k))) = 0 ;

          consider r be object such that

           A8: r in ( rng (f | ( divset (D,k)))) by A5;

          reconsider r as Element of REAL by A8;

          reconsider x = (r * ( vol ( divset (D,k)))) as Element of REAL by XREAL_0:def 1;

          

           A9: (( upper_volume (f,D)) . k) = (( upper_bound ( rng (f | ( divset (D,k))))) * ( vol ( divset (D,k)))) by A4, INTEGRA1:def 6

          .= 0 by A7;

          then ((( upper_volume (f,D)) . k) - e) < x by A2, A7;

          hence ex x be Element of REAL st P1[k, x] by A7, A8, A9;

        end;

          suppose

           A10: ( vol ( divset (D,k))) <> 0 ;

          set l = ( upper_bound ( rng (f | ( divset (D,k)))));

          set e1 = (e / ( vol ( divset (D,k))));

          

           A11: 0 < ( vol ( divset (D,k))) by A10, INTEGRA1: 9;

          then 0 < e1 by A2, XREAL_1: 139;

          then

          consider r be Real such that

           A12: r in ( rng (f | ( divset (D,k)))) and

           A13: (l - e1) < r by A6, A5, SEQ_4:def 1;

          

           A14: (( upper_volume (f,D)) . k) = (( upper_bound ( rng (f | ( divset (D,k))))) * ( vol ( divset (D,k)))) by A4, INTEGRA1:def 6;

          reconsider x = (r * ( vol ( divset (D,k)))) as Element of REAL by XREAL_0:def 1;

          ((l - e1) * ( vol ( divset (D,k)))) < x by A11, A13, XREAL_1: 68;

          then ((( upper_volume (f,D)) . k) - (e1 * ( vol ( divset (D,k))))) < x by A14;

          then

           A15: ((( upper_volume (f,D)) . k) - e) < x by A10, XCMPLX_1: 87;

          r <= l by A6, A12, SEQ_4:def 1;

          then x <= (( upper_volume (f,D)) . k) by A11, A14, XREAL_1: 64;

          hence ex x be Element of REAL st P1[k, x] by A12, A15;

        end;

      end;

      consider p be FinSequence of REAL such that

       A16: ( dom p) = ( Seg ( len D)) & for k be Nat st k in ( Seg ( len D)) holds P1[k, (p . k)] from FINSEQ_1:sch 5( A3);

       A17:

      now

        let i be Nat;

        assume i in ( dom D);

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

        then

        consider r be Element of REAL such that

         A18: r in ( rng (f | ( divset (D,i)))) & (p . i) = (r * ( vol ( divset (D,i)))) and (p . i) <= (( upper_volume (f,D)) . i) and ((( upper_volume (f,D)) . i) - e) < (p . i) by A16;

        take r;

        thus r in ( rng (f | ( divset (D,i)))) & (p . i) = (r * ( vol ( divset (D,i)))) by A18;

      end;

      ( len p) = ( len D) by A16, FINSEQ_1:def 3;

      then

      reconsider p as middle_volume of f, D by A17, Def1;

      now

        let i be Nat;

        assume i in ( dom D);

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

        then ex r be Element of REAL st r in ( rng (f | ( divset (D,i)))) & (p . i) = (r * ( vol ( divset (D,i)))) & (p . i) <= (( upper_volume (f,D)) . i) & ((( upper_volume (f,D)) . i) - e) < (p . i) by A16;

        hence (p . i) <= (( upper_volume (f,D)) . i) & ((( upper_volume (f,D)) . i) - e) < (p . i);

      end;

      hence thesis;

    end;

    

     Lm4: for A be non empty closed_interval Subset of REAL , f be Function of A, REAL , D be Division of A, F be middle_volume of f, D, i be Nat st (f | A) is bounded_above & i in ( dom D) holds (F . i) <= (( upper_volume (f,D)) . i)

    proof

      let A be non empty closed_interval Subset of REAL , f be Function of A, REAL , D be Division of A, F be middle_volume of f, D, i be Nat;

      assume that

       A1: (f | A) is bounded_above and

       A2: i in ( dom D);

      

       A3: (( upper_volume (f,D)) . i) = (( upper_bound ( rng (f | ( divset (D,i))))) * ( vol ( divset (D,i)))) by A2, INTEGRA1:def 6;

      consider r be Element of REAL such that

       A4: r in ( rng (f | ( divset (D,i)))) and

       A5: (F . i) = (r * ( vol ( divset (D,i)))) by A2, Def1;

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

      then ( rng (f | ( divset (D,i)))) is bounded_above by RELAT_1: 70, XXREAL_2: 43;

      then 0 <= ( vol ( divset (D,i))) & r <= ( upper_bound ( rng (f | ( divset (D,i))))) by A4, INTEGRA1: 9, SEQ_4:def 1;

      hence (F . i) <= (( upper_volume (f,D)) . i) by A5, A3, XREAL_1: 64;

    end;

    definition

      let A be non empty closed_interval Subset of REAL ;

      let f be Function of A, REAL ;

      let D be Division of A;

      let F be middle_volume of f, D;

      :: INTEGR15:def2

      func middle_sum (f,F) -> Real equals ( Sum F);

      correctness ;

    end

    theorem :: INTEGR15:1

    

     Th1: for A be non empty closed_interval Subset of REAL , f be Function of A, REAL , D be Division of A, F be middle_volume of f, D st (f | A) is bounded_below holds ( lower_sum (f,D)) <= ( middle_sum (f,F))

    proof

      let A be non empty closed_interval Subset of REAL , f be Function of A, REAL , D be Division of A, F be middle_volume of f, D;

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

      then

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

      ( len F) = ( len D) by Def1;

      then

      reconsider q = F as Element of (( len D) -tuples_on REAL ) by FINSEQ_2: 92;

      assume

       A1: (f | A) is bounded_below;

      now

        let i be Nat;

        assume i in ( Seg ( len D));

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

        hence (p . i) <= (q . i) by A1, Lm1;

      end;

      hence thesis by RVSUM_1: 82;

    end;

    theorem :: INTEGR15:2

    

     Th2: for A be non empty closed_interval Subset of REAL , f be Function of A, REAL , D be Division of A, F be middle_volume of f, D st (f | A) is bounded_above holds ( middle_sum (f,F)) <= ( upper_sum (f,D))

    proof

      let A be non empty closed_interval Subset of REAL , f be Function of A, REAL , D be Division of A, F be middle_volume of f, D;

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

      then

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

      ( len F) = ( len D) by Def1;

      then

      reconsider q = F as Element of (( len D) -tuples_on REAL ) by FINSEQ_2: 92;

      assume

       A1: (f | A) is bounded_above;

      now

        let i be Nat;

        assume i in ( Seg ( len D));

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

        hence (q . i) <= (p . i) by A1, Lm4;

      end;

      hence thesis by RVSUM_1: 82;

    end;

    theorem :: INTEGR15:3

    

     Th3: for A be non empty closed_interval Subset of REAL , f be Function of A, REAL , D be Division of A, e be Real st (f | A) is bounded_below & 0 < e holds ex F be middle_volume of f, D st ( middle_sum (f,F)) <= (( lower_sum (f,D)) + e)

    proof

      let A be non empty closed_interval Subset of REAL , f be Function of A, REAL , D be Division of A, e be Real;

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

      then

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

      reconsider e1 = (e / ( len D)) as Element of REAL by XREAL_0:def 1;

      assume (f | A) is bounded_below & 0 < e;

      then

      consider F be middle_volume of f, D such that

       A1: for i be Nat st i in ( dom D) holds (( lower_volume (f,D)) . i) <= (F . i) & (F . i) < ((( lower_volume (f,D)) . i) + e1) by Lm2, XREAL_1: 139;

      set s = (( len D) |-> e1);

      reconsider t = (p + s) as Element of (( len D) -tuples_on REAL );

      take F;

      ( len F) = ( len D) by Def1;

      then

      reconsider q = F as Element of (( len D) -tuples_on REAL ) by FINSEQ_2: 92;

      now

        let i be Nat;

        assume

         A2: i in ( Seg ( len D));

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

        then (q . i) <= ((p . i) + e1) by A1;

        then (q . i) <= ((p . i) + (s . i)) by A2, FINSEQ_2: 57;

        hence (q . i) <= (t . i) by RVSUM_1: 11;

      end;

      then ( Sum q) <= ( Sum t) by RVSUM_1: 82;

      then ( Sum q) <= (( Sum p) + ( Sum s)) by RVSUM_1: 89;

      then ( Sum q) <= (( Sum p) + (( len D) * e1)) by RVSUM_1: 80;

      hence thesis by XCMPLX_1: 87;

    end;

    theorem :: INTEGR15:4

    

     Th4: for A be non empty closed_interval Subset of REAL , f be Function of A, REAL , D be Division of A, e be Real st (f | A) is bounded_above & 0 < e holds ex F be middle_volume of f, D st (( upper_sum (f,D)) - e) <= ( middle_sum (f,F))

    proof

      let A be non empty closed_interval Subset of REAL , f be Function of A, REAL , D be Division of A, e be Real;

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

      then

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

      reconsider e1 = (e / ( len D)) as Element of REAL by XREAL_0:def 1;

      assume (f | A) is bounded_above & 0 < e;

      then

      consider F be middle_volume of f, D such that

       A1: for i be Nat st i in ( dom D) holds (F . i) <= (( upper_volume (f,D)) . i) & ((( upper_volume (f,D)) . i) - e1) < (F . i) by Lm3, XREAL_1: 139;

      set s = (( len D) |-> e1);

      reconsider t = (p - s) as Element of (( len D) -tuples_on REAL );

      take F;

      ( len F) = ( len D) by Def1;

      then

      reconsider q = F as Element of (( len D) -tuples_on REAL ) by FINSEQ_2: 92;

      now

        let i be Nat;

        assume

         A2: i in ( Seg ( len D));

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

        then ((p . i) - e1) <= (q . i) by A1;

        then ((p . i) - (s . i)) <= (q . i) by A2, FINSEQ_2: 57;

        hence (t . i) <= (q . i) by RVSUM_1: 27;

      end;

      then ( Sum t) <= ( Sum q) by RVSUM_1: 82;

      then (( Sum p) - ( Sum s)) <= ( Sum q) by RVSUM_1: 90;

      then (( Sum p) - (( len D) * e1)) <= ( Sum q) by RVSUM_1: 80;

      hence thesis by XCMPLX_1: 87;

    end;

    definition

      let A be non empty closed_interval Subset of REAL , f be Function of A, REAL , T be DivSequence of A;

      :: INTEGR15:def3

      mode middle_volume_Sequence of f,T -> sequence of ( REAL * ) means

      : Def3: for k be Element of NAT holds (it . k) is middle_volume of f, (T . k);

      correctness

      proof

        defpred P[ Element of NAT , set] means $2 is middle_volume of f, (T . $1);

        

         A1: for x be Element of NAT holds ex y be Element of ( REAL * ) st P[x, y]

        proof

          let x be Element of NAT ;

          set y = the middle_volume of f, (T . x);

          reconsider y as Element of ( REAL * ) by FINSEQ_1:def 11;

          y is middle_volume of f, (T . x);

          hence thesis;

        end;

        ex f be sequence of ( REAL * ) st for x be Element of NAT holds P[x, (f . x)] from FUNCT_2:sch 3( A1);

        hence thesis;

      end;

    end

    definition

      let A be non empty closed_interval Subset of REAL , f be Function of A, REAL , T be DivSequence of A, S be middle_volume_Sequence of f, T, k be Element of NAT ;

      :: original: .

      redefine

      func S . k -> middle_volume of f, (T . k) ;

      coherence by Def3;

    end

    definition

      let A be non empty closed_interval Subset of REAL , f be Function of A, REAL , T be DivSequence of A, S be middle_volume_Sequence of f, T;

      :: INTEGR15:def4

      func middle_sum (f,S) -> Real_Sequence means

      : Def4: for i be Element of NAT holds (it . i) = ( middle_sum (f,(S . i)));

      existence

      proof

        deffunc H1( Nat) = ( middle_sum (f,(S . ( In ($1, NAT )))));

        consider IT be Real_Sequence such that

         A1: for i be Nat holds (IT . i) = H1(i) from SEQ_1:sch 1;

        take IT;

        let i be Element of NAT ;

        (IT . i) = H1(i) by A1;

        hence thesis;

      end;

      uniqueness

      proof

        let F1,F2 be Real_Sequence;

        assume that

         A2: for i be Element of NAT holds (F1 . i) = ( middle_sum (f,(S . i))) and

         A3: for i be Element of NAT holds (F2 . i) = ( middle_sum (f,(S . i)));

        for i be Element of NAT holds (F1 . i) = (F2 . i)

        proof

          let i be Element of NAT ;

          (F1 . i) = ( middle_sum (f,(S . i))) by A2

          .= (F2 . i) by A3;

          hence (F1 . i) = (F2 . i);

        end;

        hence F1 = F2 by FUNCT_2: 63;

      end;

    end

    theorem :: INTEGR15:5

    

     Th5: for A be non empty closed_interval Subset of REAL , f be Function of A, REAL , T be DivSequence of A, S be middle_volume_Sequence of f, T, i be Element of NAT st (f | A) is bounded_below holds (( lower_sum (f,T)) . i) <= (( middle_sum (f,S)) . i)

    proof

      let A be non empty closed_interval Subset of REAL , f be Function of A, REAL , T be DivSequence of A, S be middle_volume_Sequence of f, T, i be Element of NAT ;

      assume

       A1: (f | A) is bounded_below;

      (( middle_sum (f,S)) . i) = ( middle_sum (f,(S . i))) & (( lower_sum (f,T)) . i) = ( lower_sum (f,(T . i))) by Def4, INTEGRA2:def 3;

      hence thesis by A1, Th1;

    end;

    theorem :: INTEGR15:6

    

     Th6: for A be non empty closed_interval Subset of REAL , f be Function of A, REAL , T be DivSequence of A, S be middle_volume_Sequence of f, T, i be Element of NAT st (f | A) is bounded_above holds (( middle_sum (f,S)) . i) <= (( upper_sum (f,T)) . i)

    proof

      let A be non empty closed_interval Subset of REAL , f be Function of A, REAL , T be DivSequence of A, S be middle_volume_Sequence of f, T, i be Element of NAT ;

      assume

       A1: (f | A) is bounded_above;

      (( middle_sum (f,S)) . i) = ( middle_sum (f,(S . i))) & (( upper_sum (f,T)) . i) = ( upper_sum (f,(T . i))) by Def4, INTEGRA2:def 2;

      hence thesis by A1, Th2;

    end;

    theorem :: INTEGR15:7

    

     Th7: for A be non empty closed_interval Subset of REAL , f be Function of A, REAL , T be DivSequence of A, e be Element of REAL st 0 < e & (f | A) is bounded_below holds ex S be middle_volume_Sequence of f, T st for i be Element of NAT holds (( middle_sum (f,S)) . i) <= ((( lower_sum (f,T)) . i) + e)

    proof

      let A be non empty closed_interval Subset of REAL , f be Function of A, REAL , T be DivSequence of A, e be Element of REAL ;

      defpred P[ Element of NAT , set] means $2 is middle_volume of f, (T . $1) & ex z be middle_volume of f, (T . $1) st z = $2 & ( middle_sum (f,z)) <= (( lower_sum (f,(T . $1))) + e);

      assume

       A1: 0 < e & (f | A) is bounded_below;

      

       A2: for x be Element of NAT holds ex y be Element of ( REAL * ) st P[x, y]

      proof

        let x be Element of NAT ;

        consider z be middle_volume of f, (T . x) such that

         A3: ( middle_sum (f,z)) <= (( lower_sum (f,(T . x))) + e) by A1, Th3;

        reconsider y = z as Element of ( REAL * ) by FINSEQ_1:def 11;

        take y;

        thus thesis by A3;

      end;

      consider F be sequence of ( REAL * ) such that

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

      reconsider F as middle_volume_Sequence of f, T by A4, Def3;

      now

        let x be Element of NAT ;

        ex z be middle_volume of f, (T . x) st z = (F . x) & ( middle_sum (f,z)) <= (( lower_sum (f,(T . x))) + e) by A4;

        then (( middle_sum (f,F)) . x) <= (( lower_sum (f,(T . x))) + e) by Def4;

        hence (( middle_sum (f,F)) . x) <= ((( lower_sum (f,T)) . x) + e) by INTEGRA2:def 3;

      end;

      hence thesis;

    end;

    theorem :: INTEGR15:8

    

     Th8: for A be non empty closed_interval Subset of REAL , f be Function of A, REAL , T be DivSequence of A, e be Element of REAL st 0 < e & (f | A) is bounded_above holds ex S be middle_volume_Sequence of f, T st for i be Element of NAT holds ((( upper_sum (f,T)) . i) - e) <= (( middle_sum (f,S)) . i)

    proof

      let A be non empty closed_interval Subset of REAL , f be Function of A, REAL , T be DivSequence of A, e be Element of REAL ;

      defpred P[ Element of NAT , set] means $2 is middle_volume of f, (T . $1) & ex z be middle_volume of f, (T . $1) st z = $2 & (( upper_sum (f,(T . $1))) - e) <= ( middle_sum (f,z));

      assume

       A1: 0 < e & (f | A) is bounded_above;

      

       A2: for x be Element of NAT holds ex y be Element of ( REAL * ) st P[x, y]

      proof

        let x be Element of NAT ;

        consider z be middle_volume of f, (T . x) such that

         A3: (( upper_sum (f,(T . x))) - e) <= ( middle_sum (f,z)) by A1, Th4;

        reconsider y = z as Element of ( REAL * ) by FINSEQ_1:def 11;

        take y;

        thus thesis by A3;

      end;

      consider F be sequence of ( REAL * ) such that

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

      reconsider F as middle_volume_Sequence of f, T by A4, Def3;

      now

        let x be Element of NAT ;

        ex z be middle_volume of f, (T . x) st z = (F . x) & (( upper_sum (f,(T . x))) - e) <= ( middle_sum (f,z)) by A4;

        then (( upper_sum (f,(T . x))) - e) <= (( middle_sum (f,F)) . x) by Def4;

        hence ((( upper_sum (f,T)) . x) - e) <= (( middle_sum (f,F)) . x) by INTEGRA2:def 2;

      end;

      hence thesis;

    end;

    

     Lm5: for p,q,r be Real_Sequence st p is convergent & r is convergent & ( lim p) = ( lim r) & (for i be Element of NAT holds (p . i) <= (q . i)) & (for i be Element of NAT holds (q . i) <= (r . i)) holds q is convergent & ( lim p) = ( lim q) & ( lim r) = ( lim q)

    proof

      let p,q,r be Real_Sequence;

      assume that

       A1: p is convergent and

       A2: r is convergent and

       A3: ( lim p) = ( lim r) and

       A4: for i be Element of NAT holds (p . i) <= (q . i) and

       A5: for i be Element of NAT holds (q . i) <= (r . i);

       A6:

      now

        let e be Real;

        assume

         A7: 0 < e;

        then

        consider n1 be Nat such that

         A8: for m be Nat st n1 <= m holds |.((p . m) - ( lim p)).| < e by A1, SEQ_2:def 7;

        consider n2 be Nat such that

         A9: for m be Nat st n2 <= m holds |.((r . m) - ( lim r)).| < e by A2, A7, SEQ_2:def 7;

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

        take n;

        thus for m be Nat st n <= m holds |.((q . m) - ( lim p)).| < e

        proof

          let m be Nat;

          assume

           A10: n <= m;

          

           A11: m in NAT by ORDINAL1:def 12;

          n1 <= n by XXREAL_0: 25;

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

          then |.((p . m) - ( lim p)).| < e by A8;

          then (p . m) in ].(( lim p) - e), (( lim p) + e).[ by RCOMP_1: 1;

          then (p . m) in { z where z be Real : (( lim p) - e) < z & z < (( lim p) + e) } by RCOMP_1:def 2;

          then

           A12: ex z be Real st z = (p . m) & (( lim p) - e) < z & z < (( lim p) + e);

          (p . m) <= (q . m) by A4, A11;

          then

           A13: (( lim p) - e) < (q . m) by A12, XXREAL_0: 2;

          n2 <= n by XXREAL_0: 25;

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

          then |.((r . m) - ( lim r)).| < e by A9;

          then (r . m) in ].(( lim r) - e), (( lim r) + e).[ by RCOMP_1: 1;

          then (r . m) in { z where z be Real : (( lim r) - e) < z & z < (( lim r) + e) } by RCOMP_1:def 2;

          then

           A14: ex z be Real st z = (r . m) & (( lim r) - e) < z & z < (( lim r) + e);

          (q . m) <= (r . m) by A5, A11;

          then (q . m) < (( lim p) + e) by A3, A14, XXREAL_0: 2;

          then (q . m) in { z where z be Real : (( lim p) - e) < z & z < (( lim p) + e) } by A13;

          then (q . m) in ].(( lim p) - e), (( lim p) + e).[ by RCOMP_1:def 2;

          hence |.((q . m) - ( lim p)).| < e by RCOMP_1: 1;

        end;

      end;

      hence q is convergent by SEQ_2:def 6;

      hence ( lim q) = ( lim p) & ( lim q) = ( lim r) by A3, A6, SEQ_2:def 7;

    end;

    theorem :: INTEGR15:9

    

     Th9: for A be non empty closed_interval Subset of REAL , f be Function of A, REAL , T be DivSequence of A, S be middle_volume_Sequence of f, T st f is bounded & f is integrable & ( delta T) is convergent & ( lim ( delta T)) = 0 holds ( middle_sum (f,S)) is convergent & ( lim ( middle_sum (f,S))) = ( integral f)

    proof

      let A be non empty closed_interval Subset of REAL , f be Function of A, REAL , T be DivSequence of A, S be middle_volume_Sequence of f, T;

      assume that

       A1: f is bounded and

       A2: f is integrable and

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

      (f | A) is bounded_below by A1;

      then

       A5: for i be Element of NAT holds (( lower_sum (f,T)) . i) <= (( middle_sum (f,S)) . i) by Th5;

      

       A6: (f | A) = f;

      then

       A7: ( lower_sum (f,T)) is convergent & ( upper_sum (f,T)) is convergent by A1, A3, INTEGRA4: 8, INTEGRA4: 9;

      (f | A) is bounded_above by A1;

      then

       A8: for i be Element of NAT holds (( middle_sum (f,S)) . i) <= (( upper_sum (f,T)) . i) by Th6;

      

       A9: (( lim ( upper_sum (f,T))) - ( lim ( lower_sum (f,T)))) = 0 by A1, A2, A3, A6, INTEGRA4: 12;

      then ( lim ( lower_sum (f,T))) = ( integral f) by A1, A3, A6, INTEGRA4: 9;

      hence thesis by A7, A9, A5, A8, Lm5;

    end;

    theorem :: INTEGR15:10

    

     Th10: for A be non empty closed_interval Subset of REAL , f be Function of A, REAL st f is bounded holds f is integrable iff ex I be Real st 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 A be non empty closed_interval Subset of REAL , f be Function of A, REAL ;

      assume

       A1: f is bounded;

      hereby

        assume

         A2: f is integrable;

        reconsider I = ( integral f) as Real;

        take I;

        thus 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 by A1, A2, Th9;

      end;

      

       A3: (f | A) is bounded by A1;

      now

        given I be Real such that

         A4: 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;

        

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

        proof

          let T be DivSequence of A;

          set S = the middle_volume_Sequence of f, T;

           A6:

          now

            let i be Nat;

            

             A7: i in NAT by ORDINAL1:def 12;

            (( middle_sum (f,S)) . i) <= (( upper_sum (f,T)) . i) by A3, Th6, A7;

            then ((( middle_sum (f,S)) . i) - (( middle_sum (f,S)) . i)) <= ((( upper_sum (f,T)) . i) - (( middle_sum (f,S)) . i)) by XREAL_1: 9;

            hence 0 <= ((( upper_sum (f,T)) - ( middle_sum (f,S))) . i) by VALUED_1: 15, A7;

          end;

          assume

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

          then

           A9: ( upper_sum (f,T)) is convergent by A3, INTEGRA4: 9;

           A10:

          now

            let e1 be Real;

            reconsider e = e1 as Element of REAL by XREAL_0:def 1;

            assume 0 < e1;

            then

            consider S be middle_volume_Sequence of f, T such that

             A11: for i be Element of NAT holds ((( upper_sum (f,T)) . i) - e) <= (( middle_sum (f,S)) . i) by A3, Th8;

             A12:

            now

              let i be Nat;

              

               A13: i in NAT by ORDINAL1:def 12;

              ((( upper_sum (f,T)) . i) - e) <= (( middle_sum (f,S)) . i) by A11, A13;

              then (((( upper_sum (f,T)) . i) - e) + e) <= ((( middle_sum (f,S)) . i) + e) by XREAL_1: 6;

              then ((( upper_sum (f,T)) . i) - (( middle_sum (f,S)) . i)) <= (((( middle_sum (f,S)) . i) + e) - (( middle_sum (f,S)) . i)) by XREAL_1: 9;

              hence ((( upper_sum (f,T)) - ( middle_sum (f,S))) . i) <= e by VALUED_1: 15, A13;

            end;

            

             A14: ( middle_sum (f,S)) is convergent by A4, A8;

            then

             A15: (( upper_sum (f,T)) - ( middle_sum (f,S))) is convergent by A9;

            ( lim (( upper_sum (f,T)) - ( middle_sum (f,S)))) = (( lim ( upper_sum (f,T))) - ( lim ( middle_sum (f,S)))) by A9, A14, SEQ_2: 12

            .= (( lim ( upper_sum (f,T))) - I) by A4, A8;

            hence (( lim ( upper_sum (f,T))) - I) <= e1 by A12, A15, PREPOWER: 2;

          end;

          

           A16: ( middle_sum (f,S)) is convergent by A4, A8;

          then

           A17: (( upper_sum (f,T)) - ( middle_sum (f,S))) is convergent by A9;

          ( lim (( upper_sum (f,T)) - ( middle_sum (f,S)))) = (( lim ( upper_sum (f,T))) - ( lim ( middle_sum (f,S)))) by A9, A16, SEQ_2: 12

          .= (( lim ( upper_sum (f,T))) - I) by A4, A8;

          then 0 <= (( lim ( upper_sum (f,T))) - I) by A6, A17, SEQ_2: 17;

          then (( lim ( upper_sum (f,T))) - I) = 0 by A10, XREAL_1: 5;

          hence thesis;

        end;

        

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

        proof

          let T be DivSequence of A;

          set S = the middle_volume_Sequence of f, T;

           A19:

          now

            let i be Nat;

            

             A20: i in NAT by ORDINAL1:def 12;

            (( lower_sum (f,T)) . i) <= (( middle_sum (f,S)) . i) by A3, Th5, A20;

            then ((( lower_sum (f,T)) . i) - (( lower_sum (f,T)) . i)) <= ((( middle_sum (f,S)) . i) - (( lower_sum (f,T)) . i)) by XREAL_1: 9;

            hence 0 <= ((( middle_sum (f,S)) - ( lower_sum (f,T))) . i) by VALUED_1: 15, A20;

          end;

          assume

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

          then

           A22: ( lower_sum (f,T)) is convergent by A3, INTEGRA4: 8;

           A23:

          now

            let e1 be Real;

            reconsider e = e1 as Element of REAL by XREAL_0:def 1;

            assume 0 < e1;

            then

            consider S be middle_volume_Sequence of f, T such that

             A24: for i be Element of NAT holds (( middle_sum (f,S)) . i) <= ((( lower_sum (f,T)) . i) + e) by A3, Th7;

             A25:

            now

              let i be Nat;

              

               A26: i in NAT by ORDINAL1:def 12;

              (( middle_sum (f,S)) . i) <= ((( lower_sum (f,T)) . i) + e) by A24, A26;

              then ((( middle_sum (f,S)) . i) - (( lower_sum (f,T)) . i)) <= (((( lower_sum (f,T)) . i) + e) - (( lower_sum (f,T)) . i)) by XREAL_1: 9;

              hence ((( middle_sum (f,S)) - ( lower_sum (f,T))) . i) <= e by VALUED_1: 15, A26;

            end;

            

             A27: ( middle_sum (f,S)) is convergent by A4, A21;

            then

             A28: (( middle_sum (f,S)) - ( lower_sum (f,T))) is convergent by A22;

            ( lim (( middle_sum (f,S)) - ( lower_sum (f,T)))) = (( lim ( middle_sum (f,S))) - ( lim ( lower_sum (f,T)))) by A22, A27, SEQ_2: 12

            .= (I - ( lim ( lower_sum (f,T)))) by A4, A21;

            hence (I - ( lim ( lower_sum (f,T)))) <= e1 by A25, A28, PREPOWER: 2;

          end;

          

           A29: ( middle_sum (f,S)) is convergent by A4, A21;

          then

           A30: (( middle_sum (f,S)) - ( lower_sum (f,T))) is convergent by A22;

          ( lim (( middle_sum (f,S)) - ( lower_sum (f,T)))) = (( lim ( middle_sum (f,S))) - ( lim ( lower_sum (f,T)))) by A22, A29, SEQ_2: 12

          .= (I - ( lim ( lower_sum (f,T)))) by A4, A21;

          then 0 <= (I - ( lim ( lower_sum (f,T)))) by A19, A30, SEQ_2: 17;

          then (I - ( lim ( lower_sum (f,T)))) = 0 by A23, XREAL_1: 5;

          hence thesis;

        end;

        now

          let T be DivSequence of A;

          assume

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

          

          hence (( lim ( upper_sum (f,T))) - ( lim ( lower_sum (f,T)))) = (( lim ( upper_sum (f,T))) - I) by A18

          .= (I - I) by A5, A31

          .= 0 ;

        end;

        hence f is integrable by A3, INTEGRA4: 12;

      end;

      hence thesis;

    end;

    definition

      let n be Element of NAT ;

      let A be non empty closed_interval Subset of REAL ;

      let f be Function of A, ( REAL n);

      let D be Division of A;

      :: INTEGR15:def5

      mode middle_volume of f,D -> FinSequence of ( REAL n) means

      : Def5: ( len it ) = ( len D) & for i be Nat st i in ( dom D) holds ex r be Element of ( REAL n) st r in ( rng (f | ( divset (D,i)))) & (it . i) = (( vol ( divset (D,i))) * r);

      correctness

      proof

        defpred P1[ Nat, set] means ex r be Element of ( REAL n) st r in ( rng (f | ( divset (D,$1)))) & $2 = (( vol ( divset (D,$1))) * r);

        

         A1: ( Seg ( len D)) = ( dom D) by FINSEQ_1:def 3;

        

         A2: for k be Nat st k in ( Seg ( len D)) holds ex x be Element of ( REAL n) st P1[k, x]

        proof

          let k be Nat;

          assume k in ( Seg ( len D));

          then

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

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

          then ( dom (f | ( divset (D,k)))) = ( divset (D,k)) by A3, INTEGRA1: 8, RELAT_1: 62;

          then ( rng (f | ( divset (D,k)))) is non empty by RELAT_1: 42;

          then

          consider r be object such that

           A4: r in ( rng (f | ( divset (D,k))));

          reconsider r as Element of ( REAL n) by A4;

          (( vol ( divset (D,k))) * r) is Element of ( REAL n);

          hence thesis by A4;

        end;

        consider p be FinSequence of ( REAL n) such that

         A5: ( dom p) = ( Seg ( len D)) & for k be Nat st k in ( Seg ( len D)) holds P1[k, (p . k)] from FINSEQ_1:sch 5( A2);

        ( len p) = ( len D) by A5, FINSEQ_1:def 3;

        hence thesis by A5, A1;

      end;

    end

    definition

      let n be Element of NAT ;

      let A be non empty closed_interval Subset of REAL ;

      let f be Function of A, ( REAL n);

      let D be Division of A;

      let F be middle_volume of f, D;

      :: INTEGR15:def6

      func middle_sum (f,F) -> Element of ( REAL n) means

      : Def6: for i be Element of NAT st i in ( Seg n) holds ex Fi be FinSequence of REAL st Fi = (( proj (i,n)) * F) & (it . i) = ( Sum Fi);

      existence

      proof

        defpred P[ Nat, Real] means ex i be Element of NAT , Fi be FinSequence of REAL st $1 = i & Fi = (( proj (i,n)) * F) & $2 = ( Sum Fi);

        

         A1: for i be Nat st i in ( Seg n) holds ex x be Element of REAL st P[i, x]

        proof

          let i be Nat;

          assume i in ( Seg n);

          then

          reconsider ii = i as Element of NAT ;

          reconsider Fi = (( proj (ii,n)) * F) as FinSequence of REAL ;

          reconsider x = ( Sum Fi) as Element of REAL by XREAL_0:def 1;

          take x;

          thus ex ii be Element of NAT , Fi be FinSequence of REAL st i = ii & Fi = (( proj (ii,n)) * F) & x = ( Sum Fi);

        end;

        consider p be FinSequence of REAL such that

         A2: ( dom p) = ( Seg n) & for i be Nat st i in ( Seg n) holds P[i, (p . i)] from FINSEQ_1:sch 5( A1);

        take p;

        

         A3: for i be Element of NAT st i in ( Seg n) holds ex Fi be FinSequence of REAL st Fi = (( proj (i,n)) * F) & (p . i) = ( Sum Fi)

        proof

          let i be Element of NAT ;

          reconsider k = i as Nat;

          assume i in ( Seg n);

          then P[k, (p . k)] by A2;

          hence thesis;

        end;

        ( len p) = n by A2, FINSEQ_1:def 3;

        hence thesis by A3, FINSEQ_2: 92;

      end;

      uniqueness

      proof

        let x1,x2 be Element of ( REAL n) such that

         A4: (for i be Element of NAT st i in ( Seg n) holds ex Fi1 be FinSequence of REAL st Fi1 = (( proj (i,n)) * F) & (x1 . i) = ( Sum Fi1)) & for i be Element of NAT st i in ( Seg n) holds ex Fi2 be FinSequence of REAL st Fi2 = (( proj (i,n)) * F) & (x2 . i) = ( Sum Fi2);

        

         A5: for k0 be Nat st k0 in ( dom x1) holds (x1 . k0) = (x2 . k0)

        proof

          let k0 be Nat;

          assume

           A6: k0 in ( dom x1);

          then

          reconsider k = k0 as Element of NAT ;

          ( len x1) = n by CARD_1:def 7;

          then k0 in ( Seg n) by A6, FINSEQ_1:def 3;

          then (ex Fi1 be FinSequence of REAL st Fi1 = (( proj (k,n)) * F) & (x1 . k) = ( Sum Fi1)) & ex Fi2 be FinSequence of REAL st Fi2 = (( proj (k,n)) * F) & (x2 . k) = ( Sum Fi2) by A4;

          hence thesis;

        end;

        

         A7: ( len x2) = n by CARD_1:def 7;

        ( len x1) = n by CARD_1:def 7;

        

        then ( dom x1) = ( Seg n) by FINSEQ_1:def 3

        .= ( dom x2) by A7, FINSEQ_1:def 3;

        hence thesis by A5, FINSEQ_1: 13;

      end;

    end

    definition

      let n be Element of NAT ;

      let A be non empty closed_interval Subset of REAL ;

      let f be Function of A, ( REAL n);

      let T be DivSequence of A;

      :: INTEGR15:def7

      mode middle_volume_Sequence of f,T -> sequence of (( REAL n) * ) means

      : Def7: for k be Element of NAT holds (it . k) is middle_volume of f, (T . k);

      correctness

      proof

        defpred P[ Element of NAT , set] means $2 is middle_volume of f, (T . $1);

        

         A1: for x be Element of NAT holds ex y be Element of (( REAL n) * ) st P[x, y]

        proof

          let x be Element of NAT ;

          set y = the middle_volume of f, (T . x);

          reconsider y as Element of (( REAL n) * ) by FINSEQ_1:def 11;

          y is middle_volume of f, (T . x);

          hence thesis;

        end;

        ex f be sequence of (( REAL n) * ) st for x be Element of NAT holds P[x, (f . x)] from FUNCT_2:sch 3( A1);

        hence thesis;

      end;

    end

    definition

      let n be Element of NAT ;

      let A be non empty closed_interval Subset of REAL ;

      let f be Function of A, ( REAL n);

      let T be DivSequence of A;

      let S be middle_volume_Sequence of f, T;

      let k be Element of NAT ;

      :: original: .

      redefine

      func S . k -> middle_volume of f, (T . k) ;

      coherence by Def7;

    end

    definition

      let n be Element of NAT ;

      let A be non empty closed_interval Subset of REAL ;

      let f be Function of A, ( REAL n);

      let T be DivSequence of A;

      let S be middle_volume_Sequence of f, T;

      :: INTEGR15:def8

      func middle_sum (f,S) -> sequence of ( REAL-NS n) means

      : Def8: for i be Element of NAT holds (it . i) = ( middle_sum (f,(S . i)));

      existence

      proof

        deffunc H1( Element of NAT ) = ( middle_sum (f,(S . $1)));

        

         A1: ( REAL n) = the carrier of ( REAL-NS n) by REAL_NS1:def 4;

        ex IT be sequence of ( REAL n) st for i be Element of NAT holds (IT . i) = H1(i) from FUNCT_2:sch 4;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let F1,F2 be sequence of ( REAL-NS n);

        assume that

         A2: for i be Element of NAT holds (F1 . i) = ( middle_sum (f,(S . i))) and

         A3: for i be Element of NAT holds (F2 . i) = ( middle_sum (f,(S . i)));

        for i be Element of NAT holds (F1 . i) = (F2 . i)

        proof

          let i be Element of NAT ;

          

          thus (F1 . i) = ( middle_sum (f,(S . i))) by A2

          .= (F2 . i) by A3;

        end;

        hence F1 = F2 by FUNCT_2: 63;

      end;

    end

    definition

      let n be Nat;

      let Z be set;

      let f,g be PartFunc of Z, ( REAL n);

      :: INTEGR15:def9

      func f + g -> PartFunc of Z, ( REAL n) equals (f <++> g);

      coherence

      proof

        set F = (f <++> g);

        ( rng F) c= ( REAL n)

        proof

          let y be object;

          assume y in ( rng F);

          then

          consider x be object such that

           A1: x in ( dom F) and

           A2: (F . x) = y by FUNCT_1:def 3;

          ( dom F) = (( dom f) /\ ( dom g)) by VALUED_2:def 45;

          then x in ( dom f) & x in ( dom g) by A1, XBOOLE_0:def 4;

          then

           A3: (f . x) = (f /. x) & (g . x) = (g /. x) by PARTFUN1:def 6;

          ((f /. x) + (g /. x)) in ( REAL n);

          hence thesis by A2, A3, A1, VALUED_2:def 45;

        end;

        hence thesis by RELSET_1: 6;

      end;

      :: INTEGR15:def10

      func f - g -> PartFunc of Z, ( REAL n) equals (f <--> g);

      coherence

      proof

        set F = (f <--> g);

        ( rng F) c= ( REAL n)

        proof

          let y be object;

          assume y in ( rng F);

          then

          consider x be object such that

           A4: x in ( dom F) and

           A5: (F . x) = y by FUNCT_1:def 3;

          ( dom F) = (( dom f) /\ ( dom g)) by VALUED_2:def 46;

          then x in ( dom f) & x in ( dom g) by A4, XBOOLE_0:def 4;

          then

           A6: (f . x) = (f /. x) & (g . x) = (g /. x) by PARTFUN1:def 6;

          ((f /. x) - (g /. x)) in ( REAL n);

          hence thesis by A5, A6, A4, VALUED_2:def 46;

        end;

        hence thesis by RELSET_1: 6;

      end;

    end

    definition

      let n be Nat;

      let r be Real;

      let Z be set;

      let f be PartFunc of Z, ( REAL n);

      :: INTEGR15:def11

      func r (#) f -> PartFunc of Z, ( REAL n) equals (f [#] r);

      coherence

      proof

        set F = (f [#] r);

        ( rng F) c= ( REAL n)

        proof

          let y be object;

          assume y in ( rng F);

          then

          consider x be object such that

           A1: x in ( dom F) and

           A2: (F . x) = y by FUNCT_1:def 3;

          ( dom F) = ( dom f) by VALUED_2:def 39;

          then

           A3: (f . x) = (f /. x) by A1, PARTFUN1:def 6;

          (r * (f /. x)) in ( REAL n);

          hence thesis by A2, A3, A1, VALUED_2:def 39;

        end;

        hence thesis by RELSET_1: 6;

      end;

    end

    begin

    definition

      let n be Element of NAT ;

      let A be non empty closed_interval Subset of REAL ;

      let f be Function of A, ( REAL n);

      :: INTEGR15:def12

      attr f is bounded means for i be Element of NAT st i in ( Seg n) holds (( proj (i,n)) * f) is bounded;

    end

    

     Lm6: for n,i be Element of NAT , f be PartFunc of REAL , ( REAL n), i be Element of NAT , A be Subset of REAL holds (( proj (i,n)) * (f | A)) = ((( proj (i,n)) * f) | A)

    proof

      let n,i be Element of NAT , f be PartFunc of REAL , ( REAL n), i be Element of NAT , A be Subset of REAL ;

      

       A1: ( dom ( proj (i,n))) = ( REAL n) by FUNCT_2:def 1;

      then

       A2: ( rng f) c= ( dom ( proj (i,n)));

      

       A3: ( rng (f | A)) c= ( dom ( proj (i,n))) by A1;

       A4:

      now

        let c be object;

        assume

         A5: c in ( dom ((( proj (i,n)) * f) | A));

        then

         A6: c in (( dom (( proj (i,n)) * f)) /\ A) by RELAT_1: 61;

        then

         A7: c in A by XBOOLE_0:def 4;

        

         A8: c in ( dom (( proj (i,n)) * f)) by A6, XBOOLE_0:def 4;

        then c in ( dom f) by A2, RELAT_1: 27;

        then c in (( dom f) /\ A) by A7, XBOOLE_0:def 4;

        then

         A9: c in ( dom (f | A)) by RELAT_1: 61;

        then c in ( dom (( proj (i,n)) * (f | A))) by A3, RELAT_1: 27;

        

        then ((( proj (i,n)) * (f | A)) . c) = (( proj (i,n)) . ((f | A) . c)) by FUNCT_1: 12

        .= (( proj (i,n)) . (f . c)) by A9, FUNCT_1: 47

        .= ((( proj (i,n)) * f) . c) by A8, FUNCT_1: 12;

        hence (((( proj (i,n)) * f) | A) . c) = ((( proj (i,n)) * (f | A)) . c) by A5, FUNCT_1: 47;

      end;

      ( dom ((( proj (i,n)) * f) | A)) = (( dom (( proj (i,n)) * f)) /\ A) by RELAT_1: 61

      .= (( dom f) /\ A) by A2, RELAT_1: 27

      .= ( dom (f | A)) by RELAT_1: 61

      .= ( dom (( proj (i,n)) * (f | A))) by A3, RELAT_1: 27;

      hence thesis by A4, FUNCT_1: 2;

    end;

    definition

      let n be Element of NAT ;

      let A be non empty closed_interval Subset of REAL ;

      let f be Function of A, ( REAL n);

      :: INTEGR15:def13

      attr f is integrable means for i be Element of NAT st i in ( Seg n) holds (( proj (i,n)) * f) is integrable;

    end

    definition

      let n be Element of NAT ;

      let A be non empty closed_interval Subset of REAL ;

      let f be Function of A, ( REAL n);

      :: INTEGR15:def14

      func integral (f) -> Element of ( REAL n) means

      : Def14: ( dom it ) = ( Seg n) & for i be Element of NAT st i in ( Seg n) holds (it . i) = ( integral (( proj (i,n)) * f));

      existence

      proof

        defpred P[ Nat, Real] means ex i be Element of NAT st $1 = i & $2 = ( integral (( proj (i,n)) * f));

        

         A1: for i be Nat st i in ( Seg n) holds ex x be Element of REAL st P[i, x]

        proof

          let i be Nat;

          assume i in ( Seg n);

          then

          reconsider ii = i as Element of NAT ;

          reconsider x = ( integral (( proj (ii,n)) * f)) as Element of REAL by XREAL_0:def 1;

          take x;

          thus thesis;

        end;

        consider p be FinSequence of REAL such that

         A2: ( dom p) = ( Seg n) & for i be Nat st i in ( Seg n) holds P[i, (p . i)] from FINSEQ_1:sch 5( A1);

        take p;

        

         A3: for i be Element of NAT st i in ( Seg n) holds (p . i) = ( integral (( proj (i,n)) * f))

        proof

          let i be Element of NAT ;

          assume i in ( Seg n);

          then P[i, (p . i)] by A2;

          hence thesis;

        end;

        ( len p) = n by A2, FINSEQ_1:def 3;

        hence thesis by A2, A3, FINSEQ_2: 92;

      end;

      uniqueness

      proof

        let x1,x2 be Element of ( REAL n) such that

         A4: ( dom x1) = ( Seg n) and

         A5: for i be Element of NAT st i in ( Seg n) holds (x1 . i) = ( integral (( proj (i,n)) * f)) and

         A6: ( dom x2) = ( Seg n) and

         A7: for i be Element of NAT st i in ( Seg n) holds (x2 . i) = ( integral (( proj (i,n)) * f));

        now

          let k be Nat;

          assume

           A8: k in ( dom x1);

          then

          reconsider i = k as Element of NAT ;

          (x1 . i) = ( integral (( proj (i,n)) * f)) by A4, A5, A8

          .= (x2 . i) by A4, A7, A8;

          hence (x1 . k) = (x2 . k);

        end;

        hence thesis by A4, A6, FINSEQ_1: 13;

      end;

    end

    theorem :: INTEGR15:11

    

     Th11: for n be Element of NAT , A be non empty closed_interval Subset of REAL , f be Function of A, ( REAL n), T be DivSequence of A, S be middle_volume_Sequence of f, T st f is bounded & f is integrable & ( delta T) is convergent & ( lim ( delta T)) = 0 holds ( middle_sum (f,S)) is convergent & ( lim ( middle_sum (f,S))) = ( integral f)

    proof

      let n be Element of NAT , A be non empty closed_interval Subset of REAL , f be Function of A, ( REAL n), T be DivSequence of A, S be middle_volume_Sequence of f, T;

      assume that

       A1: f is bounded & f is integrable and

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

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

      set xs = ( integral f);

      ( REAL n) = the carrier of ( REAL-NS n) by REAL_NS1:def 4;

      then

      reconsider xseq = seq as sequence of ( REAL n);

      

       A3: for i be Nat st i in ( Seg n) holds ex rseqi be Real_Sequence st for k be Nat holds (rseqi . k) = ((xseq . k) . i) & rseqi is convergent & (xs . i) = ( lim rseqi)

      proof

        let i be Nat;

        reconsider pjinf = (( proj (i,n)) * f) as Function of A, REAL ;

        defpred P[ Element of NAT , set] means $2 = (( proj (i,n)) * (S . $1));

        

         A4: for x be Element of NAT holds ex y be Element of ( REAL * ) st P[x, y]

        proof

          let x be Element of NAT ;

          (( proj (i,n)) * (S . x)) is Element of ( REAL * ) by FINSEQ_1:def 11;

          hence thesis;

        end;

        consider F be sequence of ( REAL * ) such that

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

        

         A6: for x be Element of NAT holds (( proj (i,n)) * (S . x)) is FinSequence of REAL & ( dom (( proj (i,n)) * (S . x))) = ( Seg ( len (S . x))) & ( rng (( proj (i,n)) * (S . x))) c= REAL

        proof

          let x be Element of NAT ;

          ( dom ( proj (i,n))) = ( REAL n) by FUNCT_2:def 1;

          then ( rng (S . x)) c= ( dom ( proj (i,n)));

          

          then ( dom (( proj (i,n)) * (S . x))) = ( dom (S . x)) by RELAT_1: 27

          .= ( Seg ( len (S . x))) by FINSEQ_1:def 3;

          hence thesis;

        end;

        for k be Element of NAT holds (F . k) is middle_volume of pjinf, (T . k)

        proof

          let k be Element of NAT ;

          reconsider Tk = (T . k) as FinSequence;

          reconsider Fk = (F . k) as FinSequence of REAL ;

          

           A7: (F . k) = (( proj (i,n)) * (S . k)) by A5;

          

          then

           A8: ( dom Fk) = ( Seg ( len (S . k))) by A6

          .= ( Seg ( len Tk)) by Def5;

          then

           A9: ( dom Fk) = ( dom Tk) by FINSEQ_1:def 3;

           A10:

          now

            let j be Nat;

            ( dom ( proj (i,n))) = ( REAL n) by FUNCT_2:def 1;

            then

             A11: ( rng f) c= ( dom ( proj (i,n)));

            assume

             A12: j in ( dom Tk);

            then

            consider r be Element of ( REAL n) such that

             A13: r in ( rng (f | ( divset ((T . k),j)))) and

             A14: ((S . k) . j) = (( vol ( divset ((T . k),j))) * r) by Def5;

            reconsider v = (( proj (i,n)) . r) as Element of REAL ;

            take v;

            consider t be object such that

             A15: t in ( dom (f | ( divset ((T . k),j)))) and

             A16: r = ((f | ( divset ((T . k),j))) . t) by A13, FUNCT_1:def 3;

            t in (( dom f) /\ ( divset ((T . k),j))) by A15, RELAT_1: 61;

            then t in ( dom f) by XBOOLE_0:def 4;

            then

             A17: t in ( dom (( proj (i,n)) * f)) by A11, RELAT_1: 27;

            

             A18: ( dom (f | ( divset ((T . k),j)))) = (( dom f) /\ ( divset ((T . k),j))) by RELAT_1: 61

            .= (( dom pjinf) /\ ( divset ((T . k),j))) by A11, RELAT_1: 27

            .= ( dom (pjinf | ( divset ((T . k),j)))) by RELAT_1: 61;

            (( proj (i,n)) . r) = (( proj (i,n)) . (f . t)) by A15, A16, FUNCT_1: 47

            .= ((( proj (i,n)) * f) . t) by A17, FUNCT_1: 12

            .= ((pjinf | ( divset ((T . k),j))) . t) by A15, A18, FUNCT_1: 47;

            hence v in ( rng (pjinf | ( divset ((T . k),j)))) by A15, A18, FUNCT_1: 3;

            

            thus (Fk . j) = (( proj (i,n)) . ((S . k) . j)) by A7, A9, A12, FUNCT_1: 12

            .= ((( vol ( divset ((T . k),j))) * r) . i) by A14, PDIFF_1:def 1

            .= (( vol ( divset ((T . k),j))) * (r . i)) by RVSUM_1: 44

            .= (v * ( vol ( divset ((T . k),j)))) by PDIFF_1:def 1;

          end;

          ( len Fk) = ( len Tk) by A8, FINSEQ_1:def 3;

          hence thesis by A10, Def1;

        end;

        then

        reconsider pjis = F as middle_volume_Sequence of pjinf, T by Def3;

        reconsider rseqi = ( middle_sum (pjinf,pjis)) as Real_Sequence;

        assume

         A19: i in ( Seg n);

        

         A20: for k be Nat holds (rseqi . k) = ((xseq . k) . i)

        proof

          let k be Nat;

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

          

           A21: ex Fi be FinSequence of REAL st Fi = (( proj (i,n)) * (S . k)) & (( middle_sum (f,(S . k))) . i) = ( Sum Fi) by A19, Def6;

          (rseqi . k) = ( middle_sum (pjinf,(pjis . k))) by Def4

          .= (( middle_sum (f,(S . k))) . i) by A5, A21

          .= ((xseq . k) . i) by Def8;

          hence thesis;

        end;

        take rseqi;

        

         A22: (( proj (i,n)) * f) is bounded & pjinf is integrable by A1, A19;

        then ( lim ( middle_sum (pjinf,pjis))) = ( integral pjinf) by A2, Th9;

        hence thesis by A2, A19, A22, A20, Def14, Th9;

      end;

      reconsider x = xs as Point of ( REAL-NS n) by REAL_NS1:def 4;

      xs = x;

      hence thesis by A3, REAL_NS1: 11;

    end;

    theorem :: INTEGR15:12

    for n be Element of NAT , A be non empty closed_interval Subset of REAL , f be Function of A, ( REAL n) st f is bounded holds f is integrable iff ex I be Element of ( REAL n) st 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 n be Element of NAT , A be non empty closed_interval Subset of REAL , f be Function of A, ( REAL n);

      assume

       A1: f is bounded;

      hereby

        reconsider I = ( integral f) as Element of ( REAL n);

        assume

         A2: f is integrable;

        take I;

        thus 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 by A1, A2, Th11;

      end;

      now

        assume ex I be Element of ( REAL n) st 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;

        then

        consider I be Element of ( REAL n) such that

         A3: 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;

        now

          let i be Element of NAT ;

          reconsider Ii = (I . i) as Element of REAL by XREAL_0:def 1;

          assume

           A4: i in ( Seg n);

           A5:

          now

            set x = I;

            let T be DivSequence of A, Si be middle_volume_Sequence of (( proj (i,n)) * f), T;

            defpred P[ Element of NAT , set] means ex H be FinSequence, z be FinSequence st H = (T . $1) & z = $2 & ( len z) = ( len H) & for j be Element of NAT st j in ( dom H) holds ex rji be Element of ( REAL n), tji be Element of REAL st tji in ( dom (f | ( divset ((T . $1),j)))) & ((Si . $1) . j) = (( vol ( divset ((T . $1),j))) * (((( proj (i,n)) * f) | ( divset ((T . $1),j))) . tji)) & rji = ((f | ( divset ((T . $1),j))) . tji) & (z . j) = (( vol ( divset ((T . $1),j))) * rji);

            reconsider xs = x as Element of ( REAL n);

            

             A6: for k be Element of NAT holds ex y be Element of (( REAL n) * ) st P[k, y]

            proof

              let k be Element of NAT ;

              reconsider Tk = (T . k) as FinSequence;

              defpred P1[ Nat, set] means ex j be Element of NAT st $1 = j & ex rji be Element of ( REAL n), tji be Element of REAL st tji in ( dom (f | ( divset ((T . k),j)))) & ((Si . k) . j) = (( vol ( divset ((T . k),j))) * (((( proj (i,n)) * f) | ( divset ((T . k),j))) . tji)) & rji = ((f | ( divset ((T . k),j))) . tji) & $2 = (( vol ( divset ((T . k),j))) * rji);

              

               A7: for j be Nat st j in ( Seg ( len Tk)) holds ex x be Element of ( REAL n) st P1[j, x]

              proof

                ( dom ( proj (i,n))) = ( REAL n) by FUNCT_2:def 1;

                then

                 A8: ( rng f) c= ( dom ( proj (i,n)));

                let j0 be Nat;

                assume

                 A9: j0 in ( Seg ( len Tk));

                then

                reconsider j = j0 as Element of NAT ;

                j in ( dom Tk) by A9, FINSEQ_1:def 3;

                then

                consider r be Element of REAL such that

                 A10: r in ( rng ((( proj (i,n)) * f) | ( divset ((T . k),j)))) and

                 A11: ((Si . k) . j) = (r * ( vol ( divset ((T . k),j)))) by Def1;

                consider tji be object such that

                 A12: tji in ( dom ((( proj (i,n)) * f) | ( divset ((T . k),j)))) and

                 A13: r = (((( proj (i,n)) * f) | ( divset ((T . k),j))) . tji) by A10, FUNCT_1:def 3;

                tji in (( dom (( proj (i,n)) * f)) /\ ( divset ((T . k),j))) by A12, RELAT_1: 61;

                then

                reconsider tji as Element of REAL ;

                

                 A14: ( dom (f | ( divset ((T . k),j)))) = (( dom f) /\ ( divset ((T . k),j))) by RELAT_1: 61

                .= (( dom (( proj (i,n)) * f)) /\ ( divset ((T . k),j))) by A8, RELAT_1: 27

                .= ( dom ((( proj (i,n)) * f) | ( divset ((T . k),j)))) by RELAT_1: 61;

                then ((f | ( divset ((T . k),j))) . tji) in ( rng (f | ( divset ((T . k),j)))) by A12, FUNCT_1: 3;

                then

                reconsider rji = ((f | ( divset ((T . k),j))) . tji) as Element of ( REAL n);

                reconsider x = (( vol ( divset ((T . k),j))) * rji) as Element of ( REAL n);

                take x;

                thus P1[j0, x] by A11, A12, A13, A14;

              end;

              consider p be FinSequence of ( REAL n) such that

               A15: ( dom p) = ( Seg ( len Tk)) & for j be Nat st j in ( Seg ( len Tk)) holds P1[j, (p . j)] from FINSEQ_1:sch 5( A7);

              reconsider x = p as Element of (( REAL n) * ) by FINSEQ_1:def 11;

              take x;

               A16:

              now

                let jj0 be Element of NAT ;

                reconsider j0 = jj0 as Nat;

                

                 A17: ( dom Tk) = ( Seg ( len Tk)) by FINSEQ_1:def 3;

                assume jj0 in ( dom Tk);

                then P1[j0, (p . j0)] by A15, A17;

                hence ex rji be Element of ( REAL n), tji be Element of REAL st tji in ( dom (f | ( divset ((T . k),jj0)))) & ((Si . k) . jj0) = (( vol ( divset ((T . k),jj0))) * (((( proj (i,n)) * f) | ( divset ((T . k),jj0))) . tji)) & rji = ((f | ( divset ((T . k),jj0))) . tji) & (p . jj0) = (( vol ( divset ((T . k),jj0))) * rji);

              end;

              ( len p) = ( len Tk) by A15, FINSEQ_1:def 3;

              hence P[k, x] by A16;

            end;

            consider S be sequence of (( REAL n) * ) such that

             A18: for x be Element of NAT holds P[x, (S . x)] from FUNCT_2:sch 3( A6);

            for k be Element of NAT holds (S . k) is middle_volume of f, (T . k)

            proof

              let k be Element of NAT ;

              consider H be FinSequence, z be FinSequence such that

               A19: H = (T . k) & z = (S . k) & ( len H) = ( len z) and

               A20: for j be Element of NAT st j in ( dom H) holds ex rji be Element of ( REAL n), tji be Element of REAL st tji in ( dom (f | ( divset ((T . k),j)))) & ((Si . k) . j) = (( vol ( divset ((T . k),j))) * (((( proj (i,n)) * f) | ( divset ((T . k),j))) . tji)) & rji = ((f | ( divset ((T . k),j))) . tji) & (z . j) = (( vol ( divset ((T . k),j))) * rji) by A18;

               A21:

              now

                let x be Nat;

                assume

                 A22: x in ( dom H);

                then

                reconsider j = x as Element of NAT ;

                consider rji be Element of ( REAL n), tji be Element of REAL such that

                 A23: tji in ( dom (f | ( divset ((T . k),j)))) and ((Si . k) . j) = (( vol ( divset ((T . k),j))) * (((( proj (i,n)) * f) | ( divset ((T . k),j))) . tji)) and

                 A24: rji = ((f | ( divset ((T . k),j))) . tji) and

                 A25: (z . j) = (( vol ( divset ((T . k),j))) * rji) by A20, A22;

                take rji;

                thus rji in ( rng (f | ( divset ((T . k),x)))) by A23, A24, FUNCT_1: 3;

                thus (z . x) = (( vol ( divset ((T . k),x))) * rji) by A25;

              end;

              thus thesis by A19, A21, Def5;

            end;

            then

            reconsider S as middle_volume_Sequence of f, T by Def7;

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

            ( REAL n) = the carrier of ( REAL-NS n) by REAL_NS1:def 4;

            then

            reconsider xseq = seq as sequence of ( REAL n);

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

            then seq is convergent & ( lim seq) = x by A3;

            then

            consider rseqi be Real_Sequence such that

             A26: for k be Nat holds (rseqi . k) = ((xseq . k) . i) & rseqi is convergent & (xs . i) = ( lim rseqi) by A4, REAL_NS1: 11;

            for k be Element of NAT holds (rseqi . k) = (( middle_sum ((( proj (i,n)) * f),Si)) . k)

            proof

              let k be Element of NAT ;

              consider H be FinSequence, z be FinSequence such that

               A27: H = (T . k) and

               A28: z = (S . k) and

               A29: ( len H) = ( len z) and

               A30: for j be Element of NAT st j in ( dom H) holds ex rji be Element of ( REAL n), tji be Element of REAL st tji in ( dom (f | ( divset ((T . k),j)))) & ((Si . k) . j) = (( vol ( divset ((T . k),j))) * (((( proj (i,n)) * f) | ( divset ((T . k),j))) . tji)) & rji = ((f | ( divset ((T . k),j))) . tji) & (z . j) = (( vol ( divset ((T . k),j))) * rji) by A18;

              ( dom ( proj (i,n))) = ( REAL n) by FUNCT_2:def 1;

              then ( rng (S . k)) c= ( dom ( proj (i,n)));

              

              then

               A31: ( dom (( proj (i,n)) * (S . k))) = ( dom (S . k)) by RELAT_1: 27

              .= ( Seg ( len H)) by A28, A29, FINSEQ_1:def 3

              .= ( Seg ( len (Si . k))) by A27, Def1

              .= ( dom (Si . k)) by FINSEQ_1:def 3;

              

               A32: for j be Nat st j in ( dom (( proj (i,n)) * (S . k))) holds ((( proj (i,n)) * (S . k)) . j) = ((Si . k) . j)

              proof

                let j0 be Nat;

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

                ( dom ( proj (i,n))) = ( REAL n) by FUNCT_2:def 1;

                then

                 A33: ( rng f) c= ( dom ( proj (i,n)));

                assume

                 A34: j0 in ( dom (( proj (i,n)) * (S . k)));

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

                then j0 in ( Seg ( len H)) by A27, Def1;

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

                then

                consider rji be Element of ( REAL n), tji be Element of REAL such that

                 A35: tji in ( dom (f | ( divset ((T . k),j)))) and

                 A36: ((Si . k) . j) = (( vol ( divset ((T . k),j))) * (((( proj (i,n)) * f) | ( divset ((T . k),j))) . tji)) and

                 A37: rji = ((f | ( divset ((T . k),j))) . tji) and

                 A38: (z . j) = (( vol ( divset ((T . k),j))) * rji) by A30;

                

                 A39: ( dom (f | ( divset ((T . k),j)))) = (( dom f) /\ ( divset ((T . k),j))) by RELAT_1: 61

                .= (( dom (( proj (i,n)) * f)) /\ ( divset ((T . k),j))) by A33, RELAT_1: 27

                .= ( dom ((( proj (i,n)) * f) | ( divset ((T . k),j)))) by RELAT_1: 61;

                then tji in (( dom (( proj (i,n)) * f)) /\ ( divset ((T . k),j))) by A35, RELAT_1: 61;

                then

                 A40: tji in ( dom (( proj (i,n)) * f)) by XBOOLE_0:def 4;

                

                 A41: (((( proj (i,n)) * f) | ( divset ((T . k),j))) . tji) = ((( proj (i,n)) * f) . tji) by A35, A39, FUNCT_1: 47

                .= (( proj (i,n)) . (f . tji)) by A40, FUNCT_1: 12

                .= (( proj (i,n)) . rji) by A35, A37, FUNCT_1: 47;

                ((( proj (i,n)) * (S . k)) . j) = (( proj (i,n)) . ((S . k) . j)) by A34, FUNCT_1: 12

                .= ((( vol ( divset ((T . k),j))) * rji) . i) by A28, A38, PDIFF_1:def 1

                .= (( vol ( divset ((T . k),j))) * (rji . i)) by RVSUM_1: 44

                .= ((Si . k) . j) by A36, A41, PDIFF_1:def 1;

                hence thesis;

              end;

              consider Fi be FinSequence of REAL such that

               A42: Fi = (( proj (i,n)) * (S . k)) and

               A43: (( middle_sum (f,(S . k))) . i) = ( Sum Fi) by A4, Def6;

              

              thus (rseqi . k) = ((xseq . k) . i) by A26

              .= ( Sum Fi) by A43, Def8

              .= ( middle_sum ((( proj (i,n)) * f),(Si . k))) by A31, A32, A42, FINSEQ_1: 13

              .= (( middle_sum ((( proj (i,n)) * f),Si)) . k) by Def4;

            end;

            hence ( middle_sum ((( proj (i,n)) * f),Si)) is convergent & ( lim ( middle_sum ((( proj (i,n)) * f),Si))) = Ii by A26, FUNCT_2: 63;

          end;

          (( proj (i,n)) * f) is bounded by A1, A4;

          hence (( proj (i,n)) * f) is integrable by A5, Th10;

        end;

        hence f is integrable;

      end;

      hence thesis;

    end;

    definition

      let n be Element of NAT ;

      let f be PartFunc of REAL , ( REAL n);

      :: INTEGR15:def15

      attr f is bounded means for i be Element of NAT st i in ( Seg n) holds (( proj (i,n)) * f) is bounded;

    end

    definition

      let n be Element of NAT ;

      let A be non empty closed_interval Subset of REAL ;

      let f be PartFunc of REAL , ( REAL n);

      :: INTEGR15:def16

      pred f is_integrable_on A means for i be Element of NAT st i in ( Seg n) holds (( proj (i,n)) * f) is_integrable_on A;

    end

    definition

      let n be Element of NAT ;

      let A be non empty closed_interval Subset of REAL ;

      let f be PartFunc of REAL , ( REAL n);

      :: INTEGR15:def17

      func integral (f,A) -> Element of ( REAL n) means

      : Def17: ( dom it ) = ( Seg n) & for i be Element of NAT st i in ( Seg n) holds (it . i) = ( integral ((( proj (i,n)) * f),A));

      existence

      proof

        defpred P[ Nat, Real] means ex i be Element of NAT st $1 = i & $2 = ( integral ((( proj (i,n)) * f),A));

        

         A1: for i be Nat st i in ( Seg n) holds ex x be Element of REAL st P[i, x]

        proof

          let i be Nat;

          assume i in ( Seg n);

          then

          reconsider ii = i as Element of NAT ;

          reconsider x = ( integral ((( proj (ii,n)) * f),A)) as Element of REAL by XREAL_0:def 1;

          take x;

          thus thesis;

        end;

        consider p be FinSequence of REAL such that

         A2: ( dom p) = ( Seg n) & for i be Nat st i in ( Seg n) holds P[i, (p . i)] from FINSEQ_1:sch 5( A1);

        take p;

        

         A3: for i be Element of NAT st i in ( Seg n) holds (p . i) = ( integral ((( proj (i,n)) * f),A))

        proof

          let i be Element of NAT ;

          assume i in ( Seg n);

          then P[i, (p . i)] by A2;

          hence thesis;

        end;

        ( len p) = n by A2, FINSEQ_1:def 3;

        hence thesis by A2, A3, FINSEQ_2: 92;

      end;

      uniqueness

      proof

        let x1,x2 be Element of ( REAL n) such that

         A4: ( dom x1) = ( Seg n) and

         A5: for i be Element of NAT st i in ( Seg n) holds (x1 . i) = ( integral ((( proj (i,n)) * f),A)) and

         A6: ( dom x2) = ( Seg n) and

         A7: for i be Element of NAT st i in ( Seg n) holds (x2 . i) = ( integral ((( proj (i,n)) * f),A));

        for k be Nat st k in ( dom x1) holds (x1 . k) = (x2 . k)

        proof

          let k be Nat;

          assume

           A8: k in ( dom x1);

          then

          reconsider k as Element of NAT ;

          (x2 . k) = ( integral ((( proj (k,n)) * f),A)) by A4, A7, A8;

          hence thesis by A4, A5, A8;

        end;

        hence thesis by A4, A6, FINSEQ_1: 13;

      end;

    end

    theorem :: INTEGR15:13

    for n be Element of NAT , A be non empty closed_interval Subset of REAL , f be PartFunc of REAL , ( REAL n), g be Function of A, ( REAL n) st (f | A) = g holds f is_integrable_on A iff g is integrable

    proof

      let n be Element of NAT , A be non empty closed_interval Subset of REAL , f be PartFunc of REAL , ( REAL n), g be Function of A, ( REAL n);

      assume

       A1: (f | A) = g;

      thus f is_integrable_on A implies g is integrable

      proof

        assume

         A2: f is_integrable_on A;

        for i be Element of NAT st i in ( Seg n) holds (( proj (i,n)) * g) is integrable

        proof

          let i be Element of NAT ;

          ( dom ( proj (i,n))) = ( REAL n) by FUNCT_2:def 1;

          then ( rng f) c= ( dom ( proj (i,n)));

          then

           A3: ( dom (( proj (i,n)) * f)) = ( dom f) by RELAT_1: 27;

          A = ( dom g) by FUNCT_2:def 1

          .= (( dom f) /\ A) by A1, RELAT_1: 61;

          then ((( proj (i,n)) * f) || A) is total by A3, INTEGRA5: 6, XBOOLE_1: 17;

          then

          reconsider F = ((( proj (i,n)) * f) | A) as Function of A, REAL ;

          assume i in ( Seg n);

          then (( proj (i,n)) * f) is_integrable_on A by A2;

          then F is integrable;

          hence thesis by A1, Lm6;

        end;

        hence thesis;

      end;

      assume

       A4: g is integrable;

      for i be Element of NAT st i in ( Seg n) holds (( proj (i,n)) * f) is_integrable_on A

      proof

        let i be Element of NAT ;

        assume

         A5: i in ( Seg n);

        (( proj (i,n)) * g) = ((( proj (i,n)) * f) | A) by A1, Lm6;

        then ((( proj (i,n)) * f) || A) is integrable by A4, A5;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: INTEGR15:14

    for n be Element of NAT , A be non empty closed_interval Subset of REAL , f be PartFunc of REAL , ( REAL n), g be Function of A, ( REAL n) st (f | A) = g holds ( integral (f,A)) = ( integral g)

    proof

      let n be Element of NAT , A be non empty closed_interval Subset of REAL , f be PartFunc of REAL , ( REAL n), g be Function of A, ( REAL n);

      assume

       A1: (f | A) = g;

       A2:

      now

        let k be Nat;

        assume

         A3: k in ( dom ( integral (f,A)));

        then

        reconsider i = k as Element of NAT ;

        ( dom ( proj (i,n))) = ( REAL n) by FUNCT_2:def 1;

        then ( rng f) c= ( dom ( proj (i,n)));

        then

         A4: ( dom (( proj (i,n)) * f)) = ( dom f) by RELAT_1: 27;

        A = ( dom g) by FUNCT_2:def 1

        .= (( dom f) /\ A) by A1, RELAT_1: 61;

        then ((( proj (i,n)) * f) || A) is total by A4, INTEGRA5: 6, XBOOLE_1: 17;

        then

        reconsider F = ((( proj (i,n)) * f) | A) as Function of A, REAL ;

        

         A5: F = (( proj (i,n)) * g) by A1, Lm6;

        

         A6: i in ( Seg n) by A3, Def17;

        

        then (( integral (f,A)) . i) = ( integral ((( proj (i,n)) * f),A)) by Def17

        .= ( integral ((( proj (i,n)) * f) || A));

        hence (( integral (f,A)) . k) = (( integral g) . k) by A6, A5, Def14;

      end;

      ( dom ( integral (f,A))) = ( Seg n) by Def17

      .= ( dom ( integral g)) by Def14;

      hence thesis by A2, FINSEQ_1: 13;

    end;

    definition

      let a,b be Real;

      let n be Element of NAT ;

      let f be PartFunc of REAL , ( REAL n);

      :: INTEGR15:def18

      func integral (f,a,b) -> Element of ( REAL n) means

      : Def18: ( dom it ) = ( Seg n) & for i be Element of NAT st i in ( Seg n) holds (it . i) = ( integral ((( proj (i,n)) * f),a,b));

      existence

      proof

        defpred P[ Nat, Real] means ex i be Element of NAT st $1 = i & $2 = ( integral ((( proj (i,n)) * f),a,b));

        

         A1: for i be Nat st i in ( Seg n) holds ex x be Element of REAL st P[i, x]

        proof

          let i be Nat;

          assume i in ( Seg n);

          then

          reconsider ii = i as Element of NAT ;

          reconsider x = ( integral ((( proj (ii,n)) * f),a,b)) as Element of REAL by XREAL_0:def 1;

          take x;

          thus thesis;

        end;

        consider p be FinSequence of REAL such that

         A2: ( dom p) = ( Seg n) & for i be Nat st i in ( Seg n) holds P[i, (p . i)] from FINSEQ_1:sch 5( A1);

        take p;

        

         A3: for i be Element of NAT st i in ( Seg n) holds (p . i) = ( integral ((( proj (i,n)) * f),a,b))

        proof

          let i be Element of NAT ;

          assume i in ( Seg n);

          then P[i, (p . i)] by A2;

          hence thesis;

        end;

        ( len p) = n by A2, FINSEQ_1:def 3;

        hence thesis by A2, A3, FINSEQ_2: 92;

      end;

      uniqueness

      proof

        let x1,x2 be Element of ( REAL n) such that

         A4: ( dom x1) = ( Seg n) and

         A5: for i be Element of NAT st i in ( Seg n) holds (x1 . i) = ( integral ((( proj (i,n)) * f),a,b)) and

         A6: ( dom x2) = ( Seg n) and

         A7: for i be Element of NAT st i in ( Seg n) holds (x2 . i) = ( integral ((( proj (i,n)) * f),a,b));

        for k be Nat st k in ( dom x1) holds (x1 . k) = (x2 . k)

        proof

          let k be Nat;

          assume

           A8: k in ( dom x1);

          then

          reconsider k as Element of NAT ;

          (x2 . k) = ( integral ((( proj (k,n)) * f),a,b)) by A4, A7, A8;

          hence thesis by A4, A5, A8;

        end;

        hence thesis by A4, A6, FINSEQ_1: 13;

      end;

    end

    begin

    theorem :: INTEGR15:15

    

     Th15: for n,i be Element of NAT , f1,f2 be PartFunc of Z, ( REAL n) holds (( proj (i,n)) * (f1 + f2)) = ((( proj (i,n)) * f1) + (( proj (i,n)) * f2)) & (( proj (i,n)) * (f1 - f2)) = ((( proj (i,n)) * f1) - (( proj (i,n)) * f2))

    proof

      let n,i be Element of NAT ;

      let f1,f2 be PartFunc of Z, ( REAL n);

      

       A1: ( dom ( proj (i,n))) = ( REAL n) by FUNCT_2:def 1;

      then ( rng f1) c= ( dom ( proj (i,n)));

      then

       A2: ( dom (( proj (i,n)) * f1)) = ( dom f1) by RELAT_1: 27;

      

       A3: ( rng (f1 + f2)) c= ( dom ( proj (i,n))) by A1;

      then

       A4: ( dom (( proj (i,n)) * (f1 + f2))) = ( dom (f1 + f2)) by RELAT_1: 27;

      ( rng f2) c= ( dom ( proj (i,n))) by A1;

      then

       A5: ( dom (( proj (i,n)) * f2)) = ( dom f2) by RELAT_1: 27;

      

       A6: ( dom (f1 + f2)) = (( dom f1) /\ ( dom f2)) by VALUED_2:def 45;

      

       A7: for z be Element of Z st z in ( dom (( proj (i,n)) * (f1 + f2))) holds ((( proj (i,n)) * (f1 + f2)) . z) = (((( proj (i,n)) * f1) + (( proj (i,n)) * f2)) . z)

      proof

        let z be Element of Z;

        reconsider f1z = (f1 /. z) as Element of (n -tuples_on REAL );

        reconsider f2z = (f2 /. z) as Element of (n -tuples_on REAL );

        assume

         A8: z in ( dom (( proj (i,n)) * (f1 + f2)));

        then

         A9: z in ( dom (f1 + f2)) by A3, RELAT_1: 27;

        then

         A10: z in (( dom f1) /\ ( dom f2)) by VALUED_2:def 45;

        then z in ( dom f1) by XBOOLE_0:def 4;

        then

         A11: (f1 . z) = f1z by PARTFUN1:def 6;

        z in ( dom f2) by A10, XBOOLE_0:def 4;

        then

         A12: (f2 . z) = f2z by PARTFUN1:def 6;

        (( proj (i,n)) . ((f1 + f2) . z)) = (( proj (i,n)) . ((f1 . z) + (f2 . z))) by A9, VALUED_2:def 45;

        then (( proj (i,n)) . ((f1 + f2) . z)) = (((f1 /. z) + (f2 /. z)) . i) by A11, A12, PDIFF_1:def 1;

        then

         A13: (( proj (i,n)) . ((f1 + f2) . z)) = ((f1z . i) + (f2z . i)) by RVSUM_1: 11;

        

         A14: z in (( dom (( proj (i,n)) * f1)) /\ ( dom (( proj (i,n)) * f2))) by A2, A5, A4, A8, VALUED_2:def 45;

        then z in ( dom (( proj (i,n)) * f1)) by XBOOLE_0:def 4;

        then ((( proj (i,n)) * f1) . z) = (( proj (i,n)) . (f1 . z)) by FUNCT_1: 12;

        then

         A15: ((( proj (i,n)) * f1) . z) = (f1z . i) by A11, PDIFF_1:def 1;

        z in ( dom (( proj (i,n)) * f2)) by A14, XBOOLE_0:def 4;

        then ((( proj (i,n)) * f2) . z) = (( proj (i,n)) . (f2 . z)) by FUNCT_1: 12;

        then

         A16: ((( proj (i,n)) * f2) . z) = (f2z . i) by A12, PDIFF_1:def 1;

        z in ( dom ((( proj (i,n)) * f1) + (( proj (i,n)) * f2))) by A6, A2, A5, A4, A8, VALUED_1:def 1;

        then (((( proj (i,n)) * f1) + (( proj (i,n)) * f2)) . z) = ((f1z . i) + (f2z . i)) by A15, A16, VALUED_1:def 1;

        hence thesis by A8, A13, FUNCT_1: 12;

      end;

      ( dom (( proj (i,n)) * (f1 + f2))) = ( dom ((( proj (i,n)) * f1) + (( proj (i,n)) * f2))) by A6, A2, A5, A4, VALUED_1:def 1;

      hence (( proj (i,n)) * (f1 + f2)) = ((( proj (i,n)) * f1) + (( proj (i,n)) * f2)) by A7, PARTFUN1: 5;

      

       A17: ( rng (f1 - f2)) c= ( dom ( proj (i,n))) by A1;

      then

       A18: ( dom (( proj (i,n)) * (f1 - f2))) = ( dom (f1 - f2)) by RELAT_1: 27;

      

       A19: ( dom (f1 - f2)) = (( dom f1) /\ ( dom f2)) by VALUED_2:def 46;

      then

       A20: ( dom (( proj (i,n)) * (f1 - f2))) = ( dom ((( proj (i,n)) * f1) - (( proj (i,n)) * f2))) by A2, A5, A18, VALUED_1: 12;

      for z be Element of Z st z in ( dom (( proj (i,n)) * (f1 - f2))) holds ((( proj (i,n)) * (f1 - f2)) . z) = (((( proj (i,n)) * f1) - (( proj (i,n)) * f2)) . z)

      proof

        let z be Element of Z;

        reconsider f1z = (f1 /. z) as Element of (n -tuples_on REAL );

        reconsider f2z = (f2 /. z) as Element of (n -tuples_on REAL );

        assume

         A21: z in ( dom (( proj (i,n)) * (f1 - f2)));

        then

         A22: z in ( dom (f1 - f2)) by A17, RELAT_1: 27;

        then

         A23: z in (( dom f1) /\ ( dom f2)) by VALUED_2:def 46;

        then z in ( dom f1) by XBOOLE_0:def 4;

        then

         A24: (f1 . z) = f1z by PARTFUN1:def 6;

        z in ( dom f2) by A23, XBOOLE_0:def 4;

        then

         A25: (f2 . z) = f2z by PARTFUN1:def 6;

        z in ( dom (( proj (i,n)) * f2)) by A5, A19, A18, A21, XBOOLE_0:def 4;

        then ((( proj (i,n)) * f2) . z) = (( proj (i,n)) . (f2 . z)) by FUNCT_1: 12;

        then

         A26: ((( proj (i,n)) * f2) . z) = (f2z . i) by A25, PDIFF_1:def 1;

        (( proj (i,n)) . ((f1 - f2) . z)) = (( proj (i,n)) . ((f1 . z) - (f2 . z))) by A22, VALUED_2:def 46;

        then (( proj (i,n)) . ((f1 - f2) . z)) = (((f1 /. z) - (f2 /. z)) . i) by A24, A25, PDIFF_1:def 1;

        then

         A27: (( proj (i,n)) . ((f1 - f2) . z)) = ((f1z . i) - (f2z . i)) by RVSUM_1: 27;

        z in ( dom (( proj (i,n)) * f1)) by A2, A19, A18, A21, XBOOLE_0:def 4;

        then ((( proj (i,n)) * f1) . z) = (( proj (i,n)) . (f1 . z)) by FUNCT_1: 12;

        then

         A28: ((( proj (i,n)) * f1) . z) = (f1z . i) by A24, PDIFF_1:def 1;

        (((( proj (i,n)) * f1) - (( proj (i,n)) * f2)) . z) = (((( proj (i,n)) * f1) . z) - ((( proj (i,n)) * f2) . z)) by A20, A21, VALUED_1: 13;

        hence thesis by A21, A27, A28, A26, FUNCT_1: 12;

      end;

      hence thesis by A20, PARTFUN1: 5;

    end;

    theorem :: INTEGR15:16

    

     Th16: for n,i be Element of NAT , r be Real, f be PartFunc of Z, ( REAL n) holds (( proj (i,n)) * (r (#) f)) = (r (#) (( proj (i,n)) * f))

    proof

      let n,i be Element of NAT ;

      let r be Real;

      let f be PartFunc of Z, ( REAL n);

      

       A1: ( dom (r (#) f)) = ( dom f) by VALUED_2:def 39;

      

       A2: ( dom ( proj (i,n))) = ( REAL n) by FUNCT_2:def 1;

      then

       A3: ( rng (r (#) f)) c= ( dom ( proj (i,n)));

      ( rng f) c= ( dom ( proj (i,n))) by A2;

      then

       A4: ( dom (( proj (i,n)) * f)) = ( dom f) by RELAT_1: 27;

      then ( dom (r (#) (( proj (i,n)) * f))) = ( dom f) by VALUED_1:def 5;

      then

       A5: ( dom (( proj (i,n)) * (r (#) f))) = ( dom (r (#) (( proj (i,n)) * f))) by A1, A3, RELAT_1: 27;

      for z be Element of Z st z in ( dom (r (#) (( proj (i,n)) * f))) holds ((( proj (i,n)) * (r (#) f)) . z) = ((r (#) (( proj (i,n)) * f)) . z)

      proof

        let z be Element of Z;

        reconsider fz = (f /. z) as Element of (n -tuples_on REAL );

        reconsider rfz = ((r (#) f) /. z) as Element of (n -tuples_on REAL );

        assume

         A6: z in ( dom (r (#) (( proj (i,n)) * f)));

        then

         A7: z in ( dom (( proj (i,n)) * f)) by VALUED_1:def 5;

        then

         A8: (f . z) = fz by A4, PARTFUN1:def 6;

        ((r (#) (( proj (i,n)) * f)) . z) = (r * ((( proj (i,n)) * f) . z)) by A6, VALUED_1:def 5

        .= (r * (( proj (i,n)) . fz)) by A7, A8, FUNCT_1: 12;

        then

         A9: ((r (#) (( proj (i,n)) * f)) . z) = (r * (fz . i)) by PDIFF_1:def 1;

        

         A10: ((r (#) f) . z) = rfz by A1, A4, A7, PARTFUN1:def 6;

        

        thus ((( proj (i,n)) * (r (#) f)) . z) = (( proj (i,n)) . ((r (#) f) . z)) by A5, A6, FUNCT_1: 12

        .= (rfz . i) by A10, PDIFF_1:def 1

        .= ((r (#) fz) . i) by A1, A4, A7, A8, A10, VALUED_2:def 39

        .= ((r (#) (( proj (i,n)) * f)) . z) by A9, RVSUM_1: 44;

      end;

      hence thesis by A5, PARTFUN1: 5;

    end;

    theorem :: INTEGR15:17

    for n be Element of NAT holds for A be non empty closed_interval Subset of REAL holds for f1,f2 be PartFunc of REAL , ( REAL n) st f1 is_integrable_on A & f2 is_integrable_on A & A c= ( dom f1) & A c= ( dom f2) & (f1 | A) is bounded & (f2 | A) is bounded holds (f1 + f2) is_integrable_on A & (f1 - f2) is_integrable_on A & ( integral ((f1 + f2),A)) = (( integral (f1,A)) + ( integral (f2,A))) & ( integral ((f1 - f2),A)) = (( integral (f1,A)) - ( integral (f2,A)))

    proof

      let n be Element of NAT ;

      let A be non empty closed_interval Subset of REAL ;

      let f1,f2 be PartFunc of REAL , ( REAL n);

      assume that

       A1: f1 is_integrable_on A & f2 is_integrable_on A and

       A2: A c= ( dom f1) & A c= ( dom f2) and

       A3: (f1 | A) is bounded and

       A4: (f2 | A) is bounded;

      

       A5: for i be Element of NAT st i in ( Seg n) holds A c= ( dom (( proj (i,n)) * f1)) & A c= ( dom (( proj (i,n)) * f2))

      proof

        let i be Element of NAT ;

        assume i in ( Seg n);

        ( dom ( proj (i,n))) = ( REAL n) by FUNCT_2:def 1;

        then ( rng f1) c= ( dom ( proj (i,n))) & ( rng f2) c= ( dom ( proj (i,n)));

        hence thesis by A2, RELAT_1: 27;

      end;

      

       A6: for i be Element of NAT st i in ( Seg n) holds ((( proj (i,n)) * f1) + (( proj (i,n)) * f2)) is_integrable_on A & ( integral (((( proj (i,n)) * f1) + (( proj (i,n)) * f2)),A)) = (( integral ((( proj (i,n)) * f1),A)) + ( integral ((( proj (i,n)) * f2),A))) & ((( proj (i,n)) * f1) - (( proj (i,n)) * f2)) is_integrable_on A & ( integral (((( proj (i,n)) * f1) - (( proj (i,n)) * f2)),A)) = (( integral ((( proj (i,n)) * f1),A)) - ( integral ((( proj (i,n)) * f2),A)))

      proof

        let i be Element of NAT ;

        assume

         A7: i in ( Seg n);

        then

         A8: A c= ( dom (( proj (i,n)) * f1)) & A c= ( dom (( proj (i,n)) * f2)) by A5;

        (( proj (i,n)) * (f2 | A)) is bounded by A4, A7;

        then

         A9: ((( proj (i,n)) * f2) | A) is bounded by Lm6;

        (( proj (i,n)) * (f1 | A)) is bounded by A3, A7;

        then

         A10: ((( proj (i,n)) * f1) | A) is bounded by Lm6;

        

         A11: (( proj (i,n)) * f1) is_integrable_on A & (( proj (i,n)) * f2) is_integrable_on A by A1, A7;

        hence ((( proj (i,n)) * f1) + (( proj (i,n)) * f2)) is_integrable_on A & ( integral (((( proj (i,n)) * f1) + (( proj (i,n)) * f2)),A)) = (( integral ((( proj (i,n)) * f1),A)) + ( integral ((( proj (i,n)) * f2),A))) by A8, A10, A9, INTEGRA6: 11;

        thus ((( proj (i,n)) * f1) - (( proj (i,n)) * f2)) is_integrable_on A & ( integral (((( proj (i,n)) * f1) - (( proj (i,n)) * f2)),A)) = (( integral ((( proj (i,n)) * f1),A)) - ( integral ((( proj (i,n)) * f2),A))) by A8, A10, A9, A11, INTEGRA6: 11;

      end;

      

       A12: for i be Element of NAT st i in ( Seg n) holds (( proj (i,n)) * (f1 + f2)) is_integrable_on A & (( proj (i,n)) * (f1 - f2)) is_integrable_on A

      proof

        let i be Element of NAT ;

        assume i in ( Seg n);

        then ((( proj (i,n)) * f1) + (( proj (i,n)) * f2)) is_integrable_on A & ((( proj (i,n)) * f1) - (( proj (i,n)) * f2)) is_integrable_on A by A6;

        hence thesis by Th15;

      end;

      then for i be Element of NAT st i in ( Seg n) holds (( proj (i,n)) * (f1 + f2)) is_integrable_on A;

      hence (f1 + f2) is_integrable_on A;

      

       A13: for i be Element of NAT st i in ( Seg n) holds ((( integral (f1,A)) . i) + (( integral (f2,A)) . i)) = (( integral ((( proj (i,n)) * f1),A)) + ( integral ((( proj (i,n)) * f2),A))) & ((( integral (f1,A)) . i) - (( integral (f2,A)) . i)) = (( integral ((( proj (i,n)) * f1),A)) - ( integral ((( proj (i,n)) * f2),A)))

      proof

        let i be Element of NAT ;

        assume

         A14: i in ( Seg n);

        then (( integral (f1,A)) . i) = ( integral ((( proj (i,n)) * f1),A)) by Def17;

        hence thesis by A14, Def17;

      end;

      

       A15: for i be Element of NAT st i in ( Seg n) holds ((( integral (f1,A)) . i) + (( integral (f2,A)) . i)) = ( integral (((( proj (i,n)) * f1) + (( proj (i,n)) * f2)),A)) & ((( integral (f1,A)) . i) - (( integral (f2,A)) . i)) = ( integral (((( proj (i,n)) * f1) - (( proj (i,n)) * f2)),A))

      proof

        let i be Element of NAT ;

        assume

         A16: i in ( Seg n);

        then ((( integral (f1,A)) . i) + (( integral (f2,A)) . i)) = (( integral ((( proj (i,n)) * f1),A)) + ( integral ((( proj (i,n)) * f2),A))) & ((( integral (f1,A)) . i) - (( integral (f2,A)) . i)) = (( integral ((( proj (i,n)) * f1),A)) - ( integral ((( proj (i,n)) * f2),A))) by A13;

        hence thesis by A6, A16;

      end;

      

       A17: for i be Element of NAT st i in ( Seg n) holds ((( integral (f1,A)) . i) + (( integral (f2,A)) . i)) = ( integral ((( proj (i,n)) * (f1 + f2)),A)) & ((( integral (f1,A)) . i) - (( integral (f2,A)) . i)) = ( integral ((( proj (i,n)) * (f1 - f2)),A))

      proof

        let i be Element of NAT ;

        assume i in ( Seg n);

        then ((( integral (f1,A)) . i) + (( integral (f2,A)) . i)) = ( integral (((( proj (i,n)) * f1) + (( proj (i,n)) * f2)),A)) & ((( integral (f1,A)) . i) - (( integral (f2,A)) . i)) = ( integral (((( proj (i,n)) * f1) - (( proj (i,n)) * f2)),A)) by A15;

        hence thesis by Th15;

      end;

      

       A18: for i be Element of NAT st i in ( Seg n) holds (( integral ((f1 + f2),A)) . i) = ((( integral (f1,A)) . i) + (( integral (f2,A)) . i)) & (( integral ((f1 - f2),A)) . i) = ((( integral (f1,A)) . i) - (( integral (f2,A)) . i))

      proof

        let i be Element of NAT ;

        assume

         A19: i in ( Seg n);

        then ((( integral (f1,A)) . i) + (( integral (f2,A)) . i)) = ( integral ((( proj (i,n)) * (f1 + f2)),A)) & ((( integral (f1,A)) . i) - (( integral (f2,A)) . i)) = ( integral ((( proj (i,n)) * (f1 - f2)),A)) by A17;

        hence thesis by A19, Def17;

      end;

      for i be Element of NAT st i in ( Seg n) holds (( proj (i,n)) * (f1 - f2)) is_integrable_on A by A12;

      hence (f1 - f2) is_integrable_on A;

      

       A20: ( dom ( integral ((f1 + f2),A))) = ( Seg n) by FINSEQ_1: 89;

      

       A21: for i be Element of NAT st i in ( dom ( integral ((f1 + f2),A))) holds (( integral ((f1 + f2),A)) . i) = ((( integral (f1,A)) + ( integral (f2,A))) . i)

      proof

        let i be Element of NAT ;

        assume i in ( dom ( integral ((f1 + f2),A)));

        then (( integral ((f1 + f2),A)) . i) = ((( integral (f1,A)) . i) + (( integral (f2,A)) . i)) by A18, A20;

        hence thesis by RVSUM_1: 11;

      end;

      ( dom (( integral (f1,A)) + ( integral (f2,A)))) = ( Seg n) by FINSEQ_1: 89;

      hence ( integral ((f1 + f2),A)) = (( integral (f1,A)) + ( integral (f2,A))) by A21, FINSEQ_1: 89, PARTFUN1: 5;

      

       A22: ( dom ( integral ((f1 - f2),A))) = ( Seg n) by FINSEQ_1: 89;

      

       A23: for i be Element of NAT st i in ( dom ( integral ((f1 - f2),A))) holds (( integral ((f1 - f2),A)) . i) = ((( integral (f1,A)) - ( integral (f2,A))) . i)

      proof

        let i be Element of NAT ;

        assume i in ( dom ( integral ((f1 - f2),A)));

        then (( integral ((f1 - f2),A)) . i) = ((( integral (f1,A)) . i) - (( integral (f2,A)) . i)) by A18, A22;

        hence thesis by RVSUM_1: 27;

      end;

      ( dom (( integral (f1,A)) - ( integral (f2,A)))) = ( Seg n) by FINSEQ_1: 89;

      hence thesis by A23, FINSEQ_1: 89, PARTFUN1: 5;

    end;

    theorem :: INTEGR15:18

    for n be Element of NAT holds for r be Real holds for A be non empty closed_interval Subset of REAL holds for f be PartFunc of REAL , ( REAL n) st A c= ( dom f) & f is_integrable_on A & (f | A) is bounded holds (r (#) f) is_integrable_on A & ( integral ((r (#) f),A)) = (r * ( integral (f,A)))

    proof

      let n be Element of NAT ;

      let r be Real;

      let A be non empty closed_interval Subset of REAL ;

      let f be PartFunc of REAL , ( REAL n);

      assume that

       A1: A c= ( dom f) and

       A2: f is_integrable_on A and

       A3: (f | A) is bounded;

       A4:

      now

        let i be Element of NAT ;

        ( dom ( proj (i,n))) = ( REAL n) by FUNCT_2:def 1;

        then ( rng f) c= ( dom ( proj (i,n)));

        hence A c= ( dom (( proj (i,n)) * f)) by A1, RELAT_1: 27;

      end;

      

       A5: for i be Element of NAT st i in ( Seg n) holds ( integral ((r (#) (( proj (i,n)) * f)),A)) = (r * ( integral ((( proj (i,n)) * f),A)))

      proof

        let i be Element of NAT ;

        assume

         A6: i in ( Seg n);

        ((( proj (i,n)) * f) | A) = (( proj (i,n)) * (f | A)) by Lm6;

        then

         A7: ((( proj (i,n)) * f) | A) is bounded by A3, A6;

        

         A8: A c= ( dom (( proj (i,n)) * f)) by A4;

        (( proj (i,n)) * f) is_integrable_on A by A2, A6;

        hence thesis by A7, A8, INTEGRA6: 9;

      end;

      

       A9: for i be Element of NAT st i in ( Seg n) holds ((r * ( integral (f,A))) . i) = (r * ( integral ((( proj (i,n)) * f),A)))

      proof

        let i be Element of NAT ;

        assume i in ( Seg n);

        then (r * (( integral (f,A)) . i)) = (r * ( integral ((( proj (i,n)) * f),A))) by Def17;

        hence thesis by RVSUM_1: 45;

      end;

      

       A10: for i be Element of NAT st i in ( Seg n) holds (( integral ((r (#) f),A)) . i) = ((r * ( integral (f,A))) . i)

      proof

        let i be Element of NAT ;

        

         A11: ( integral ((r (#) (( proj (i,n)) * f)),A)) = ( integral ((( proj (i,n)) * (r (#) f)),A)) by Th16;

        assume

         A12: i in ( Seg n);

        then (( integral ((r (#) f),A)) . i) = ( integral ((( proj (i,n)) * (r (#) f)),A)) & ((r * ( integral (f,A))) . i) = (r * ( integral ((( proj (i,n)) * f),A))) by A9, Def17;

        hence thesis by A5, A12, A11;

      end;

      for i be Element of NAT st i in ( Seg n) holds (( proj (i,n)) * (r (#) f)) is_integrable_on A

      proof

        let i be Element of NAT ;

        assume

         A13: i in ( Seg n);

        ((( proj (i,n)) * f) | A) = (( proj (i,n)) * (f | A)) by Lm6;

        then

         A14: ((( proj (i,n)) * f) | A) is bounded by A3, A13;

        

         A15: A c= ( dom (( proj (i,n)) * f)) by A4;

        (( proj (i,n)) * f) is_integrable_on A by A2, A13;

        then (r (#) (( proj (i,n)) * f)) is_integrable_on A by A14, A15, INTEGRA6: 9;

        hence thesis by Th16;

      end;

      hence (r (#) f) is_integrable_on A;

      

       A16: ( dom ( integral ((r (#) f),A))) = ( Seg n) by FINSEQ_1: 89;

      then ( dom ( integral ((r (#) f),A))) = ( dom (r * ( integral (f,A)))) by FINSEQ_1: 89;

      hence thesis by A10, A16, PARTFUN1: 5;

    end;

    theorem :: INTEGR15:19

    for n be Element of NAT holds for f be PartFunc of REAL , ( REAL n), A be non empty closed_interval Subset of REAL , a,b be Real st A = [.a, b.] holds ( integral (f,A)) = ( integral (f,a,b))

    proof

      let n be Element of NAT ;

      let f be PartFunc of REAL , ( REAL n), A be non empty closed_interval Subset of REAL , a,b be Real;

      assume

       A1: A = [.a, b.];

       A2:

      now

        let i be Nat;

        assume

         A3: i in ( dom ( integral (f,A)));

        then

        reconsider k = i as Element of NAT ;

        ( dom ( integral (f,A))) = ( Seg n) by Def17;

        then (( integral (f,A)) . k) = ( integral ((( proj (k,n)) * f),A)) & (( integral (f,a,b)) . k) = ( integral ((( proj (k,n)) * f),a,b)) by A3, Def17, Def18;

        hence (( integral (f,A)) . i) = (( integral (f,a,b)) . i) by A1, INTEGRA5: 19;

      end;

      ( dom ( integral (f,A))) = ( Seg n) by Def17

      .= ( dom ( integral (f,a,b))) by Def18;

      hence ( integral (f,A)) = ( integral (f,a,b)) by A2, FINSEQ_1: 13;

    end;

    theorem :: INTEGR15:20

    for n be Element of NAT holds for f be PartFunc of REAL , ( REAL n), A be non empty closed_interval Subset of REAL , a,b be Real st A = [.b, a.] holds ( - ( integral (f,A))) = ( integral (f,a,b))

    proof

      let n be Element of NAT ;

      let f be PartFunc of REAL , ( REAL n), A be non empty closed_interval Subset of REAL , a,b be Real;

      assume

       A1: A = [.b, a.];

       A2:

      now

        let i be Nat;

        assume

         A3: i in ( dom ( - ( integral (f,A))));

        then

        reconsider k = i as Element of NAT ;

        

         A4: ( dom ( integral (f,A))) = ( Seg n) by Def17;

        

         A5: k in ( dom ( integral (f,A))) by A3, VALUED_1: 8;

        then

         A6: (( integral (f,a,b)) . k) = ( integral ((( proj (k,n)) * f),a,b)) by A4, Def18;

        (( - ( integral (f,A))) . k) = ( - (( integral (f,A)) . k)) by VALUED_1: 8

        .= ( - ( integral ((( proj (k,n)) * f),A))) by A5, A4, Def17;

        hence (( - ( integral (f,A))) . i) = (( integral (f,a,b)) . i) by A1, A6, INTEGRA5: 20;

      end;

      reconsider jj = 1 as Real;

      ( dom ( - ( integral (f,A)))) = ( dom (( - jj) (#) ( integral (f,A)))) by VALUED_1:def 6

      .= ( dom ( integral (f,A))) by VALUED_1:def 5

      .= ( Seg n) by Def17

      .= ( dom ( integral (f,a,b))) by Def18;

      hence thesis by A2, FINSEQ_1: 13;

    end;

    theorem :: INTEGR15:21

    for n be Nat, Z,x be set, f,g be PartFunc of Z, ( REAL n) st x in ( dom (f + g)) holds ((f + g) /. x) = ((f /. x) + (g /. x))

    proof

      let n be Nat;

      let Z,x be set;

      let f,g be PartFunc of Z, ( REAL n);

      assume

       A1: x in ( dom (f + g));

      ( dom (f + g)) = (( dom f) /\ ( dom g)) by VALUED_2:def 45;

      then x in ( dom f) & x in ( dom g) by A1, XBOOLE_0:def 4;

      then

       A2: (f . x) = (f /. x) & (g . x) = (g /. x) by PARTFUN1:def 6;

      

      thus ((f + g) /. x) = ((f + g) . x) by A1, PARTFUN1:def 6

      .= ((f /. x) + (g /. x)) by A1, A2, VALUED_2:def 45;

    end;

    theorem :: INTEGR15:22

    for n be Nat, Z,x be set, f,g be PartFunc of Z, ( REAL n) st x in ( dom (f - g)) holds ((f - g) /. x) = ((f /. x) - (g /. x))

    proof

      let n be Nat;

      let Z,x be set;

      let f,g be PartFunc of Z, ( REAL n);

      assume

       A1: x in ( dom (f - g));

      ( dom (f - g)) = (( dom f) /\ ( dom g)) by VALUED_2:def 46;

      then x in ( dom f) & x in ( dom g) by A1, XBOOLE_0:def 4;

      then

       A2: (f . x) = (f /. x) & (g . x) = (g /. x) by PARTFUN1:def 6;

      

      thus ((f - g) /. x) = ((f - g) . x) by A1, PARTFUN1:def 6

      .= ((f /. x) - (g /. x)) by A1, A2, VALUED_2:def 46;

    end;

    theorem :: INTEGR15:23

    for n be Nat, Z,x be set, f be PartFunc of Z, ( REAL n) holds for r be Real st x in ( dom (r (#) f)) holds ((r (#) f) /. x) = (r * (f /. x))

    proof

      let n be Nat;

      let Z,x be set;

      let f be PartFunc of Z, ( REAL n);

      let r be Real;

      assume

       A1: x in ( dom (r (#) f));

      ( dom (r (#) f)) = ( dom f) by VALUED_2:def 39;

      then

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

      

      thus ((r (#) f) /. x) = ((r (#) f) . x) by A1, PARTFUN1:def 6

      .= (r * (f /. x)) by A1, A2, VALUED_2:def 39;

    end;