integr18.miz



    begin

    reserve X for RealNormSpace;

    definition

      let X be RealNormSpace;

      let A be non empty closed_interval Subset of REAL ;

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

      let D be Division of A;

      :: INTEGR18:def1

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

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

      correctness

      proof

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

        

         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 the carrier of X 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 c be object such that

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

          reconsider c as Point of X by A4;

          (( vol ( divset (D,k))) * c) is Element of the carrier of X;

          hence thesis by A4;

        end;

        consider p be FinSequence of the carrier of X 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 X be RealNormSpace;

      let A be non empty closed_interval Subset of REAL ;

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

      let D be Division of A;

      let F be middle_volume of f, D;

      :: INTEGR18:def2

      func middle_sum (f,F) -> Point of X equals ( Sum F);

      coherence ;

    end

    definition

      let X be RealNormSpace;

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

      :: INTEGR18:def3

      mode middle_volume_Sequence of f,T -> sequence of (the carrier of X * ) 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 (the carrier of X * ) 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 (the carrier of X * ) by FINSEQ_1:def 11;

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

          hence thesis;

        end;

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

        hence thesis;

      end;

    end

    definition

      let X be RealNormSpace;

      let A be non empty closed_interval Subset of REAL , f be Function of A, the carrier of X, T be DivSequence of A, S be middle_volume_Sequence of f, T, k be Nat;

      :: original: .

      redefine

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

      coherence

      proof

        k in NAT by ORDINAL1:def 12;

        hence thesis by Def3;

      end;

    end

    definition

      let X be RealNormSpace;

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

      :: INTEGR18:def4

      func middle_sum (f,S) -> sequence of X means

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

      existence

      proof

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

        consider IT be sequence of the carrier of X such that

         A1: for i be Element of NAT holds (IT . i) = H1(i) from FUNCT_2:sch 4;

        take IT;

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let F1,F2 be sequence of X;

        assume that

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

         A3: for i be 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

    begin

    definition

      let X be RealNormSpace;

      let A be non empty closed_interval Subset of REAL ;

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

      :: INTEGR18:def5

      attr f is integrable means ex I be Point of X 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;

    end

    theorem :: INTEGR18:1

    

     Th1: for X be RealNormSpace, R1,R2,R3 be FinSequence of X st ( len R1) = ( len R2) & R3 = (R1 + R2) holds ( Sum R3) = (( Sum R1) + ( Sum R2))

    proof

      let X be RealNormSpace, R1,R2,R3 be FinSequence of X;

      assume

       A1: ( len R1) = ( len R2) & R3 = (R1 + R2);

      then ( dom R1) = ( dom R2) by FINSEQ_3: 29;

      hence ( Sum R3) = (( Sum R1) + ( Sum R2)) by A1, BINOM: 7;

    end;

    theorem :: INTEGR18:2

    for X be RealNormSpace, R1,R2,R3 be FinSequence of X st ( len R1) = ( len R2) & R3 = (R1 - R2) holds ( Sum R3) = (( Sum R1) - ( Sum R2))

    proof

      let X be RealNormSpace, R1,R2,R3 be FinSequence of X;

      assume

       A1: ( len R1) = ( len R2) & R3 = (R1 - R2);

      then

       A2: ( dom R1) = ( dom R2) by FINSEQ_3: 29;

      

       A3: ( dom R3) = (( dom R1) /\ ( dom R2)) by A1, VFUNCT_1:def 2

      .= ( dom R1) by A2;

      then

       A4: ( len R3) = ( len R1) by FINSEQ_3: 29;

      

       A5: for k be Nat st k in ( dom R1) holds (R3 . k) = ((R1 /. k) - (R2 /. k))

      proof

        let k be Nat;

        assume

         A6: k in ( dom R1);

        

        thus (R3 . k) = (R3 /. k) by A6, A3, PARTFUN1:def 6

        .= ((R1 /. k) - (R2 /. k)) by A1, A6, A3, VFUNCT_1:def 2;

      end;

      thus thesis by A1, A4, A5, RLVECT_2: 5;

    end;

    theorem :: INTEGR18:3

    

     Th3: for X be RealNormSpace, R1,R2 be FinSequence of X, a be Real st R2 = (a (#) R1) holds ( Sum R2) = (a * ( Sum R1))

    proof

      let X be RealNormSpace, R1,R2 be FinSequence of X, a be Real;

      assume

       A1: R2 = (a (#) R1);

      ( dom R2) = ( dom R1) by A1, VFUNCT_1:def 4;

      then

       A2: ( len R2) = ( len R1) by FINSEQ_3: 29;

      

       A3: for k be Nat st k in ( dom R1) holds (R2 . k) = (a * (R1 /. k))

      proof

        let k be Nat;

        assume k in ( dom R1);

        then

         A4: k in ( dom R2) by A1, VFUNCT_1:def 4;

        

        thus (R2 . k) = (R2 /. k) by A4, PARTFUN1:def 6

        .= (a * (R1 /. k)) by A4, A1, VFUNCT_1:def 4;

      end;

      thus thesis by A2, A3, RLVECT_2: 3;

    end;

    definition

      let X be RealNormSpace;

      let A be non empty closed_interval Subset of REAL ;

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

      assume

       A1: f is integrable;

      :: INTEGR18:def6

      func integral (f) -> Point of X means

      : Def6: 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))) = it ;

      existence by A1;

      uniqueness

      proof

        let I1,I2 be Point of X;

        assume

         A2: 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))) = I1;

        assume

         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))) = I2;

        consider T be DivSequence of A such that

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

        set S = the middle_volume_Sequence of f, T;

        

        thus I1 = ( lim ( middle_sum (f,S))) by A2, A4

        .= I2 by A3, A4;

      end;

    end

    theorem :: INTEGR18:4

    

     Th4: for X be RealNormSpace, A be non empty closed_interval Subset of REAL , r be Real, f,h be Function of A, the carrier of X st h = (r (#) f) & f is integrable holds h is integrable & ( integral h) = (r * ( integral f))

    proof

      let X be RealNormSpace, A be non empty closed_interval Subset of REAL , r be Real, f,h be Function of A, the carrier of X;

      assume

       A1: h = (r (#) f) & f is integrable;

      

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

       A3:

      now

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

        assume

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

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

        

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

        proof

          let k be Element of NAT ;

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

          

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

          

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

          proof

            let i be Nat;

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

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

            then

            consider c be Point of X such that

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

            consider x be object such that

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

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

            then

            reconsider x as Element of REAL ;

            take x;

            thus thesis by A8, A9;

          end;

          consider p be FinSequence of REAL such that

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

          take p;

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

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

        end;

        consider F be sequence of ( REAL * ) such that

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

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

        

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

        proof

          let k be Element of NAT ;

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

          

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

          

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

          proof

            let i be Nat;

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

            then

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

            consider p be FinSequence of REAL such that

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

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

            then

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

            then (p . i) in ( dom (f | ( divset ((T . k),i)))) by A2, RELAT_1: 57;

            then ((f | ( divset ((T . k),i))) . (p . i)) in ( rng (f | ( divset ((T . k),i)))) by FUNCT_1: 3;

            then

            reconsider x = ((f | ( divset ((T . k),i))) . (p . i)) as Element of the carrier of X;

            

             A18: ((F . k) . i) in ( dom (f | ( divset ((T . k),i)))) by A16, A17, A2, RELAT_1: 57;

            (( vol ( divset ((T . k),i))) * x) is Element of the carrier of X;

            hence thesis by A16, A18;

          end;

          consider q be FinSequence of the carrier of X such that

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

          

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

          now

            let i be Nat;

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

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

            then

            consider c be Point of X such that

             A21: ((F . k) . i) in ( dom (f | ( divset ((T . k),i)))) & c = ((f | ( divset ((T . k),i))) . ((F . k) . i)) & (q . i) = (( vol ( divset ((T . k),i))) * c) by A19;

            thus ex c be Point of X st c in ( rng (f | ( divset ((T . k),i)))) & (q . i) = (( vol ( divset ((T . k),i))) * c) by A21, FUNCT_1: 3;

          end;

          then

          reconsider q as middle_volume of f, (T . k) by A20, Def1;

          q is Element of (the carrier of X * ) by FINSEQ_1:def 11;

          hence thesis by A13, A19;

        end;

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

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

        now

          let k be Element of NAT ;

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

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

        end;

        then

        reconsider Sf as middle_volume_Sequence of f, T by Def3;

        

         A23: ( middle_sum (f,Sf)) is convergent by A1, A4;

        

         A24: (r * ( middle_sum (f,Sf))) = ( middle_sum (h,S))

        proof

          now

            let n be Nat;

            

             A25: n in NAT by ORDINAL1:def 12;

            consider p be FinSequence of REAL such that

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

            consider q be middle_volume of f, (T . n) such that

             A27: q = (Sf . n) & for i be Nat st i in ( dom (T . n)) holds ex z be Point of X st ((F . n) . i) in ( dom (f | ( divset ((T . n),i)))) & z = ((f | ( divset ((T . n),i))) . ((F . n) . i)) & (q . i) = (( vol ( divset ((T . n),i))) * z) by A22, A25;

            ( len (Sf . n)) = ( len (T . n)) & ( len (S . n)) = ( len (T . n)) by Def1;

            then

             A28: ( dom (Sf . n)) = ( dom (T . n)) & ( dom (S . n)) = ( dom (T . n)) by FINSEQ_3: 29;

            now

              let x be Element of NAT ;

              assume

               A29: x in ( dom (S . n));

              reconsider i = x as Nat;

              consider t be Point of X such that

               A30: t = ((h | ( divset ((T . n),i))) . ((F . n) . i)) & ((S . n) . i) = (( vol ( divset ((T . n),i))) * t) by A29, A28, A26;

              consider z be Point of X such that

               A31: ((F . n) . i) in ( dom (f | ( divset ((T . n),i)))) & z = ((f | ( divset ((T . n),i))) . ((F . n) . i)) & (q . i) = (( vol ( divset ((T . n),i))) * z) by A27, A29, A28;

              

               A32: ((F . n) . i) in ( divset ((T . n),i)) by A31, RELAT_1: 57;

              ((F . n) . i) in A by A31;

              then

               A33: ((F . n) . i) in ( dom h) by FUNCT_2:def 1;

              

               A34: ((F . n) . i) in ( dom f) by A31, RELAT_1: 57;

              

               A35: (f /. ((F . n) . i)) = (f . ((F . n) . i)) by A34, PARTFUN1:def 6

              .= z by A31, A32, FUNCT_1: 49;

              

               A36: t = ((h | ( divset ((T . n),i))) . ((F . n) . i)) by A30

              .= (h . ((F . n) . i)) by A32, FUNCT_1: 49

              .= (h /. ((F . n) . i)) by A33, PARTFUN1:def 6

              .= (r * (f /. ((F . n) . i))) by A33, A1, VFUNCT_1:def 4

              .= (r * z) by A35;

              

               A37: (( vol ( divset ((T . n),i))) * z) = ((Sf . n) . x) by A31, A27

              .= ((Sf . n) /. x) by A29, A28, PARTFUN1:def 6;

              

              thus ((S . n) /. x) = ((S . n) . x) by A29, PARTFUN1:def 6

              .= (( vol ( divset ((T . n),i))) * t) by A30

              .= (( vol ( divset ((T . n),i))) * (r * z)) by A36

              .= ((( vol ( divset ((T . n),i))) * r) * z) by RLVECT_1:def 7

              .= (r * (( vol ( divset ((T . n),i))) * z)) by RLVECT_1:def 7

              .= (r * ((Sf . n) /. x)) by A37;

            end;

            then

             A38: (r (#) (Sf . n)) = (S . n) by A28, VFUNCT_1:def 4;

            

            thus (r * (( middle_sum (f,Sf)) . n)) = (r * ( middle_sum (f,(Sf . n)))) by Def4

            .= (r * ( Sum (Sf . n)))

            .= ( Sum (S . n)) by A38, Th3

            .= ( middle_sum (h,(S . n)))

            .= (( middle_sum (h,S)) . n) by Def4;

          end;

          hence thesis by NORMSP_1:def 5;

        end;

        

         A39: ( lim (r * ( middle_sum (f,Sf)))) = (r * ( lim ( middle_sum (f,Sf)))) by A23, NORMSP_1: 28

        .= (r * ( integral f)) by Def6, A1, A4;

        thus ( middle_sum (h,S)) is convergent by A23, A24, NORMSP_1: 22;

        thus ( lim ( middle_sum (h,S))) = (r * ( integral f)) by A24, A39;

      end;

      hence h is integrable;

      hence ( integral h) = (r * ( integral f)) by Def6, A3;

    end;

    reconsider jj = 1 as Real;

    theorem :: INTEGR18:5

    

     Th5: for X be RealNormSpace, A be non empty closed_interval Subset of REAL , f,h be Function of A, the carrier of X st h = ( - f) & f is integrable holds h is integrable & ( integral h) = ( - ( integral f))

    proof

      let X be RealNormSpace, A be non empty closed_interval Subset of REAL , f,h be Function of A, the carrier of X;

      assume

       A1: h = ( - f) & f is integrable;

      then

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

      hence h is integrable by A1, Th4;

      ( integral h) = (( - jj) * ( integral f)) by A1, A2, Th4;

      hence ( integral h) = ( - ( integral f)) by RLVECT_1: 16;

    end;

    theorem :: INTEGR18:6

    

     Th6: for X be RealNormSpace, A be non empty closed_interval Subset of REAL , f,g,h be Function of A, the carrier of X st h = (f + g) & f is integrable & g is integrable holds h is integrable & ( integral h) = (( integral f) + ( integral g))

    proof

      let X be RealNormSpace, A be non empty closed_interval Subset of REAL , f,g,h be Function of A, the carrier of X;

      assume

       A1: h = (f + g) & f is integrable & g is integrable;

      

       A2: ( dom h) = A & ( dom f) = A & ( dom g) = A by FUNCT_2:def 1;

       A3:

      now

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

        assume

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

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

        

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

        proof

          let k be Element of NAT ;

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

          

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

          

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

          proof

            let i be Nat;

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

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

            then

            consider c be Point of X such that

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

            consider x be object such that

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

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

            then

            reconsider x as Element of REAL ;

            take x;

            thus thesis by A8, A9;

          end;

          consider p be FinSequence of REAL such that

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

          take p;

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

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

        end;

        consider F be sequence of ( REAL * ) such that

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

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

        

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

        proof

          let k be Element of NAT ;

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

          

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

          

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

          proof

            let i be Nat;

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

            then

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

            consider p be FinSequence of REAL such that

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

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

            then

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

            then (p . i) in ( dom (f | ( divset ((T . k),i)))) by A2, RELAT_1: 57;

            then ((f | ( divset ((T . k),i))) . (p . i)) in ( rng (f | ( divset ((T . k),i)))) by FUNCT_1: 3;

            then

            reconsider x = ((f | ( divset ((T . k),i))) . (p . i)) as Element of the carrier of X;

            

             A18: ((F . k) . i) in ( dom (f | ( divset ((T . k),i)))) by A16, A17, A2, RELAT_1: 57;

            (( vol ( divset ((T . k),i))) * x) is Element of the carrier of X;

            hence thesis by A16, A18;

          end;

          consider q be FinSequence of the carrier of X such that

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

          

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

          now

            let i be Nat;

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

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

            then

            consider c be Point of X such that

             A21: ((F . k) . i) in ( dom (f | ( divset ((T . k),i)))) & c = ((f | ( divset ((T . k),i))) . ((F . k) . i)) & (q . i) = (( vol ( divset ((T . k),i))) * c) by A19;

            thus ex c be Point of X st c in ( rng (f | ( divset ((T . k),i)))) & (q . i) = (( vol ( divset ((T . k),i))) * c) by A21, FUNCT_1: 3;

          end;

          then

          reconsider q as middle_volume of f, (T . k) by A20, Def1;

          q is Element of (the carrier of X * ) by FINSEQ_1:def 11;

          hence thesis by A13, A19;

        end;

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

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

        now

          let k be Element of NAT ;

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

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

        end;

        then

        reconsider Sf as middle_volume_Sequence of f, T by Def3;

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

        

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

        proof

          let k be Element of NAT ;

          defpred Q11[ Nat, set] means ex c be Point of X st ((F . k) . $1) in ( dom (g | ( divset ((T . k),$1)))) & c = ((g | ( divset ((T . k),$1))) . ((F . k) . $1)) & $2 = (( vol ( divset ((T . k),$1))) * c);

          

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

          

           A25: for i be Nat st i in ( Seg ( len (T . k))) holds ex x be Element of the carrier of X st Q11[i, x]

          proof

            let i be Nat;

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

            then

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

            consider p be FinSequence of REAL such that

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

            (p . i) in ( dom (h | ( divset ((T . k),i)))) by A26, A27;

            then

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

            then (p . i) in ( dom (g | ( divset ((T . k),i)))) by A2, RELAT_1: 57;

            then ((g | ( divset ((T . k),i))) . (p . i)) in ( rng (g | ( divset ((T . k),i)))) by FUNCT_1: 3;

            then

            reconsider x = ((g | ( divset ((T . k),i))) . (p . i)) as Element of the carrier of X;

            

             A29: ((F . k) . i) in ( dom (g | ( divset ((T . k),i)))) by A27, A28, A2, RELAT_1: 57;

            (( vol ( divset ((T . k),i))) * x) is Element of the carrier of X;

            hence thesis by A27, A29;

          end;

          consider q be FinSequence of the carrier of X such that

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

          

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

          now

            let i be Nat;

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

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

            then

            consider c be Point of X such that

             A32: ((F . k) . i) in ( dom (g | ( divset ((T . k),i)))) & c = ((g | ( divset ((T . k),i))) . ((F . k) . i)) & (q . i) = (( vol ( divset ((T . k),i))) * c) by A30;

            thus ex c be Point of X st c in ( rng (g | ( divset ((T . k),i)))) & (q . i) = (( vol ( divset ((T . k),i))) * c) by A32, FUNCT_1: 3;

          end;

          then

          reconsider q as middle_volume of g, (T . k) by A31, Def1;

          q is Element of (the carrier of X * ) by FINSEQ_1:def 11;

          hence thesis by A24, A30;

        end;

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

         A33: for x be Element of NAT holds Q1[x, (Sg . x)] from FUNCT_2:sch 3( A23);

        now

          let k be Element of NAT ;

          ex q be middle_volume of g, (T . k) st q = (Sg . k) & for i be Nat st i in ( dom (T . k)) holds ex z be Point of X st ((F . k) . i) in ( dom (g | ( divset ((T . k),i)))) & z = ((g | ( divset ((T . k),i))) . ((F . k) . i)) & (q . i) = (( vol ( divset ((T . k),i))) * z) by A33;

          hence (Sg . k) is middle_volume of g, (T . k);

        end;

        then

        reconsider Sg as middle_volume_Sequence of g, T by Def3;

        

         A34: ( middle_sum (f,Sf)) is convergent & ( lim ( middle_sum (f,Sf))) = ( integral f) by Def6, A1, A4;

        

         A35: ( middle_sum (g,Sg)) is convergent & ( lim ( middle_sum (g,Sg))) = ( integral g) by Def6, A1, A4;

        

         A36: (( middle_sum (f,Sf)) + ( middle_sum (g,Sg))) = ( middle_sum (h,S))

        proof

          now

            let n be Nat;

            

             A37: n in NAT by ORDINAL1:def 12;

            consider p be FinSequence of REAL such that

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

            consider q be middle_volume of f, (T . n) such that

             A39: q = (Sf . n) & for i be Nat st i in ( dom (T . n)) holds ex z be Point of X st ((F . n) . i) in ( dom (f | ( divset ((T . n),i)))) & z = ((f | ( divset ((T . n),i))) . ((F . n) . i)) & (q . i) = (( vol ( divset ((T . n),i))) * z) by A22, A37;

            consider r be middle_volume of g, (T . n) such that

             A40: r = (Sg . n) & for i be Nat st i in ( dom (T . n)) holds ex z be Point of X st ((F . n) . i) in ( dom (g | ( divset ((T . n),i)))) & z = ((g | ( divset ((T . n),i))) . ((F . n) . i)) & (r . i) = (( vol ( divset ((T . n),i))) * z) by A33, A37;

            

             A41: ( len (Sf . n)) = ( len (T . n)) & ( len (Sg . n)) = ( len (T . n)) & ( len (S . n)) = ( len (T . n)) by Def1;

            

             A42: ( dom (Sf . n)) = ( dom (T . n)) & ( dom (Sg . n)) = ( dom (T . n)) & ( dom (S . n)) = ( dom (T . n)) by A41, FINSEQ_3: 29;

            now

              let i be Nat;

              assume 1 <= i & i <= ( len (S . n));

              then i in ( Seg ( len (S . n))) by FINSEQ_1: 1;

              then

               A43: i in ( dom (S . n)) by FINSEQ_1:def 3;

              consider t be Point of X such that

               A44: t = ((h | ( divset ((T . n),i))) . ((F . n) . i)) & ((S . n) . i) = (( vol ( divset ((T . n),i))) * t) by A43, A42, A38;

              consider z be Point of X such that

               A45: ((F . n) . i) in ( dom (f | ( divset ((T . n),i)))) & z = ((f | ( divset ((T . n),i))) . ((F . n) . i)) & (q . i) = (( vol ( divset ((T . n),i))) * z) by A39, A43, A42;

              consider w be Point of X such that

               A46: ((F . n) . i) in ( dom (g | ( divset ((T . n),i)))) & w = ((g | ( divset ((T . n),i))) . ((F . n) . i)) & (r . i) = (( vol ( divset ((T . n),i))) * w) by A40, A43, A42;

              

               A47: ((F . n) . i) in ( divset ((T . n),i)) by A46, RELAT_1: 57;

              

               A48: ((F . n) . i) in ( dom g) by A46, RELAT_1: 57;

              

               A49: ((F . n) . i) in A by A46;

              then

               A50: ((F . n) . i) in ( dom h) by FUNCT_2:def 1;

              

               A51: ((F . n) . i) in ( dom f) by A49, FUNCT_2:def 1;

              

               A52: (f /. ((F . n) . i)) = (f . ((F . n) . i)) by A51, PARTFUN1:def 6

              .= z by A45, A47, FUNCT_1: 49;

              

               A53: (g /. ((F . n) . i)) = (g . ((F . n) . i)) by A48, PARTFUN1:def 6

              .= w by A46, A47, FUNCT_1: 49;

              

               A54: t = ((h | ( divset ((T . n),i))) . ((F . n) . i)) by A44

              .= (h . ((F . n) . i)) by A47, FUNCT_1: 49

              .= (h /. ((F . n) . i)) by A50, PARTFUN1:def 6

              .= ((f /. ((F . n) . i)) + (g /. ((F . n) . i))) by A50, A1, VFUNCT_1:def 1

              .= (z + w) by A52, A53;

              

               A55: (( vol ( divset ((T . n),i))) * z) = ((Sf . n) . i) by A45, A39

              .= ((Sf . n) /. i) by A43, A42, PARTFUN1:def 6;

              

               A56: (( vol ( divset ((T . n),i))) * w) = ((Sg . n) . i) by A46, A40

              .= ((Sg . n) /. i) by A43, A42, PARTFUN1:def 6;

              

              thus ((S . n) /. i) = ((S . n) . i) by A43, PARTFUN1:def 6

              .= (( vol ( divset ((T . n),i))) * t) by A44

              .= ((( vol ( divset ((T . n),i))) * z) + (( vol ( divset ((T . n),i))) * w)) by A54, RLVECT_1:def 5

              .= (((Sf . n) /. i) + ((Sg . n) /. i)) by A55, A56;

            end;

            then

             A57: ((Sf . n) + (Sg . n)) = (S . n) by A42, BINOM:def 1;

            

            thus ((( middle_sum (f,Sf)) . n) + (( middle_sum (g,Sg)) . n)) = (( middle_sum (f,(Sf . n))) + (( middle_sum (g,Sg)) . n)) by Def4

            .= (( middle_sum (f,(Sf . n))) + ( middle_sum (g,(Sg . n)))) by Def4

            .= (( Sum (Sf . n)) + ( middle_sum (g,(Sg . n))))

            .= (( Sum (Sf . n)) + ( Sum (Sg . n)))

            .= ( Sum (S . n)) by A57, A41, Th1

            .= ( middle_sum (h,(S . n)))

            .= (( middle_sum (h,S)) . n) by Def4;

          end;

          hence thesis by NORMSP_1:def 2;

        end;

        hence ( middle_sum (h,S)) is convergent by A34, A35, NORMSP_1: 19;

        thus ( lim ( middle_sum (h,S))) = (( integral f) + ( integral g)) by A34, A35, A36, NORMSP_1: 25;

      end;

      hence h is integrable;

      hence ( integral h) = (( integral f) + ( integral g)) by Def6, A3;

    end;

    theorem :: INTEGR18:7

    for X be RealNormSpace, A be non empty closed_interval Subset of REAL , f,g,h be Function of A, the carrier of X st h = (f - g) & f is integrable & g is integrable holds h is integrable & ( integral h) = (( integral f) - ( integral g))

    proof

      let X be RealNormSpace, A be non empty closed_interval Subset of REAL , f,g,h be Function of A, the carrier of X;

      assume

       A1: h = (f - g) & f is integrable & g is integrable;

      then

       A2: h = (f + ( - g)) by VFUNCT_1: 25;

      ( dom ( - g)) = ( dom g) by VFUNCT_1:def 5

      .= A by FUNCT_2:def 1;

      then

      reconsider gg = ( - g) as Function of A, the carrier of X by FUNCT_2:def 1;

      

       A3: gg is integrable by A1, Th5;

      hence h is integrable by A1, A2, Th6;

      ( integral h) = (( integral f) + ( integral gg)) by A1, A2, A3, Th6;

      then ( integral h) = (( integral f) + ( - ( integral g))) by A1, Th5;

      hence ( integral h) = (( integral f) - ( integral g)) by RLVECT_1:def 11;

    end;

    definition

      let X be RealNormSpace;

      let A be non empty closed_interval Subset of REAL ;

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

      :: INTEGR18:def7

      pred f is_integrable_on A means ex g be Function of A, the carrier of X st g = (f | A) & g is integrable;

    end

    definition

      let X be RealNormSpace;

      let A be non empty closed_interval Subset of REAL ;

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

      assume

       A1: A c= ( dom f);

      :: INTEGR18:def8

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

      : Def8: ex g be Function of A, the carrier of X st g = (f | A) & it = ( integral g);

      correctness

      proof

        

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

        ( rng (f | A)) c= the carrier of X;

        then

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

        ( integral g) is Point of X;

        hence thesis;

      end;

    end

    theorem :: INTEGR18:8

    for A be non empty closed_interval Subset of REAL , f be PartFunc of REAL , the carrier of X, g be Function of A, the carrier of X st (f | A) = g holds f is_integrable_on A iff g is integrable;

    theorem :: INTEGR18:9

    for A be non empty closed_interval Subset of REAL , f be PartFunc of REAL , the carrier of X, g be Function of A, the carrier of X st A c= ( dom f) & (f | A) = g holds ( integral (f,A)) = ( integral g) by Def8;

    theorem :: INTEGR18:10

    

     Th10: for X,Y be non empty set, V be RealNormSpace, g,f be PartFunc of X, the carrier of V, g1,f1 be PartFunc of Y, the carrier of V st g = g1 & f = f1 holds (g1 + f1) = (g + f)

    proof

      let X,Y be non empty set, V be RealNormSpace, g,f be PartFunc of X, the carrier of V, g1,f1 be PartFunc of Y, the carrier of V;

      assume

       A1: g = g1 & f = f1;

      

       A2: ( dom (g + f)) = (( dom g) /\ ( dom f)) by VFUNCT_1:def 1

      .= (( dom g1) /\ ( dom f1)) by A1;

      

       A3: (g + f) is PartFunc of Y, the carrier of V by A2, RELSET_1: 5;

      for c be Element of Y st c in ( dom (g + f)) holds ((g + f) /. c) = ((g1 /. c) + (f1 /. c)) by A1, VFUNCT_1:def 1;

      hence thesis by A3, A2, VFUNCT_1:def 1;

    end;

    theorem :: INTEGR18:11

    for X,Y be non empty set, V be RealNormSpace, g,f be PartFunc of X, the carrier of V, g1,f1 be PartFunc of Y, the carrier of V st g = g1 & f = f1 holds (g1 - f1) = (g - f)

    proof

      let X,Y be non empty set, V be RealNormSpace, g,f be PartFunc of X, the carrier of V, g1,f1 be PartFunc of Y, the carrier of V;

      assume

       A1: g = g1 & f = f1;

      

       A2: ( dom (g - f)) = (( dom g) /\ ( dom f)) by VFUNCT_1:def 2

      .= (( dom g1) /\ ( dom f1)) by A1;

      

       A3: (g - f) is PartFunc of Y, the carrier of V by A2, RELSET_1: 5;

      for c be Element of Y st c in ( dom (g - f)) holds ((g - f) /. c) = ((g1 /. c) - (f1 /. c)) by A1, VFUNCT_1:def 2;

      hence thesis by A3, A2, VFUNCT_1:def 2;

    end;

    theorem :: INTEGR18:12

    

     Th12: for r be Real, X,Y be non empty set, V be RealNormSpace, g be PartFunc of X, the carrier of V, g1 be PartFunc of Y, the carrier of V st g = g1 holds (r (#) g1) = (r (#) g)

    proof

      let r be Real, X,Y be non empty set, V be RealNormSpace, g be PartFunc of X, the carrier of V, g1 be PartFunc of Y, the carrier of V;

      assume

       A1: g = g1;

      

       A2: ( dom (r (#) g)) = ( dom g) by VFUNCT_1:def 4

      .= ( dom g1) by A1;

      

       A3: (r (#) g) is PartFunc of Y, the carrier of V by A2, RELSET_1: 5;

      for c be Element of Y st c in ( dom (r (#) g)) holds ((r (#) g) /. c) = (r * (g1 /. c)) by A1, VFUNCT_1:def 4;

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

    end;

    begin

    theorem :: INTEGR18:13

    

     Th13: for r be Real holds for A be non empty closed_interval Subset of REAL holds for f be PartFunc of REAL , the carrier of X st A c= ( dom f) & f is_integrable_on A holds (r (#) f) is_integrable_on A & ( integral ((r (#) f),A)) = (r * ( integral (f,A)))

    proof

      let r be Real;

      let A be non empty closed_interval Subset of REAL ;

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

      assume

       A1: A c= ( dom f) & f is_integrable_on A;

      

       A2: A c= ( dom (r (#) f)) by A1, VFUNCT_1:def 4;

      consider g be Function of A, the carrier of X such that

       A3: g = (f | A) & g is integrable by A1;

      

       A4: ((r (#) f) | A) = (r (#) (f | A)) by VFUNCT_1: 31

      .= (r (#) g) by A3, Th12;

      (r (#) g) is total by VFUNCT_1: 34;

      then

      reconsider gg = (r (#) g) as Function of A, the carrier of X;

      gg is integrable & ( integral gg) = (r * ( integral g)) by A3, Th4;

      hence (r (#) f) is_integrable_on A by A4;

      

      thus ( integral ((r (#) f),A)) = ( integral gg) by A4, A2, Def8

      .= (r * ( integral g)) by A3, Th4

      .= (r * ( integral (f,A))) by A3, A1, Def8;

    end;

    theorem :: INTEGR18:14

    

     Th14: for A be non empty closed_interval Subset of REAL , f1,f2 be PartFunc of REAL , the carrier of X st f1 is_integrable_on A & f2 is_integrable_on A & A c= ( dom f1) & A c= ( dom f2) holds (f1 + f2) is_integrable_on A & ( integral ((f1 + f2),A)) = (( integral (f1,A)) + ( integral (f2,A)))

    proof

      let A be non empty closed_interval Subset of REAL ;

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

      assume that

       A1: f1 is_integrable_on A & f2 is_integrable_on A and

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

      A c= (( dom f1) /\ ( dom f2)) by A2, XBOOLE_1: 19;

      then

       A3: A c= ( dom (f1 + f2)) by VFUNCT_1:def 1;

      consider g1 be Function of A, the carrier of X such that

       A4: g1 = (f1 | A) & g1 is integrable by A1;

      consider g2 be Function of A, the carrier of X such that

       A5: g2 = (f2 | A) & g2 is integrable by A1;

      ((f1 + f2) | A) = ((f1 | A) + (f2 | A)) by VFUNCT_1: 27;

      then

       A6: ((f1 + f2) | A) = (g1 + g2) by A4, A5, Th10;

      (g1 + g2) is total by VFUNCT_1: 32;

      then

      reconsider g = (g1 + g2) as Function of A, the carrier of X;

      g is integrable by Th6, A4, A5;

      hence (f1 + f2) is_integrable_on A by A6;

      

      thus ( integral ((f1 + f2),A)) = ( integral g) by Def8, A6, A3

      .= (( integral g1) + ( integral g2)) by Th6, A4, A5

      .= (( integral (f1,A)) + ( integral g2)) by A2, A4, Def8

      .= (( integral (f1,A)) + ( integral (f2,A))) by A2, A5, Def8;

    end;

    theorem :: INTEGR18:15

    for A be non empty closed_interval Subset of REAL , f1,f2 be PartFunc of REAL , the carrier of X st f1 is_integrable_on A & f2 is_integrable_on A & A c= ( dom f1) & A c= ( dom f2) holds (f1 - f2) is_integrable_on A & ( integral ((f1 - f2),A)) = (( integral (f1,A)) - ( integral (f2,A)))

    proof

      let A be non empty closed_interval Subset of REAL ;

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

      assume that

       A1: f1 is_integrable_on A & f2 is_integrable_on A and

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

      

       A3: (f1 - f2) = (f1 + ( - f2)) by VFUNCT_1: 25;

      

       A4: ( dom ( - f2)) = ( dom f2) by VFUNCT_1:def 5;

      

       A5: ( - f2) = (( - jj) (#) f2) by VFUNCT_1: 23;

      then

       A6: ( - f2) is_integrable_on A by A1, A2, Th13;

      hence (f1 - f2) is_integrable_on A by A1, A2, A3, A4, Th14;

      

      thus ( integral ((f1 - f2),A)) = ( integral ((f1 + ( - f2)),A)) by VFUNCT_1: 25

      .= (( integral (f1,A)) + ( integral (( - f2),A))) by A1, A2, A4, A6, Th14

      .= (( integral (f1,A)) + (( - jj) * ( integral (f2,A)))) by A1, A2, A5, Th13

      .= (( integral (f1,A)) + ( - ( integral (f2,A)))) by RLVECT_1: 16

      .= (( integral (f1,A)) - ( integral (f2,A))) by RLVECT_1:def 11;

    end;

    definition

      let X be RealNormSpace;

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

      let a,b be Real;

      :: INTEGR18:def9

      func integral (f,a,b) -> Element of X equals

      : Def9: ( integral (f, ['a, b'])) if a <= b

      otherwise ( - ( integral (f, ['b, a'])));

      correctness ;

    end

    theorem :: INTEGR18:16

    

     Th16: for f be PartFunc of REAL , the carrier of X, 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 f be PartFunc of REAL , the carrier of X;

      let A be non empty closed_interval Subset of REAL ;

      let a,b be Real;

      consider a1,b1 be Real such that

       A1: a1 <= b1 and

       A2: A = [.a1, b1.] by MEASURE5: 14;

      assume A = [.a, b.];

      then

       A3: a1 = a & b1 = b by A2, INTEGRA1: 5;

      then ( integral (f,a,b)) = ( integral (f, ['a, b'])) by A1, Def9;

      hence thesis by A1, A2, A3, INTEGRA5:def 3;

    end;

    theorem :: INTEGR18:17

    

     Th17: for f be PartFunc of REAL , the carrier of X, A be non empty closed_interval Subset of REAL st ( vol A) = 0 & A c= ( dom f) holds f is_integrable_on A & ( integral (f,A)) = ( 0. X)

    proof

      let f be PartFunc of REAL , the carrier of X, A be non empty closed_interval Subset of REAL ;

      assume

       A1: ( vol A) = 0 & A c= ( dom f);

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

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

      then

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

      

       A2: for T be DivSequence of A, S be middle_volume_Sequence of g, T st ( delta T) is convergent & ( lim ( delta T)) = 0 holds ( middle_sum (g,S)) is convergent & ( lim ( middle_sum (g,S))) = ( 0. X)

      proof

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

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

        

         A3: for i be Nat holds ( middle_sum (g,(S . i))) = ( 0. X)

        proof

          let i be Nat;

          

           A4: ( len (S . i)) = ( len (S . i));

          now

            let k be Nat, v be Element of X;

            assume

             A5: k in ( dom (S . i)) & v = ((S . i) . k);

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

            then k in ( Seg ( len (T . i))) by Def1;

            then

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

            then

            consider c be VECTOR of X such that

             A7: c in ( rng (g | ( divset ((T . i),k)))) & ((S . i) . k) = (( vol ( divset ((T . i),k))) * c) by Def1;

             0 <= ( vol ( divset ((T . i),k))) & ( vol ( divset ((T . i),k))) <= 0 by A1, A6, INTEGRA1: 8, INTEGRA1: 9, INTEGRA2: 38;

            then

             A8: ( vol ( divset ((T . i),k))) = 0 ;

            ((S . i) . k) = ( 0. X) by A8, A7, RLVECT_1: 10;

            hence ((S . i) . k) = ( - v) by A5, RLVECT_1: 12;

          end;

          then ( Sum (S . i)) = ( - ( Sum (S . i))) by A4, RLVECT_1: 40;

          hence thesis by RLVECT_1: 19;

        end;

        

         A9: for i be Nat holds (( middle_sum (g,S)) . i) = ( 0. X)

        proof

          let i be Nat;

          

          thus (( middle_sum (g,S)) . i) = ( middle_sum (g,(S . i))) by Def4

          .= ( 0. X) by A3;

        end;

        

         A10: for r be Real st 0 < r holds ex m be Nat st for n be Nat st m <= n holds ||.((( middle_sum (g,S)) . n) - ( 0. X)).|| < r

        proof

          let r be Real;

          assume

           A11: 0 < r;

          take m = 0 ;

          let n be Nat;

          assume m <= n;

           ||.((( middle_sum (g,S)) . n) - ( 0. X)).|| = ||.(( 0. X) - ( 0. X)).|| by A9

          .= 0 by NORMSP_1: 6;

          hence ||.((( middle_sum (g,S)) . n) - ( 0. X)).|| < r by A11;

        end;

        hence ( middle_sum (g,S)) is convergent by NORMSP_1:def 6;

        hence ( lim ( middle_sum (g,S))) = ( 0. X) by A10, NORMSP_1:def 7;

      end;

      then

       A12: g is integrable;

      hence f is_integrable_on A;

      ( integral g) = ( 0. X) by A12, A2, Def6;

      hence ( integral (f,A)) = ( 0. X) by Def8, A1;

    end;

    theorem :: INTEGR18:18

    for f be PartFunc of REAL , the carrier of X, A be non empty closed_interval Subset of REAL , a,b be Real st A = [.b, a.] & A c= ( dom f) holds ( - ( integral (f,A))) = ( integral (f,a,b))

    proof

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

      let A be non empty closed_interval Subset of REAL ;

      let a,b be Real;

      consider a1,b1 be Real such that

       A1: a1 <= b1 and

       A2: A = [.a1, b1.] by MEASURE5: 14;

      assume

       A3: A = [.b, a.] & A c= ( dom f);

      then

       A4: a1 = b & b1 = a by A2, INTEGRA1: 5;

      now

        per cases by A1, A4, XXREAL_0: 1;

          suppose

           A5: b < a;

          then ( integral (f,a,b)) = ( - ( integral (f, ['b, a']))) by Def9;

          hence thesis by A3, A5, INTEGRA5:def 3;

        end;

          suppose

           A6: b = a;

          A = [.( lower_bound A), ( upper_bound A).] by INTEGRA1: 4;

          then ( lower_bound A) = b & ( upper_bound A) = a by A3, INTEGRA1: 5;

          

          then

           A7: ( vol A) = (( upper_bound A) - ( upper_bound A)) by A6

          .= 0 ;

          

           A8: ( integral (f,a,b)) = ( integral (f,A)) by A3, A6, Th16;

          

           A9: ( - ( integral (f,a,b))) = ( - ( integral (f,A))) by A3, A6, Th16;

          ( integral (f,a,b)) = ( 0. X) by A7, A3, Th17, A8;

          hence thesis by A9, RLVECT_1: 12;

        end;

      end;

      hence thesis;

    end;