integr19.miz



    begin

    reserve X for set;

    reserve n,i for Element of NAT ;

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

    reserve A for non empty closed_interval Subset of REAL ;

    reserve f,g,h for PartFunc of REAL , ( REAL n);

    reserve E for Element of ( REAL n);

    

     Lm1: (f - g) = (f + ( - g)) by NDIFF_4: 1;

    theorem :: INTEGR19:1

    

     Th1: a <= c & c <= b implies c in ['a, b'] & ['a, c'] c= ['a, b'] & ['c, b'] c= ['a, b']

    proof

      assume that

       A1: a <= c and

       A2: c <= b;

      

       A3: c in [.a, b.] by A1, A2;

      hence c in ['a, b'] by A1, A2, INTEGRA5:def 3, XXREAL_0: 2;

      

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

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

      then

       A5: a in [.a, b.] & b in [.a, b.];

       ['a, b'] = [.a, b.] & ['a, c'] = [.a, c.] by A1, A2, INTEGRA5:def 3, XXREAL_0: 2;

      hence thesis by A4, A3, A5, XXREAL_2:def 12;

    end;

    theorem :: INTEGR19:2

    

     Th2: a <= c & c <= d & d <= b & ['a, b'] c= X implies ['c, d'] c= X

    proof

      assume that

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

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

      

       A3: ['c, d'] c= ['c, b'] by Th1, A1;

      c <= b by A1, XXREAL_0: 2;

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

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

      hence thesis by A2;

    end;

    

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

    proof

      assume

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

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

      then

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

      per cases ;

        suppose

         A3: c <= d;

        then

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

        

         A5: ['c, b'] c= ['a, b'] by A2, Th1;

         ['c, d'] c= ['c, b'] by A2, A3, Th1;

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

      end;

        suppose

         A6: not c <= d;

        then

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

        

         A8: ['d, b'] c= ['a, b'] by A2, Th1;

         ['d, c'] c= ['d, b'] by A2, A6, Th1;

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

      end;

    end;

    theorem :: INTEGR19:3

    

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

    proof

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

      then ['( min (c,d)), ( max (c,d))'] c= ['a, b'] by Lm2;

      hence thesis;

    end;

    theorem :: INTEGR19:4

    

     Th4: a <= c & c <= d & d <= b & ['a, b'] c= ( dom f) & ['a, b'] c= ( dom g) implies ['c, d'] c= ( dom (f + g))

    proof

      assume that

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

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

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

      then ( ['a, b'] /\ ['a, b']) c= ( dom (f + g)) by A2, XBOOLE_1: 27;

      hence thesis by A1, Th2;

    end;

    theorem :: INTEGR19:5

    

     Th5: a <= c & c <= d & d <= b & ['a, b'] c= ( dom f) & ['a, b'] c= ( dom g) implies ['c, d'] c= ( dom (f - g))

    proof

      assume that

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

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

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

      then ( ['a, b'] /\ ['a, b']) c= ( dom (f - g)) by A2, XBOOLE_1: 27;

      hence thesis by A1, Th2;

    end;

    

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

    proof

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

      ( rng f) c= Y;

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

      hence thesis by FUNCT_2: 32;

    end;

    theorem :: INTEGR19:6

    

     Th6: for f be PartFunc of REAL , REAL holds a <= c & c <= d & d <= b & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) implies (r (#) f) is_integrable_on ['c, d'] & ((r (#) f) | ['c, d']) is bounded

    proof

      let f be PartFunc of REAL , REAL ;

      assume that

       A1: a <= c and

       A2: c <= d & d <= b and

       A3: f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded and

       A4: ['a, b'] c= ( dom f);

      

       A5: (f | ['c, d']) is bounded by A1, A2, A3, A4, INTEGRA6: 18;

      

       A6: ['c, d'] c= ( dom f) by A2, A1, Th2, A4;

      f is_integrable_on ['c, d'] by A1, A2, A3, A4, INTEGRA6: 18;

      hence (r (#) f) is_integrable_on ['c, d'] by A5, A6, INTEGRA6: 9;

      thus thesis by A5, RFUNCT_1: 80;

    end;

    theorem :: INTEGR19:7

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

    proof

      let f,g be PartFunc of REAL , REAL ;

      assume

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

      

       A2: ((( - 1) (#) g) | ['a, b']) is bounded by A1, RFUNCT_1: 80;

      

       A3: ['a, b'] c= ( dom (( - 1) (#) g)) by A1, VALUED_1:def 5;

      (( - 1) (#) g) is_integrable_on ['a, b'] by A1, INTEGRA6: 9;

      hence thesis by A1, A2, A3, INTEGRA6: 19;

    end;

    

     Lm4: for f be PartFunc of REAL , REAL st (a <= b & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'] & for x be Real st x in ['( min (c,d)), ( max (c,d))'] holds |.(f . x).| <= e) holds |.( integral (f,c,d)).| <= (e * |.(d - c).|)

    proof

      let f be PartFunc of REAL , REAL ;

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

      assume that

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

       A2: for x be Real st x in ['( min (c,d)), ( max (c,d))'] holds |.(f . x).| <= e;

      ( rng ( abs f)) c= REAL ;

      then

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

       ['( min (c,d)), ( max (c,d))'] c= ( dom ( abs f)) by A1, INTEGRA6: 21;

      then

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

      

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

      ( abs f) is_integrable_on A by A1, INTEGRA6: 21;

      then

       A5: g is integrable;

      consider h be Function of A, REAL such that

       A6: ( rng h) = {e} and

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

       A8:

      now

        let x be Real;

        assume

         A9: x in A;

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

        then

         A10: (g . x) = |.(f . x).| by VALUED_1: 18;

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

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

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

      end;

      

       A11: |.( integral (f,c,d)).| <= ( integral (( abs f),( min (c,d)),( max (c,d)))) by A1, INTEGRA6: 21;

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

      then ( min (c,d)) <= ( max (c,d)) by XXREAL_0: 2;

      then

       A12: ( integral (( abs f),( min (c,d)),( max (c,d)))) = ( integral (( abs f),A)) by INTEGRA5:def 4;

      (( abs f) | A) is bounded by A1, INTEGRA6: 21;

      then

       A13: (g | A) is bounded;

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

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

      hence thesis by A11, XXREAL_0: 2;

    end;

    

     Lm5: for f be PartFunc of REAL , REAL st A c= ( dom f) holds (f | A) is Function of A, REAL by Lm3;

    theorem :: INTEGR19:8

    a <= b & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] implies f is_integrable_on ['a, c'] & f is_integrable_on ['c, b'] & ( integral (f,a,b)) = (( integral (f,a,c)) + ( integral (f,c,b)))

    proof

      assume

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

       A2:

      now

        let i;

        set P = ( proj (i,n));

        assume

         A3: i in ( Seg n);

        then

         A4: (P * f) is_integrable_on ['a, b'] by A1;

        (P * (f | ['a, b'])) is bounded by A3, A1;

        then

         A5: ((P * f) | ['a, b']) is bounded by RELAT_1: 83;

        ( dom P) = ( REAL n) by FUNCT_2:def 1;

        then ( rng f) c= ( dom P);

        then ( dom (P * f)) = ( dom f) by RELAT_1: 27;

        hence (P * f) is_integrable_on ['a, c'] & (P * f) is_integrable_on ['c, b'] & ( integral ((P * f),a,b)) = (( integral ((P * f),a,c)) + ( integral ((P * f),c,b))) by A4, A5, A1, INTEGRA6: 17;

      end;

      then for i be Element of NAT st i in ( Seg n) holds (( proj (i,n)) * f) is_integrable_on ['a, c'];

      hence f is_integrable_on ['a, c'];

      for i be Element of NAT st i in ( Seg n) holds (( proj (i,n)) * f) is_integrable_on ['c, b'] by A2;

      hence f is_integrable_on ['c, b'];

       A6:

      now

        let i be Nat;

        assume i in ( dom ( integral (f,a,b)));

        then

         A7: i in ( Seg n) by INTEGR15:def 18;

        set P = ( proj (i,n));

        

        thus (( integral (f,a,b)) . i) = ( integral ((P * f),a,b)) by A7, INTEGR15:def 18

        .= (( integral ((P * f),a,c)) + ( integral ((P * f),c,b))) by A7, A2

        .= ((( integral (f,a,c)) . i) + ( integral ((P * f),c,b))) by A7, INTEGR15:def 18

        .= ((( integral (f,a,c)) . i) + (( integral (f,c,b)) . i)) by A7, INTEGR15:def 18

        .= ((( integral (f,a,c)) + ( integral (f,c,b))) . i) by RVSUM_1: 11;

      end;

      

       A8: ( Seg n) = ( dom ( integral (f,a,b))) by INTEGR15:def 18;

      ( len (( integral (f,a,c)) + ( integral (f,c,b)))) = n by CARD_1:def 7;

      then ( Seg n) = ( dom (( integral (f,a,c)) + ( integral (f,c,b)))) by FINSEQ_1:def 3;

      hence thesis by A8, A6, FINSEQ_1: 13;

    end;

    theorem :: INTEGR19:9

    

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

    proof

      assume

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

       A2:

      now

        let i;

        set P = ( proj (i,n));

        assume

         A3: i in ( Seg n);

        then

         A4: (P * f) is_integrable_on ['a, b'] by A1;

        (P * (f | ['a, b'])) is bounded by A3, A1;

        then

         A5: ((P * f) | ['a, b']) is bounded by RELAT_1: 83;

        ( dom P) = ( REAL n) by FUNCT_2:def 1;

        then ( rng f) c= ( dom P);

        then ( dom (P * f)) = ( dom f) by RELAT_1: 27;

        then (P * f) is_integrable_on ['c, d'] & ((P * f) | ['c, d']) is bounded & ['c, d'] c= ( dom (P * f)) by A4, A5, A1, INTEGRA6: 18;

        hence (P * f) is_integrable_on ['c, d'] & (P * (f | ['c, d'])) is bounded by RELAT_1: 83;

      end;

      then for i be Element of NAT st i in ( Seg n) holds (( proj (i,n)) * f) is_integrable_on ['c, d'];

      hence f is_integrable_on ['c, d'];

      for i be Element of NAT st i in ( Seg n) holds (( proj (i,n)) * (f | ['c, d'])) is bounded by A2;

      hence thesis;

    end;

    theorem :: INTEGR19:10

    

     Th10: a <= c & c <= d & d <= b & f is_integrable_on ['a, b'] & g is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & (g | ['a, b']) is bounded & ['a, b'] c= ( dom f) & ['a, b'] c= ( dom g) implies (f + g) is_integrable_on ['c, d'] & ((f + g) | ['c, d']) is bounded

    proof

      assume that

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

       A2: f is_integrable_on ['a, b'] & g is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & (g | ['a, b']) is bounded and

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

       A4:

      now

        let i;

        set P = ( proj (i,n));

        assume

         A5: i in ( Seg n);

        then

         A6: (P * f) is_integrable_on ['a, b'] by A2;

        (P * (f | ['a, b'])) is bounded by A5, A2;

        then

         A7: ((P * f) | ['a, b']) is bounded by RELAT_1: 83;

        

         A8: ( dom P) = ( REAL n) by FUNCT_2:def 1;

        then ( rng f) c= ( dom P);

        then

         A9: ( dom (P * f)) = ( dom f) by RELAT_1: 27;

        

         A10: (P * g) is_integrable_on ['a, b'] by A5, A2;

        (P * (g | ['a, b'])) is bounded by A5, A2;

        then

         A11: ((P * g) | ['a, b']) is bounded by RELAT_1: 83;

        ( rng g) c= ( dom P) by A8;

        then ( dom (P * g)) = ( dom g) by RELAT_1: 27;

        then

         A12: ((P * f) + (P * g)) is_integrable_on ['c, d'] & (((P * f) + (P * g)) | ['c, d']) is bounded by A1, A3, A6, A7, A9, A10, A11, INTEGRA6: 19;

        (((P * f) + (P * g)) | ['c, d']) = ((P * (f + g)) | ['c, d']) by INTEGR15: 15

        .= (P * ((f + g) | ['c, d'])) by RELAT_1: 83;

        hence (P * (f + g)) is_integrable_on ['c, d'] & (P * ((f + g) | ['c, d'])) is bounded by A12, INTEGR15: 15;

      end;

      then for i be Element of NAT st i in ( Seg n) holds (( proj (i,n)) * (f + g)) is_integrable_on ['c, d'];

      hence (f + g) is_integrable_on ['c, d'];

      for i be Element of NAT st i in ( Seg n) holds (( proj (i,n)) * ((f + g) | ['c, d'])) is bounded by A4;

      hence thesis;

    end;

    theorem :: INTEGR19:11

    

     Th11: a <= c & c <= d & d <= b & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) implies (r (#) f) is_integrable_on ['c, d'] & ((r (#) f) | ['c, d']) is bounded

    proof

      assume that

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

       A2: f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded and

       A3: ['a, b'] c= ( dom f);

       A4:

      now

        let i;

        set P = ( proj (i,n));

        assume

         A5: i in ( Seg n);

        then

         A6: (P * f) is_integrable_on ['a, b'] by A2;

        (P * (f | ['a, b'])) is bounded by A5, A2;

        then

         A7: ((P * f) | ['a, b']) is bounded by RELAT_1: 83;

        ( dom P) = ( REAL n) by FUNCT_2:def 1;

        then ( rng f) c= ( dom P);

        then

         A8: ( dom (P * f)) = ( dom f) by RELAT_1: 27;

        

         A9: (r (#) (P * f)) is_integrable_on ['c, d'] & ((r (#) (P * f)) | ['c, d']) is bounded by A1, A3, Th6, A6, A7, A8;

        ((r (#) (P * f)) | ['c, d']) = ((P * (r (#) f)) | ['c, d']) by INTEGR15: 16

        .= (P * ((r (#) f) | ['c, d'])) by RELAT_1: 83;

        hence (P * (r (#) f)) is_integrable_on ['c, d'] & (P * ((r (#) f) | ['c, d'])) is bounded by A9, INTEGR15: 16;

      end;

      then for i be Element of NAT st i in ( Seg n) holds (( proj (i,n)) * (r (#) f)) is_integrable_on ['c, d'];

      hence (r (#) f) is_integrable_on ['c, d'];

      for i be Element of NAT st i in ( Seg n) holds (( proj (i,n)) * ((r (#) f) | ['c, d'])) is bounded by A4;

      hence thesis;

    end;

    theorem :: INTEGR19:12

    

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

    proof

      ( - f) = (( - 1) (#) f) by NFCONT_4: 7;

      hence thesis by Th11;

    end;

    theorem :: INTEGR19:13

    

     Th13: a <= c & c <= d & d <= b & f is_integrable_on ['a, b'] & g is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & (g | ['a, b']) is bounded & ['a, b'] c= ( dom f) & ['a, b'] c= ( dom g) implies (f - g) is_integrable_on ['c, d'] & ((f - g) | ['c, d']) is bounded

    proof

      assume that

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

       A2: f is_integrable_on ['a, b'] & g is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & (g | ['a, b']) is bounded and

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

      

       A4: ( dom g) = ( dom ( - g)) by NFCONT_4:def 3;

      

       A5: (f - g) = (f + ( - g)) by Lm1;

      a <= d by A1, XXREAL_0: 2;

      then a <= b by A1, XXREAL_0: 2;

      then ( - g) is_integrable_on ['a, b'] & (( - g) | ['a, b']) is bounded by A2, A3, Th12;

      hence thesis by A5, A1, A2, A3, A4, Th10;

    end;

    theorem :: INTEGR19:14

    

     Th14: for n be non zero Element of NAT , f be Function of A, ( REAL n) holds f is bounded iff |.f.| is bounded

    proof

      let n be non zero Element of NAT , f be Function of A, ( REAL n);

      hereby

        assume

         A1: f is bounded;

        defpred YX[ Nat, set] means ex K be Element of REAL st 0 <= K & K = $2 & for y be set st y in ( dom (( proj ($1,n)) * f)) holds |.((( proj ($1,n)) * f) . y).| < K;

        

         A2: for i be Nat st i in ( Seg n) holds ex r be Element of REAL st YX[i, r]

        proof

          let i be Nat;

          assume

           A3: i in ( Seg n);

          set P = ( proj (i,n));

          (P * f) is bounded by A1, A3;

          then

          consider L be Real such that

           A4: for y be set st y in ( dom (P * f)) holds |.((P * f) . y).| < L by COMSEQ_2:def 3;

          reconsider r = |.L.| as Element of REAL by XREAL_0:def 1;

          take r;

          now

            let y be set;

            assume

             A5: y in ( dom (P * f));

            L <= r by ABSVALUE: 4;

            hence |.((( proj (i,n)) * f) . y).| < r by A4, A5, XXREAL_0: 2;

          end;

          hence thesis by COMPLEX1: 46;

        end;

        consider w be FinSequence of REAL such that

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

         A7:

        now

          let i;

          set P = ( proj (i,n));

          assume i in ( Seg n);

          then YX[i, (w . i)] by A6;

          hence 0 <= (w . i) & for y be set st y in ( dom (P * f)) holds |.((P * f) . y).| < (w . i);

        end;

        ( len w) = n by A6, FINSEQ_1:def 3;

        then

        reconsider w as Element of ( REAL n) by FINSEQ_2: 92;

        

         A8: for i be Nat st i in ( Seg n) holds 0 <= (w . i) by A7;

        set KK = ( Sum w);

        for y be set st y in ( dom |.f.|) holds |.( |.f.| . y).| < ((n * KK) + 1)

        proof

          let y be set;

          assume

           A9: y in ( dom |.f.|);

          

          then

           A10: ( |.f.| . y) = ( |.f.| /. y) by PARTFUN1:def 6

          .= |.(f /. y).| by A9, NFCONT_4:def 2;

          then

           A11: |.( |.f.| . y).| = ( |.f.| . y) by ABSVALUE:def 1;

          now

            let i;

            set P = ( proj (i,n));

            assume

             A12: 1 <= i & i <= n;

            

             A13: y in ( dom f) by A9, NFCONT_4:def 2;

            then (f . y) in ( rng f) by FUNCT_1: 3;

            then (f . y) in ( REAL n);

            then (f . y) in ( dom P) by FUNCT_2:def 1;

            then

             A14: y in ( dom (P * f)) by A13, FUNCT_1: 11;

            

             A15: i in ( Seg n) by A12;

            then |.((P * f) . y).| < (w . i) by A7, A14;

            then |.(P . (f . y)).| < (w . i) by A14, FUNCT_1: 12;

            then

             A16: |.(P . (f /. y)).| < (w . i) by A13, PARTFUN1:def 6;

            (w . i) <= ( Sum w) by A8, A15, REAL_NS1: 7;

            hence |.(P . (f /. y)).| <= KK by A16, XXREAL_0: 2;

          end;

          then |.(f /. y).| <= (n * KK) by PDIFF_8: 17;

          then ( 0 qua Real + |.( |.f.| . y).|) < ((n * KK) + 1) by A10, A11, XREAL_1: 8;

          hence thesis;

        end;

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

      end;

      assume |.f.| is bounded;

      then

      consider K be Real such that

       A17: for y be set st y in ( dom |.f.|) holds |.( |.f.| . y).| < K by COMSEQ_2:def 3;

      let i;

      set P = ( proj (i,n));

      assume

       A18: i in ( Seg n);

      for y be set st y in ( dom (P * f)) holds |.((P * f) . y).| < K

      proof

        let y be set;

        assume

         A19: y in ( dom (P * f));

        then

         A20: y in ( dom f) by FUNCT_1: 11;

        

         A21: ((P * f) . y) = (P . (f . y)) by A19, FUNCT_1: 12

        .= (P . (f /. y)) by A20, PARTFUN1:def 6;

        1 <= i & i <= n by A18, FINSEQ_1: 1;

        then

         A22: |.(P . (f /. y)).| <= |.(f /. y).| by PDIFF_8: 5;

        

         A23: y in ( dom |.f.|) by A20, NFCONT_4:def 2;

        then |.( |.f.| . y).| < K by A17;

        then |.( |.f.| /. y).| < K by A23, PARTFUN1:def 6;

        then |. |.(f /. y).|.| < K by A23, NFCONT_4:def 2;

        then |.(f /. y).| < K by ABSVALUE:def 1;

        hence |.((P * f) . y).| < K by A21, A22, XXREAL_0: 2;

      end;

      hence (P * f) is bounded by COMSEQ_2:def 3;

    end;

    

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

    proof

      defpred P[ Nat] means for p be FinSequence of ( REAL n), r be Element of ( REAL n) st ( len p) = $1 & (for i be Element of NAT st i in ( Seg n) holds ex Pi be FinSequence of REAL st Pi = (( proj (i,n)) * p) & (r . i) = ( Sum Pi)) holds r = ( Sum p);

      

       A1: P[ 0 ]

      proof

        let p be FinSequence of ( REAL n), r be Element of ( REAL n);

        assume

         A2: ( len p) = 0 & (for i be Element of NAT st i in ( Seg n) holds ex Pi be FinSequence of REAL st Pi = (( proj (i,n)) * p) & (r . i) = ( Sum Pi));

        

         A3: p = {} by A2;

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

        then

         A4: ( dom r) = ( Seg n) by FINSEQ_1:def 3;

        

         A5: ( dom (( Seg n) --> 0 )) = ( Seg n) by FUNCOP_1: 13;

         A6:

        now

          let x be object;

          assume

           A7: x in ( dom r);

          then

          reconsider i = x as Element of NAT ;

          set P = ( proj (i,n));

          consider Pi be FinSequence of REAL such that

           A8: Pi = (P * p) & (r . i) = ( Sum Pi) by A2, A4, A7;

          (r . x) = 0 by A3, A8, RVSUM_1: 72;

          hence (r . x) = ((( Seg n) --> 0 ) . x) by A4, A7, FUNCOP_1: 7;

        end;

        ( Sum p) = ( 0* n) by A2, EUCLID_7:def 11;

        hence r = ( Sum p) by A6, A4, A5, FUNCT_1: 2;

      end;

      

       A9: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         A10: P[k];

        now

          let p be FinSequence of ( REAL n), r be Element of ( REAL n);

          assume

           A11: ( len p) = (k + 1) & (for i be Element of NAT st i in ( Seg n) holds ex Pi be FinSequence of REAL st Pi = (( proj (i,n)) * p) & (r . i) = ( Sum Pi));

          set p1 = (p | k);

          (k + 1) in ( Seg (k + 1)) by FINSEQ_1: 4;

          then (k + 1) in ( dom p) by A11, FINSEQ_1:def 3;

          then (p . (k + 1)) in ( rng p) by FUNCT_1: 3;

          then

          reconsider pk1 = (p . (k + 1)) as Element of ( REAL n);

          defpred YX[ Nat, set] means ex P1i be FinSequence of REAL st P1i = (( proj ($1,n)) * p1) & $2 = ( Sum P1i);

          

           A12: for i be Nat st i in ( Seg n) holds ex r be Element of REAL st YX[i, r]

          proof

            let i be Nat;

            assume i in ( Seg n);

            reconsider S = ( Sum (( proj (i,n)) * p1)) as Element of REAL by XREAL_0:def 1;

            take S;

            thus thesis;

          end;

          consider r1 be FinSequence of REAL such that

           A13: ( dom r1) = ( Seg n) & for i be Nat st i in ( Seg n) holds YX[i, (r1 . i)] from FINSEQ_1:sch 5( A12);

          ( len r1) = n by A13, FINSEQ_1:def 3;

          then

          reconsider r1 as Element of ( REAL n) by FINSEQ_2: 92;

          

           A14: for i st i in ( Seg n) holds ex P1i be FinSequence of REAL st P1i = (( proj (i,n)) * p1) & (r1 . i) = ( Sum P1i) by A13;

          

           A15: k <= ( len p) by A11, NAT_1: 16;

          then

           A16: ( len p1) = k by FINSEQ_1: 59;

          

           A17: ( len r) = n by CARD_1:def 7;

          

           A18: ( len (r1 + pk1)) = n by CARD_1:def 7;

          now

            let i be Nat;

            set P = ( proj (i,n));

            assume 1 <= i & i <= n;

            then

             A19: i in ( Seg n);

            consider Pi be FinSequence of REAL such that

             A20: Pi = (P * p) & (r . i) = ( Sum Pi) by A19, A11;

            consider P1i be FinSequence of REAL such that

             A21: P1i = (P * p1) & (r1 . i) = ( Sum P1i) by A19, A13;

            

             A22: ( dom P) = ( REAL n) by FUNCT_2:def 1;

            then

             A23: ( rng p) c= ( dom P);

            

             A24: ( dom Pi) = ( dom p) by A23, A20, RELAT_1: 27

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

            

             A25: ( len p) = (( len p1) + ( len <*(pk1 . i)*>)) by A11, A16, FINSEQ_1: 40;

            

             A26: ( rng p1) c= ( dom P) by A22;

            

             A27: ( dom P1i) = ( dom p1) by A26, A21, RELAT_1: 27

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

            then

             A28: ( len P1i) = ( len p1) by FINSEQ_1:def 3;

            

             A29: ( dom Pi) = ( Seg (( len P1i) + ( len <*(pk1 . i)*>))) by A24, A25, A27, FINSEQ_1:def 3;

            ( len p1) <= ( len p) by A15, FINSEQ_1: 59;

            then

             A30: ( Seg ( len p1)) c= ( Seg ( len p)) by FINSEQ_1: 5;

            

             A31: for k be Nat st k in ( dom P1i) holds (Pi . k) = (P1i . k)

            proof

              let k be Nat;

              assume

               A32: k in ( dom P1i);

              then

               A33: k in ( dom p1) by A27, FINSEQ_1:def 3;

              

              thus (P1i . k) = (P . (p1 . k)) by A21, A32, FUNCT_1: 12

              .= (P . (p . k)) by A33, FUNCT_1: 47

              .= (Pi . k) by A20, A32, A24, A27, A30, FUNCT_1: 12;

            end;

            for k be Nat st k in ( dom <*(pk1 . i)*>) holds (Pi . (( len P1i) + k)) = ( <*(pk1 . i)*> . k)

            proof

              let j be Nat;

              assume j in ( dom <*(pk1 . i)*>);

              then j in ( Seg ( len <*(pk1 . i)*>)) by FINSEQ_1:def 3;

              then j in ( Seg 1) by FINSEQ_1: 40;

              then

               A34: j = 1 by FINSEQ_1: 2, TARSKI:def 1;

              

              hence (Pi . (( len P1i) + j)) = (P . (p . (k + 1))) by A20, A24, A11, A28, A16, FINSEQ_1: 4, FUNCT_1: 12

              .= (pk1 . i) by PDIFF_1:def 1

              .= ( <*(pk1 . i)*> . j) by A34, FINSEQ_1: 40;

            end;

            then Pi = (P1i ^ <*(pk1 . i)*>) by A31, A29, FINSEQ_1:def 7;

            

            hence (r . i) = ((r1 . i) + (pk1 . i)) by A20, A21, RVSUM_1: 74

            .= ((r1 + pk1) . i) by RVSUM_1: 11;

          end;

          then

           A35: r = (r1 + pk1) by A17, A18;

          ex v be Element of ( REAL n) st v = (p . ( len p)) & ( Sum p) = (( Sum p1) + v) by A16, A11, PDIFF_6: 15;

          hence r = ( Sum p) by A11, A35, A10, A14, A16;

        end;

        hence P[(k + 1)];

      end;

      

       A36: for k be Nat holds P[k] from NAT_1:sch 2( A1, A9);

      let p be FinSequence of ( REAL n);

      assume

       A37: for i be Element of NAT st i in ( Seg n) holds ex Pi be FinSequence of REAL st Pi = (( proj (i,n)) * p) & (E . i) = ( Sum Pi);

      ( len p) = ( len p);

      hence thesis by A37, A36;

    end;

    

     Lm7: for p be FinSequence of ( REAL n), q be FinSequence of REAL st ( len p) = ( len q) & (for j be Nat st j in ( dom p) holds |.(p /. j).| <= (q /. j)) & (for i be Element of NAT st i in ( Seg n) holds ex Pi be FinSequence of REAL st Pi = (( proj (i,n)) * p) & (E . i) = ( Sum Pi)) holds |.E.| <= ( Sum q)

    proof

      let p be FinSequence of ( REAL n), q be FinSequence of REAL ;

      assume

       A1: ( len p) = ( len q) & (for j be Nat st j in ( dom p) holds |.(p /. j).| <= (q /. j)) & (for i be Element of NAT st i in ( Seg n) holds ex Pi be FinSequence of REAL st Pi = (( proj (i,n)) * p) & (E . i) = ( Sum Pi));

      then

       A2: E = ( Sum p) by Lm6;

      defpred P1[ Nat, set] means ex v be Element of ( REAL n) st v = (p . $1) & $2 = |.v.|;

      

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

      proof

        let i be Nat;

        assume i in ( Seg ( len p));

        then

         A4: i in ( dom p) by FINSEQ_1:def 3;

        reconsider w = |.(p /. i).| as Element of REAL by XREAL_0:def 1;

        take w;

        thus thesis by A4, PARTFUN1:def 6;

      end;

      consider u be FinSequence of REAL such that

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

      

       A6: for i be Nat st i in ( dom p) holds ex v be Element of ( REAL n) st v = (p . i) & (u . i) = |.v.|

      proof

        let i be Nat;

        assume i in ( dom p);

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

        hence ex v be Element of ( REAL n) st v = (p . i) & (u . i) = |.v.| by A5;

      end;

      

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

      then

       A8: |.( Sum p).| <= ( Sum u) by A6, PDIFF_6: 17;

      set i = ( len p);

      reconsider uu = u as Element of (i -tuples_on REAL ) by A7, FINSEQ_2: 92;

      reconsider qq = q as Element of (i -tuples_on REAL ) by A1, FINSEQ_2: 92;

      now

        let j be Nat;

        assume

         A9: j in ( Seg i);

        then

         A10: j in ( dom p) by FINSEQ_1:def 3;

        then

         A11: |.(p /. j).| <= (q /. j) by A1;

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

        then

         A12: (q /. j) = (q . j) by PARTFUN1:def 6;

        ex v be Element of ( REAL n) st v = (p . j) & (u . j) = |.v.| by A6, A10;

        hence (uu . j) <= (qq . j) by A11, A12, A10, PARTFUN1:def 6;

      end;

      then ( Sum uu) <= ( Sum qq) by RVSUM_1: 82;

      hence thesis by A2, A8, XXREAL_0: 2;

    end;

    

     Lm8: for n be non zero Element of NAT , h be Function of A, ( REAL n), f be Function of A, REAL st h is bounded & h is integrable & f = |.h.| & f is integrable holds |.( integral h).| <= ( integral f)

    proof

      let n be non zero Element of NAT , h be Function of A, ( REAL n), f be Function of A, REAL ;

      assume

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

      then

       A2: f is bounded by Th14;

      consider T be DivSequence of A such that

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

      set S = the middle_volume_Sequence of h, T;

      

       A4: ( dom f) = ( dom h) by A1, NFCONT_4:def 2;

      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 Element of ( REAL n) 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 Element of ( REAL n) 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 Element of ( REAL n) such that

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

          consider x be object such that

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

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

          then

          reconsider x as Element of REAL ;

          take x;

          thus thesis by A8, A9;

        end;

        consider p be FinSequence of REAL such that

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

        take p;

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

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

      end;

      consider F be sequence of ( REAL * ) such that

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

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

      

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

      proof

        let k be Element of NAT ;

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

        

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

        

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

        proof

          let i be Nat;

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

          then

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

          consider p be FinSequence of REAL such that

           A16: p = (F . k) & ( len p) = ( len (T . k)) & for i be Nat st i in ( dom (T . k)) holds (p . i) in ( dom (h | ( divset ((T . k),i)))) & ex z be Element of ( REAL n) 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 (p . i) in ( dom h) & (p . i) in ( divset ((T . k),i)) by RELAT_1: 57;

          then

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

          

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

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

          hence thesis by A16, A17, A18;

        end;

        consider q be FinSequence of REAL 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 Element of REAL 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 Element of REAL st c in ( rng (f | ( divset ((T . k),i)))) & (q . i) = (c * ( vol ( divset ((T . k),i)))) by A21, FUNCT_1: 3;

        end;

        then

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

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

        hence thesis by A13, A19;

      end;

      consider Sf be sequence of ( REAL * ) 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 Element of REAL st ((F . k) . i) in ( dom (f | ( divset ((T . k),i)))) & z = ((f | ( divset ((T . k),i))) . ((F . k) . i)) & (q . i) = (( vol ( divset ((T . k),i))) * z) by A22;

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

      end;

      then

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

      

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

      

       A24: ( middle_sum (h,S)) is convergent & ( lim ( middle_sum (h,S))) = ( integral h) by A1, A3, INTEGR15: 11;

      

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

      proof

        let k be Element of NAT ;

        

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

        .= ( Sum (Sf . k));

        

         A27: (( middle_sum (h,S)) . k) = ( middle_sum (h,(S . k))) by INTEGR15:def 8;

        

         A28: for i be Element of NAT st i in ( Seg n) holds ex Pi be FinSequence of REAL st Pi = (( proj (i,n)) * (S . k)) & (( middle_sum (h,(S . k))) . i) = ( Sum Pi) by INTEGR15:def 6;

        

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

        

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

        

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

        

         A32: ( len (S . k)) = ( len (T . k)) by INTEGR15:def 5;

        now

          let i be Nat;

          assume

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

          then

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

          then

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

          

           A36: i in ( dom (Sf . k)) by A31, A34, FINSEQ_1:def 3;

          

           A37: ((F . k) . i) in ( dom (h | ( divset ((T . k),i)))) by A35, A29;

          consider z be Element of ( REAL n) such that

           A38: z = ((h | ( divset ((T . k),i))) . ((F . k) . i)) & ((S . k) . i) = (( vol ( divset ((T . k),i))) * z) by A29, A35;

          consider w be Element of REAL such that

           A39: ((F . k) . i) in ( dom (f | ( divset ((T . k),i)))) & w = ((f | ( divset ((T . k),i))) . ((F . k) . i)) & ((Sf . k) . i) = (( vol ( divset ((T . k),i))) * w) by A30, A35;

          

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

          

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

          

           A42: |.((S . k) /. i).| = ( |.( vol ( divset ((T . k),i))).| * |.z.|) by A38, A40, EUCLID: 11

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

          

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

          

           A44: ((h | ( divset ((T . k),i))) . ((F . k) . i)) = (h . ((F . k) . i)) by A37, FUNCT_1: 47

          .= (h /. ((F . k) . i)) by A43, A37, PARTFUN1:def 6;

          

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

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

          .= ( |.h.| /. ((F . k) . i)) by A45, A1, A39, PARTFUN1:def 6

          .= |.(h /. ((F . k) . i)).| by A45, A1, A39, NFCONT_4:def 2;

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

        end;

        then |.( middle_sum (h,(S . k))).| <= ( Sum (Sf . k)) by Lm7, A28, A31, A32;

        hence thesis by A26, A27, REAL_NS1: 1;

      end;

       A46:

      now

        let i be Nat;

        

         A47: i in NAT by ORDINAL1:def 12;

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

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

      end;

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

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

      then ||.( lim ( middle_sum (h,S))).|| <= ( lim ( middle_sum (f,Sf))) by A24, LOPBAN_1: 41;

      hence thesis by A23, A1, A3, INTEGR15: 11, REAL_NS1: 1;

    end;

    

     Lm9: A c= ( dom h) implies (h | A) is Function of A, ( REAL n) by Lm3;

    theorem :: INTEGR19:15

    f is bounded & A c= ( dom f) implies (f | A) is bounded

    proof

      assume

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

      let i;

      set P = ( proj (i,n));

      assume i in ( Seg n);

      then (P * f) is bounded by A1;

      then

      consider r be Real such that

       A2: for c be object st c in ( dom (P * f)) holds |.((P * f) . c).| <= r by RFUNCT_1: 72;

      now

        let c be object;

        assume c in (A /\ ( dom (P * f)));

        then c in ( dom (P * f)) by XBOOLE_0:def 4;

        hence |.((P * f) . c).| <= r by A2;

      end;

      then ((P * f) | A) is bounded by RFUNCT_1: 73;

      hence (P * (f | A)) is bounded by RELAT_1: 83;

    end;

    theorem :: INTEGR19:16

    

     Th16: for f be PartFunc of REAL , ( REAL n), g be Function of A, ( REAL n) st f is bounded & f = g holds g is bounded;

    theorem :: INTEGR19:17

    

     Th17: for f be PartFunc of REAL , ( REAL n), g be Function of A, ( REAL n) st f = g holds |.f.| = |.g.|

    proof

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

      assume

       A1: f = g;

      

       A2: ( dom |.f.|) = ( dom f) by NFCONT_4:def 2

      .= ( dom |.g.|) by A1, NFCONT_4:def 2;

      now

        let x be object;

        assume

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

        

        thus ( |.f.| . x) = ( |.f.| /. x) by A3, PARTFUN1:def 6

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

        .= ( |.g.| /. x) by A1, A2, A3, NFCONT_4:def 2

        .= ( |.g.| . x) by A2, A3, PARTFUN1:def 6;

      end;

      hence thesis by A2, FUNCT_1: 2;

    end;

    theorem :: INTEGR19:18

    

     Th18: A c= ( dom h) implies |.(h | A).| = ( |.h.| | A)

    proof

      assume

       A1: A c= ( dom h);

      

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

      

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

      .= (( dom h) /\ A) by NFCONT_4:def 2

      .= A by A1, XBOOLE_1: 28;

      

       A4: ( dom |.(h | A).|) = ( dom ( |.h.| | A)) by A3, A2, NFCONT_4:def 2;

      now

        let x be object;

        assume

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

        then

         A6: x in (( dom |.h.|) /\ A) by RELAT_1: 61;

        then

         A7: x in (( dom h) /\ A) by NFCONT_4:def 2;

        then

         A8: x in ( dom (h | A)) by RELAT_1: 61;

        

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

        

         A10: x in ( dom h) by A7, XBOOLE_0:def 4;

        

         A11: (h /. x) = (h . x) by A10, PARTFUN1:def 6

        .= ((h | A) . x) by A8, FUNCT_1: 47

        .= ((h | A) /. x) by A8, PARTFUN1:def 6;

        

        thus (( |.h.| | A) . x) = ( |.h.| . x) by A6, FUNCT_1: 48

        .= ( |.h.| /. x) by A9, PARTFUN1:def 6

        .= |.(h /. x).| by A9, NFCONT_4:def 2

        .= ( |.(h | A).| /. x) by A11, A4, A5, NFCONT_4:def 2

        .= ( |.(h | A).| . x) by A4, A5, PARTFUN1:def 6;

      end;

      hence thesis by A4, FUNCT_1: 2;

    end;

    theorem :: INTEGR19:19

    

     Th19: for n be non zero Element of NAT , h be PartFunc of REAL , ( REAL n) st A c= ( dom h) & (h | A) is bounded holds ( |.h.| | A) is bounded

    proof

      let n be non zero Element of NAT , h be PartFunc of REAL , ( REAL n);

      assume

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

      

       A2: |.(h | A).| = ( |.h.| | A) by Th18, A1;

      reconsider g = (h | A) as Function of A, ( REAL n) by A1, Lm9;

      g is bounded by A1;

      then |.g.| is bounded by Th14;

      hence thesis by A2, Th17;

    end;

    theorem :: INTEGR19:20

    

     Th20: for n be non zero Element of NAT , h be PartFunc of REAL , ( REAL n) st A c= ( dom h) & (h | A) is bounded & h is_integrable_on A & |.h.| is_integrable_on A holds |.( integral (h,A)).| <= ( integral ( |.h.|,A))

    proof

      let n be non zero Element of NAT , h be PartFunc of REAL , ( REAL n);

      assume

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

      set f = |.h.|;

      reconsider hA = (h | A) as Function of A, ( REAL n) by A1, Lm9;

      

       A2: ( integral (h,A)) = ( integral hA) by INTEGR15: 14;

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

      then

      reconsider fA = (f | A) as Function of A, REAL by Lm5;

      

       A3: fA is integrable by A1;

      

       A4: hA is integrable by A1, INTEGR15: 13;

       |.hA.| = |.(h | A).| by Th17

      .= (f | A) by Th18, A1;

      hence thesis by A2, A3, A4, A1, Th16, Lm8;

    end;

    theorem :: INTEGR19:21

    

     Th21: for n be non zero Element of NAT , h be PartFunc of REAL , ( REAL n) st a <= b & ['a, b'] c= ( dom h) & h is_integrable_on ['a, b'] & |.h.| is_integrable_on ['a, b'] & (h | ['a, b']) is bounded holds |.( integral (h,a,b)).| <= ( integral ( |.h.|,a,b))

    proof

      let n be non zero Element of NAT , h be PartFunc of REAL , ( REAL n);

      assume

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

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

      then

       A2: ( integral (h,a,b)) = ( integral (h, ['a, b'])) by INTEGR15: 19;

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

      hence thesis by Th20, A1, A2;

    end;

    

     Lm10: for n be non zero Element of NAT holds for f be PartFunc of REAL , ( REAL n) st a <= b & c <= d & f is_integrable_on ['a, b'] & |.f.| is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'] holds f is_integrable_on ['c, d'] & |.f.| is_integrable_on ['c, d'] & ( |.f.| | ['c, d']) is bounded & |.( integral (f,c,d)).| <= ( integral ( |.f.|,c,d))

    proof

      let n be non zero Element of NAT , f be PartFunc of REAL , ( REAL n) such that

       A1: a <= b and

       A2: c <= d and

       A3: f is_integrable_on ['a, b'] & |.f.| is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) and

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

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

      then

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

      then

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

      

       A7: ['c, d'] c= ( dom f) & f is_integrable_on ['c, d'] by A2, A3, A5, Th9, Th2;

      

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

      ( |.f.| | ['a, b']) is bounded by A3, Th19;

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

      hence thesis by A2, A6, A7, Th21, Th19;

    end;

    theorem :: INTEGR19:22

    

     Th22: for n be non zero Element of NAT , f be PartFunc of REAL , ( REAL n) st a <= b & f is_integrable_on ['a, b'] & |.f.| is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'] holds |.f.| is_integrable_on ['( min (c,d)), ( max (c,d))'] & ( |.f.| | ['( min (c,d)), ( max (c,d))']) is bounded & |.( integral (f,c,d)).| <= ( integral ( |.f.|,( min (c,d)),( max (c,d))))

    proof

      let n be non zero Element of NAT , f be PartFunc of REAL , ( REAL n);

      assume

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

      per cases ;

        suppose

         A2: not c <= d;

        then

         A3: ['d, c'] = [.d, c.] by INTEGRA5:def 3;

        then ( integral (f,c,d)) = ( - ( integral (f, ['d, c']))) by INTEGR15: 20;

        then ( integral (f,c,d)) = ( - ( integral (f,d,c))) by A3, INTEGR15: 19;

        then

         A4: |.( integral (f,c,d)).| = |.( integral (f,d,c)).| by EUCLID: 10;

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

        hence thesis by A1, A2, A4, Lm10;

      end;

        suppose

         A5: c <= d;

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

        hence thesis by A1, A5, Lm10;

      end;

    end;

    

     Lm11: for n be non zero Element of NAT holds for f be PartFunc of REAL , ( REAL n) st a <= b & c <= d & f is_integrable_on ['a, b'] & |.f.| is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'] holds |.f.| is_integrable_on ['c, d'] & ( |.f.| | ['c, d']) is bounded & |.( integral (f,c,d)).| <= ( integral ( |.f.|,c,d))

    proof

      let n be non zero Element of NAT ;

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

      assume that

       A1: a <= b and

       A2: c <= d and

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

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

      hence thesis by A1, A3, Th22;

    end;

    

     Lm12: for n be non zero Element of NAT holds for f be PartFunc of REAL , ( REAL n) st a <= b & c <= d & f is_integrable_on ['a, b'] & |.f.| is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'] holds |.( integral (f,d,c)).| <= ( integral ( |.f.|,c,d))

    proof

      let n be non zero Element of NAT ;

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

      assume that

       A1: a <= b and

       A2: c <= d and

       A3: f is_integrable_on ['a, b'] & |.f.| is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] and

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

       ['c, d'] = [.c, d.] by A2, INTEGRA5:def 3;

      then

       A5: |.( integral (f,c,d)).| <= ( integral ( |.f.|,c,d)) & ( integral (f,c,d)) = ( integral (f, ['c, d'])) by A1, A2, A3, A4, Lm11, INTEGR15: 19;

       ['c, d'] = [.c, d.] by A2, INTEGRA5:def 3;

      then ( integral (f,d,c)) = ( - ( integral (f, ['c, d']))) by INTEGR15: 20;

      hence thesis by A5, EUCLID: 10;

    end;

    theorem :: INTEGR19:23

    for n be non zero Element of NAT holds for f be PartFunc of REAL , ( REAL n) st a <= b & c <= d & f is_integrable_on ['a, b'] & |.f.| is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'] holds |.f.| is_integrable_on ['c, d'] & ( |.f.| | ['c, d']) is bounded & |.( integral (f,c,d)).| <= ( integral ( |.f.|,c,d)) & |.( integral (f,d,c)).| <= ( integral ( |.f.|,c,d)) by Lm11, Lm12;

    

     Lm13: for n be non zero Element of NAT holds for f be PartFunc of REAL , ( REAL n) st (a <= b & f is_integrable_on ['a, b'] & |.f.| is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'] & for x be Real st x in ['( min (c,d)), ( max (c,d))'] holds |.(f /. x).| <= e) holds |.( integral (f,c,d)).| <= (e * |.(d - c).|)

    proof

      let n be non zero Element of NAT ;

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

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

      assume that

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

       A2: for x be Real st x in ['( min (c,d)), ( max (c,d))'] holds |.(f /. x).| <= e;

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

      then

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

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

      then

       A4: ['( min (c,d)), ( max (c,d))'] c= ( dom |.f.|) by A1, Th3;

      then

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

      

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

       |.f.| is_integrable_on A by A1, Th22;

      then

       A6: g is integrable;

      consider h be Function of A, REAL such that

       A7: ( rng h) = {e} and

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

       A9:

      now

        let x be Real;

        assume

         A10: x in A;

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

        then (g . x) = ( |.f.| /. x) by A10, A4, PARTFUN1:def 6;

        then

         A11: (g . x) = |.(f /. x).| by A10, A4, NFCONT_4:def 2;

        (h . x) in {e} by A7, A10, FUNCT_2: 4;

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

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

      end;

      

       A12: |.( integral (f,c,d)).| <= ( integral ( |.f.|,( min (c,d)),( max (c,d)))) by A1, Th22;

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

      then ( min (c,d)) <= ( max (c,d)) by XXREAL_0: 2;

      then

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

      ( |.f.| | A) is bounded by A1, Th22;

      then

       A14: (g | A) is bounded;

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

      then ( integral ( |.f.|,( min (c,d)),( max (c,d)))) <= (e * |.(d - c).|) by A13, A8, A9, A6, A14, A5, INTEGRA2: 34;

      hence thesis by A12, XXREAL_0: 2;

    end;

    

     Lm14: for n be non zero Element of NAT holds for f be PartFunc of REAL , ( REAL n) st (a <= b & c <= d & f is_integrable_on ['a, b'] & |.f.| is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'] & for x be Real st x in ['c, d'] holds |.(f /. x).| <= e) holds |.( integral (f,c,d)).| <= (e * (d - c))

    proof

      let n be non zero Element of NAT ;

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

      assume that

       A1: a <= b and

       A2: c <= d and

       A3: f is_integrable_on ['a, b'] & |.f.| is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] & (d in ['a, b'] & for x be Real st x in ['c, d'] holds |.(f /. x).| <= e);

       0 <= (d - c) by A2, XREAL_1: 48;

      then

       A4: |.(d - c).| = (d - c) by ABSVALUE:def 1;

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

      hence thesis by A1, A3, A4, Lm13;

    end;

    

     Lm15: for n be non zero Element of NAT holds for f be PartFunc of REAL , ( REAL n) st (a <= b & c <= d & f is_integrable_on ['a, b'] & |.f.| is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'] & for x be Real st x in ['c, d'] holds |.(f /. x).| <= e) holds |.( integral (f,d,c)).| <= (e * (d - c))

    proof

      let n be non zero Element of NAT ;

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

      assume that

       A1: a <= b and

       A2: c <= d and

       A3: f is_integrable_on ['a, b'] & |.f.| is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] and

       A4: d in ['a, b'] and

       A5: for x be Real st x in ['c, d'] holds |.(f /. x).| <= e;

       ['c, d'] = [.c, d.] by A2, INTEGRA5:def 3;

      then

       A6: |.( integral (f,c,d)).| <= (e * (d - c)) & ( integral (f,c,d)) = ( integral (f, ['c, d'])) by A1, A2, A3, A4, A5, Lm14, INTEGR15: 19;

       ['c, d'] = [.c, d.] by A2, INTEGRA5:def 3;

      then ( integral (f,d,c)) = ( - ( integral (f, ['c, d']))) by INTEGR15: 20;

      hence thesis by A6, EUCLID: 10;

    end;

    theorem :: INTEGR19:24

    for n be non zero Element of NAT holds for f be PartFunc of REAL , ( REAL n) st (a <= b & c <= d & f is_integrable_on ['a, b'] & |.f.| is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'] & for x be Real st x in ['c, d'] holds |.(f /. x).| <= e) holds |.( integral (f,c,d)).| <= (e * (d - c)) & |.( integral (f,d,c)).| <= (e * (d - c)) by Lm14, Lm15;

    theorem :: INTEGR19:25

    

     Th25: a <= b & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'] implies ( integral ((r (#) f),c,d)) = (r * ( integral (f,c,d)))

    proof

      assume

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

       A2:

      now

        let i;

        set P = ( proj (i,n));

        assume

         A3: i in ( Seg n);

        then

         A4: (P * f) is_integrable_on ['a, b'] by A1;

        (P * (f | ['a, b'])) is bounded by A3, A1;

        then

         A5: ((P * f) | ['a, b']) is bounded by RELAT_1: 83;

        ( dom P) = ( REAL n) by FUNCT_2:def 1;

        then ( rng f) c= ( dom P);

        then

         A6: ['a, b'] c= ( dom (P * f)) by A1, RELAT_1: 27;

        (P * (r (#) f)) = (r (#) (P * f)) by INTEGR15: 16;

        hence ( integral ((P * (r (#) f)),c,d)) = (r * ( integral ((P * f),c,d))) by A4, A5, A6, A1, INTEGRA6: 25;

      end;

       A7:

      now

        let i be Nat;

        assume i in ( dom ( integral ((r (#) f),c,d)));

        then

         A8: i in ( Seg n) by INTEGR15:def 18;

        set P = ( proj (i,n));

        

        thus (( integral ((r (#) f),c,d)) . i) = ( integral ((P * (r (#) f)),c,d)) by A8, INTEGR15:def 18

        .= (r * ( integral ((P * f),c,d))) by A8, A2

        .= (r * (( integral (f,c,d)) . i)) by A8, INTEGR15:def 18

        .= ((r * ( integral (f,c,d))) . i) by RVSUM_1: 44;

      end;

      

       A9: ( Seg n) = ( dom ( integral ((r (#) f),c,d))) by INTEGR15:def 18;

      ( len (r * ( integral (f,c,d)))) = n by CARD_1:def 7;

      then ( Seg n) = ( dom (r * ( integral (f,c,d)))) by FINSEQ_1:def 3;

      hence ( integral ((r (#) f),c,d)) = (r * ( integral (f,c,d))) by A9, A7, FINSEQ_1: 13;

    end;

    theorem :: INTEGR19:26

    

     Th26: a <= b & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'] implies ( integral (( - f),c,d)) = ( - ( integral (f,c,d)))

    proof

      ( - f) = (( - 1) (#) f) by NFCONT_4: 7;

      hence thesis by Th25;

    end;

    theorem :: INTEGR19:27

    

     Th27: a <= b & f is_integrable_on ['a, b'] & g is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & (g | ['a, b']) is bounded & ['a, b'] c= ( dom f) & ['a, b'] c= ( dom g) & c in ['a, b'] & d in ['a, b'] implies ( integral ((f + g),c,d)) = (( integral (f,c,d)) + ( integral (g,c,d)))

    proof

      assume

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

       A2:

      now

        let i;

        set P = ( proj (i,n));

        assume

         A3: i in ( Seg n);

        then

         A4: (P * f) is_integrable_on ['a, b'] by A1;

        (P * (f | ['a, b'])) is bounded by A3, A1;

        then

         A5: ((P * f) | ['a, b']) is bounded by RELAT_1: 83;

        

         A6: (P * g) is_integrable_on ['a, b'] by A3, A1;

        (P * (g | ['a, b'])) is bounded by A3, A1;

        then

         A7: ((P * g) | ['a, b']) is bounded by RELAT_1: 83;

        

         A8: ( dom P) = ( REAL n) by FUNCT_2:def 1;

        then ( rng f) c= ( dom P);

        then

         A9: ['a, b'] c= ( dom (P * f)) by A1, RELAT_1: 27;

        ( rng g) c= ( dom P) by A8;

        then

         A10: ['a, b'] c= ( dom (P * g)) by A1, RELAT_1: 27;

        

         A11: (P * (f + g)) = ((P * f) + (P * g)) by INTEGR15: 15;

        thus ( integral ((P * (f + g)),c,d)) = (( integral ((P * f),c,d)) + ( integral ((P * g),c,d))) by A4, A5, A9, A6, A7, A10, A1, A11, INTEGRA6: 24;

      end;

       A12:

      now

        let i be Nat;

        assume i in ( dom ( integral ((f + g),c,d)));

        then

         A13: i in ( Seg n) by INTEGR15:def 18;

        set P = ( proj (i,n));

        

        thus (( integral ((f + g),c,d)) . i) = ( integral ((P * (f + g)),c,d)) by A13, INTEGR15:def 18

        .= (( integral ((P * f),c,d)) + ( integral ((P * g),c,d))) by A13, A2

        .= ((( integral (f,c,d)) . i) + ( integral ((P * g),c,d))) by A13, INTEGR15:def 18

        .= ((( integral (f,c,d)) . i) + (( integral (g,c,d)) . i)) by A13, INTEGR15:def 18

        .= ((( integral (f,c,d)) + ( integral (g,c,d))) . i) by RVSUM_1: 11;

      end;

      

       A14: ( Seg n) = ( dom ( integral ((f + g),c,d))) by INTEGR15:def 18;

      ( len (( integral (f,c,d)) + ( integral (g,c,d)))) = n by CARD_1:def 7;

      then ( Seg n) = ( dom (( integral (f,c,d)) + ( integral (g,c,d)))) by FINSEQ_1:def 3;

      hence thesis by A14, A12, FINSEQ_1: 13;

    end;

    theorem :: INTEGR19:28

    

     Th28: a <= b & f is_integrable_on ['a, b'] & g is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & (g | ['a, b']) is bounded & ['a, b'] c= ( dom f) & ['a, b'] c= ( dom g) & c in ['a, b'] & d in ['a, b'] implies ( integral ((f - g),c,d)) = (( integral (f,c,d)) - ( integral (g,c,d)))

    proof

      assume

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

      

       A2: ( - g) is_integrable_on ['a, b'] & (( - g) | ['a, b']) is bounded by A1, Th12;

      

       A3: ( dom g) = ( dom ( - g)) by NFCONT_4:def 3;

      (f - g) = (f + ( - g)) by Lm1;

      

      hence ( integral ((f - g),c,d)) = (( integral (f,c,d)) + ( integral (( - g),c,d))) by A1, A2, A3, Th27

      .= (( integral (f,c,d)) - ( integral (g,c,d))) by A1, Th26;

    end;

    theorem :: INTEGR19:29

    

     Th29: (a <= b & ['a, b'] c= ( dom f) & for x be Real st x in ['a, b'] holds (f . x) = E) implies f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ( integral (f,a,b)) = ((b - a) * E)

    proof

      assume

       A1: a <= b & ['a, b'] c= ( dom f) & (for x be Real st x in ['a, b'] holds (f . x) = E);

       A2:

      now

        let i be Element of NAT ;

        set P = ( proj (i,n));

        assume i in ( Seg n);

        ( dom P) = ( REAL n) by FUNCT_2:def 1;

        then ( rng f) c= ( dom P);

        then

         A3: ['a, b'] c= ( dom (P * f)) by A1, RELAT_1: 27;

        for x be Real st x in ['a, b'] holds ((P * f) . x) = (P . E)

        proof

          let x be Real;

          assume

           A4: x in ['a, b'];

          

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

          

          hence ((P * f) . x) = (P . (f /. x)) by A4, A3, FUNCT_1: 12

          .= (P . E) by A4, A1, A5;

        end;

        hence (P * f) is_integrable_on ['a, b'] & ((P * f) | ['a, b']) is bounded & ( integral ((P * f),a,b)) = ((P . E) * (b - a)) by A3, A1, INTEGRA6: 26;

      end;

      then

       A6: for i be Element of NAT st i in ( Seg n) holds (( proj (i,n)) * f) is_integrable_on ['a, b'];

      

       A7: ( Seg n) = ( dom ( integral (f,a,b))) by INTEGR15:def 18;

       A8:

      now

        let i;

        set P = ( proj (i,n));

        assume i in ( Seg n);

        then ((P * f) | ['a, b']) is bounded by A2;

        hence (P * (f | ['a, b'])) is bounded by RELAT_1: 83;

      end;

       A9:

      now

        let i be Nat;

        assume

         A10: i in ( dom ( integral (f,a,b)));

        

        hence (( integral (f,a,b)) . i) = ( integral ((( proj (i,n)) * f),a,b)) by A7, INTEGR15:def 18

        .= ((( proj (i,n)) . E) * (b - a)) by A10, A2, A7

        .= ((b - a) * (E . i)) by PDIFF_1:def 1

        .= (((b - a) * E) . i) by RVSUM_1: 44;

      end;

      ( len ((b - a) * E)) = n by CARD_1:def 7;

      then ( Seg n) = ( dom ((b - a) * E)) by FINSEQ_1:def 3;

      hence thesis by A6, A8, A7, A9, FINSEQ_1: 13;

    end;

    theorem :: INTEGR19:30

    

     Th30: a <= b & (for x be Real st x in ['a, b'] holds (f . x) = E) & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'] implies ( integral (f,c,d)) = ((d - c) * E)

    proof

      assume

       A1: a <= b & (for x be Real st x in ['a, b'] holds (f . x) = E) & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'];

      

       A2: ( Seg n) = ( dom ( integral (f,c,d))) by INTEGR15:def 18;

       A3:

      now

        let i;

        set P = ( proj (i,n));

        ( dom P) = ( REAL n) by FUNCT_2:def 1;

        then ( rng f) c= ( dom P);

        then

         A4: ['a, b'] c= ( dom (P * f)) by A1, RELAT_1: 27;

        for x be Real st x in ['a, b'] holds ((P * f) . x) = (P . E)

        proof

          let x be Real;

          assume

           A5: x in ['a, b'];

          then

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

          ((P * f) . x) = (P . (f /. x)) by A4, A5, A6, FUNCT_1: 12

          .= (P . E) by A6, A5, A1;

          hence thesis;

        end;

        hence ( integral ((P * f),c,d)) = ((P . E) * (d - c)) by A4, A1, INTEGRA6: 27;

      end;

       A7:

      now

        let i be Nat;

        set P = ( proj (i,n));

        assume

         A8: i in ( dom ( integral (f,c,d)));

        

        hence (( integral (f,c,d)) . i) = ( integral ((P * f),c,d)) by A2, INTEGR15:def 18

        .= ((P . E) * (d - c)) by A3, A8

        .= ((d - c) * (E . i)) by PDIFF_1:def 1

        .= (((d - c) * E) . i) by RVSUM_1: 44;

      end;

      ( len ((d - c) * E)) = n by CARD_1:def 7;

      then ( Seg n) = ( dom ((d - c) * E)) by FINSEQ_1:def 3;

      hence thesis by A2, A7, FINSEQ_1: 13;

    end;

    theorem :: INTEGR19:31

    

     Th31: a <= b & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'] implies ( integral (f,a,d)) = (( integral (f,a,c)) + ( integral (f,c,d)))

    proof

      assume

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

       A2:

      now

        let i;

        set P = ( proj (i,n));

        assume

         A3: i in ( Seg n);

        then

         A4: (P * f) is_integrable_on ['a, b'] by A1;

        (P * (f | ['a, b'])) is bounded by A3, A1;

        then

         A5: ((P * f) | ['a, b']) is bounded by RELAT_1: 83;

        ( dom P) = ( REAL n) by FUNCT_2:def 1;

        then ( rng f) c= ( dom P);

        then ( dom (P * f)) = ( dom f) by RELAT_1: 27;

        hence ( integral ((P * f),a,d)) = (( integral ((P * f),a,c)) + ( integral ((P * f),c,d))) by A4, A5, A1, INTEGRA6: 20;

      end;

      

       A6: ( Seg n) = ( dom ( integral (f,a,d))) by INTEGR15:def 18;

       A7:

      now

        let i0 be Nat;

        assume

         A8: i0 in ( dom ( integral (f,a,d)));

        set P = ( proj (i0,n));

        

        thus (( integral (f,a,d)) . i0) = ( integral ((P * f),a,d)) by A8, A6, INTEGR15:def 18

        .= (( integral ((P * f),a,c)) + ( integral ((P * f),c,d))) by A8, A2, A6

        .= ((( integral (f,a,c)) . i0) + ( integral ((P * f),c,d))) by A8, A6, INTEGR15:def 18

        .= ((( integral (f,a,c)) . i0) + (( integral (f,c,d)) . i0)) by A8, A6, INTEGR15:def 18

        .= ((( integral (f,a,c)) + ( integral (f,c,d))) . i0) by RVSUM_1: 11;

      end;

      ( len (( integral (f,a,c)) + ( integral (f,c,d)))) = n by CARD_1:def 7;

      then ( Seg n) = ( dom (( integral (f,a,c)) + ( integral (f,c,d)))) by FINSEQ_1:def 3;

      hence thesis by A6, A7, FINSEQ_1: 13;

    end;

    theorem :: INTEGR19:32

    

     Th32: (a <= b & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'] & for x be Real st x in ['( min (c,d)), ( max (c,d))'] holds |.(f /. x).| <= e) implies |.( integral (f,c,d)).| <= ((n * e) * |.(d - c).|)

    proof

      assume

       A1: a <= b & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'] & for x be Real st x in ['( min (c,d)), ( max (c,d))'] holds |.(f /. x).| <= e;

       A2:

      now

        let i;

        set P = ( proj (i,n));

        assume

         A3: i in ( Seg n);

        ( dom P) = ( REAL n) by FUNCT_2:def 1;

        then ( rng f) c= ( dom P);

        then

         A4: ['a, b'] c= ( dom (P * f)) by A1, RELAT_1: 27;

        set f1 = (P * f);

        

         A5: for x be Real st x in ['( min (c,d)), ( max (c,d))'] holds |.((P * f) . x).| <= e

        proof

          let x be Real;

          assume

           A6: x in ['( min (c,d)), ( max (c,d))'];

           ['( min (c,d)), ( max (c,d))'] c= ['a, b'] by A1, Lm2;

          then

           A7: x in ( dom (P * f)) by A4, A6;

          then

           A8: x in ( dom f) by FUNCT_1: 11;

          

           A9: |.(f /. x).| <= e by A1, A6;

          

           A10: ((P * f) . x) = (P . (f . x)) by A7, FUNCT_1: 12

          .= (P . (f /. x)) by A8, PARTFUN1:def 6;

          1 <= i & i <= n by A3, FINSEQ_1: 1;

          then |.(P . (f /. x)).| <= |.(f /. x).| by PDIFF_8: 5;

          hence |.((P * f) . x).| <= e by A10, A9, XXREAL_0: 2;

        end;

        

         A11: f1 is_integrable_on ['a, b'] by A1, A3;

        

         A12: (P * (f | ['a, b'])) is bounded by A1, A3;

        ((P * f) | ['a, b']) = (P * (f | ['a, b'])) by RELAT_1: 83;

        hence |.( integral (f1,c,d)).| <= (e * |.(d - c).|) by A12, A1, A4, A5, A11, Lm4;

      end;

      now

        let i;

        set P = ( proj (i,n));

        assume 1 <= i & i <= n;

        then

         A13: i in ( Seg n);

        then |.( integral ((P * f),c,d)).| <= (e * |.(d - c).|) by A2;

        hence |.(( integral (f,c,d)) . i).| <= (e * |.(d - c).|) by A13, INTEGR15:def 18;

      end;

      then |.( integral (f,c,d)).| <= (n * (e * |.(d - c).|)) by PDIFF_8: 15;

      hence thesis;

    end;

    theorem :: INTEGR19:33

    

     Th33: ( integral (f,b,a)) = ( - ( integral (f,a,b)))

    proof

      per cases ;

        suppose a <= b;

        then

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

        ( integral (f, ['a, b'])) = ( integral (f,a,b)) by A1, INTEGR15: 19;

        hence ( integral (f,b,a)) = ( - ( integral (f,a,b))) by A1, INTEGR15: 20;

      end;

        suppose not a <= b;

        then

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

        then ( - ( integral (f, ['b, a']))) = ( integral (f,a,b)) by INTEGR15: 20;

        hence thesis by A2, INTEGR15: 19;

      end;

    end;

    begin

    

     Lm16: for p be FinSequence of ( REAL n), r be Element of ( REAL n), q be FinSequence of ( REAL-NS n) st p = q & (for i be Element of NAT st i in ( Seg n) holds ex Pi be FinSequence of REAL st Pi = (( proj (i,n)) * p) & (r . i) = ( Sum Pi)) holds r = ( Sum q)

    proof

      defpred P[ Nat] means for p be FinSequence of ( REAL n), r be Element of ( REAL n), q be FinSequence of ( REAL-NS n) st ( len p) = $1 & p = q & (for i be Element of NAT st i in ( Seg n) holds ex Pi be FinSequence of REAL st Pi = (( proj (i,n)) * p) & (r . i) = ( Sum Pi)) holds r = ( Sum q);

      

       A1: P[ 0 ]

      proof

        let p be FinSequence of ( REAL n), r be Element of ( REAL n), q be FinSequence of ( REAL-NS n);

        assume

         A2: ( len p) = 0 & p = q & (for i be Element of NAT st i in ( Seg n) holds ex Pi be FinSequence of REAL st Pi = (( proj (i,n)) * p) & (r . i) = ( Sum Pi));

        then

         A3: p = {} ;

        

         A4: q = ( <*> the carrier of ( REAL-NS n)) by A2;

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

        then

         A5: ( dom r) = ( Seg n) by FINSEQ_1:def 3;

        

         A6: ( dom (( Seg n) --> 0 )) = ( Seg n) by FUNCOP_1: 13;

        now

          let x be object;

          assume

           A7: x in ( dom r);

          then

          reconsider i = x as Element of NAT ;

          set P = ( proj (i,n));

          consider Pi be FinSequence of REAL such that

           A8: Pi = (P * p) & (r . i) = ( Sum Pi) by A2, A5, A7;

          (r . x) = 0 by A3, A8, RVSUM_1: 72;

          hence (r . x) = ((( Seg n) --> 0 ) . x) by A5, A7, FUNCOP_1: 7;

        end;

        then r = ( 0* n) by A5, A6, FUNCT_1: 2;

        then r = ( 0. ( REAL-NS n)) by REAL_NS1:def 4;

        hence r = ( Sum q) by A4, RLVECT_1: 43;

      end;

      

       A9: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         A10: P[k];

        now

          let p be FinSequence of ( REAL n), r be Element of ( REAL n), q be FinSequence of ( REAL-NS n);

          assume

           A11: ( len p) = (k + 1) & p = q & (for i be Element of NAT st i in ( Seg n) holds ex Pi be FinSequence of REAL st Pi = (( proj (i,n)) * p) & (r . i) = ( Sum Pi));

          set p1 = (p | k);

          

           A12: (k + 1) in ( Seg (k + 1)) by FINSEQ_1: 4;

          then (k + 1) in ( dom p) by A11, FINSEQ_1:def 3;

          then (p . (k + 1)) in ( rng p) by FUNCT_1: 3;

          then

          reconsider pk1 = (p . (k + 1)) as Element of ( REAL n);

          set q1 = (q | k);

          (k + 1) in ( dom q) by A11, A12, FINSEQ_1:def 3;

          then (q . (k + 1)) in ( rng q) by FUNCT_1: 3;

          then

          reconsider qk1 = (q . (k + 1)) as Point of ( REAL-NS n);

          defpred YX[ Nat, set] means ex P1i be FinSequence of REAL st P1i = (( proj ($1,n)) * p1) & $2 = ( Sum P1i);

          

           A13: for i be Nat st i in ( Seg n) holds ex r be Element of REAL st YX[i, r]

          proof

            let i be Nat;

            assume i in ( Seg n);

            reconsider S = ( Sum (( proj (i,n)) * p1)) as Element of REAL by XREAL_0:def 1;

            take S;

            thus thesis;

          end;

          consider r1 be FinSequence of REAL such that

           A14: ( dom r1) = ( Seg n) & for i be Nat st i in ( Seg n) holds YX[i, (r1 . i)] from FINSEQ_1:sch 5( A13);

          ( len r1) = n by A14, FINSEQ_1:def 3;

          then

          reconsider r1 as Element of ( REAL n) by FINSEQ_2: 92;

          

           A15: for i st i in ( Seg n) holds ex P1i be FinSequence of REAL st P1i = (( proj (i,n)) * p1) & (r1 . i) = ( Sum P1i) by A14;

          

           A16: k <= ( len p) by A11, NAT_1: 16;

          then

           A17: ( len p1) = k by FINSEQ_1: 59;

          

           A18: r1 = ( Sum q1) by A10, A11, A15, A17;

          

           A19: ( len r) = n by CARD_1:def 7;

          

           A20: ( len (r1 + pk1)) = n by CARD_1:def 7;

          now

            let i be Nat;

            set P = ( proj (i,n));

            assume 1 <= i & i <= n;

            then

             A21: i in ( Seg n);

            consider Pi be FinSequence of REAL such that

             A22: Pi = (P * p) & (r . i) = ( Sum Pi) by A21, A11;

            consider P1i be FinSequence of REAL such that

             A23: P1i = (P * p1) & (r1 . i) = ( Sum P1i) by A21, A14;

            

             A24: ( dom P) = ( REAL n) by FUNCT_2:def 1;

            then

             A25: ( rng p) c= ( dom P);

            

             A26: ( dom Pi) = ( dom p) by A25, A22, RELAT_1: 27

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

            

             A27: ( len p) = (( len p1) + 1) by A11, A16, FINSEQ_1: 59

            .= (( len p1) + ( len <*(pk1 . i)*>)) by FINSEQ_1: 40;

            

             A28: ( rng p1) c= ( dom P) by A24;

            

             A29: ( dom P1i) = ( dom p1) by A28, A23, RELAT_1: 27

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

            then

             A30: ( dom Pi) = ( Seg (( len P1i) + ( len <*(pk1 . i)*>))) by A26, A27, FINSEQ_1:def 3;

            ( len p1) <= ( len p) by A16, FINSEQ_1: 59;

            then

             A31: ( Seg ( len p1)) c= ( Seg ( len p)) by FINSEQ_1: 5;

            

             A32: for k be Nat st k in ( dom P1i) holds (Pi . k) = (P1i . k)

            proof

              let k be Nat;

              assume

               A33: k in ( dom P1i);

              then

               A34: k in ( dom p1) by A29, FINSEQ_1:def 3;

              

              thus (P1i . k) = (P . (p1 . k)) by A23, A33, FUNCT_1: 12

              .= (P . (p . k)) by A34, FUNCT_1: 47

              .= (Pi . k) by A22, A33, A29, A26, A31, FUNCT_1: 12;

            end;

            for k be Nat st k in ( dom <*(pk1 . i)*>) holds (Pi . (( len P1i) + k)) = ( <*(pk1 . i)*> . k)

            proof

              let j be Nat;

              assume j in ( dom <*(pk1 . i)*>);

              then j in ( Seg ( len <*(pk1 . i)*>)) by FINSEQ_1:def 3;

              then j in {1} by FINSEQ_1: 2, FINSEQ_1: 40;

              then

               A35: j = 1 by TARSKI:def 1;

              

              thus (Pi . (( len P1i) + j)) = (Pi . (k + 1)) by A29, A17, A35, FINSEQ_1:def 3

              .= (P . (p . (k + 1))) by A22, A26, A11, FINSEQ_1: 4, FUNCT_1: 12

              .= (pk1 . i) by PDIFF_1:def 1

              .= ( <*(pk1 . i)*> . j) by A35, FINSEQ_1: 40;

            end;

            then Pi = (P1i ^ <*(pk1 . i)*>) by A32, A30, FINSEQ_1:def 7;

            

            hence (r . i) = ((r1 . i) + (pk1 . i)) by A22, A23, RVSUM_1: 74

            .= ((r1 + pk1) . i) by RVSUM_1: 11;

          end;

          then

           A36: r = (r1 + pk1) by A19, A20;

          

           A37: ( len q) = (( len q1) + 1) by A16, A11, FINSEQ_1: 59;

          

           A38: q1 = (q | ( dom q1)) by A17, A11, FINSEQ_1:def 3;

          

          thus r = (( Sum q1) + qk1) by A36, A18, A11, REAL_NS1: 2

          .= ( Sum q) by A11, A37, A38, RLVECT_1: 38;

        end;

        hence P[(k + 1)];

      end;

      

       A39: for k be Nat holds P[k] from NAT_1:sch 2( A1, A9);

      let p be FinSequence of ( REAL n), r be Element of ( REAL n), q be FinSequence of ( REAL-NS n);

      assume

       A40: p = q & (for i be Element of NAT st i in ( Seg n) holds ex Pi be FinSequence of REAL st Pi = (( proj (i,n)) * p) & (r . i) = ( Sum Pi));

      thus r = ( Sum q) by A40, A39;

    end;

    definition

      let R be RealNormSpace, X be non empty set, g be PartFunc of X, R;

      :: INTEGR19:def1

      attr g is bounded means ex r be Real st for y be set st y in ( dom g) holds ||.(g /. y).|| < r;

    end

    theorem :: INTEGR19:34

    

     Th34: for f be PartFunc of REAL , ( REAL n), g be PartFunc of REAL , ( REAL-NS n) st f = g holds f is bounded iff g is bounded

    proof

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

      assume

       A1: f = g;

      thus f is bounded implies g is bounded

      proof

        assume

         A2: f is bounded;

        defpred Pd[ Nat, Element of REAL ] means for y be set st y in ( dom (( proj ($1,n)) * f)) holds |.((( proj ($1,n)) * f) . y).| < $2;

        

         A3: for i be Nat st i in ( Seg n) holds ex di be Element of REAL st Pd[i, di]

        proof

          let i be Nat;

          set P = ( proj (i,n));

          assume i in ( Seg n);

          then (P * f) is bounded by A2;

          then

          consider r be Real such that

           A4: for y be set st y in ( dom (P * f)) holds |.((P * f) . y).| < r by COMSEQ_2:def 3;

          reconsider r as Element of REAL by XREAL_0:def 1;

          take r;

          thus thesis by A4;

        end;

        consider d be FinSequence of REAL such that

         A5: ( dom d) = ( Seg n) & for k be Nat st k in ( Seg n) holds Pd[k, (d /. k)] from RECDEF_1:sch 17( A3);

        set K = ( max d);

        for y be set st y in ( dom g) holds ||.(g /. y).|| < ((n * K) + 1)

        proof

          let y be set;

          assume

           A6: y in ( dom g);

          set s = (f /. y);

          now

            let i;

            set P = ( proj (i,n));

            assume

             A7: 1 <= i & i <= n;

            then

             A8: i in ( Seg n);

            ( dom P) = ( REAL n) by FUNCT_2:def 1;

            then ( rng f) c= ( dom P);

            then

             A9: y in ( dom (P * f)) by A6, A1, RELAT_1: 27;

            then

             A10: |.((P * f) . y).| < (d /. i) by A8, A5;

            (f . y) = s by A6, A1, PARTFUN1:def 6;

            then ((P * f) . y) = (P . s) by A9, FUNCT_1: 12;

            then

             A11: |.(s . i).| < (d /. i) by A10, PDIFF_1:def 1;

            ( len d) = n by A5, FINSEQ_1:def 3;

            then (d . i) <= K by A7, RFINSEQ2: 1;

            then (d /. i) <= K by A8, A5, PARTFUN1:def 6;

            hence |.(s . i).| <= K by A11, XXREAL_0: 2;

          end;

          then

           A12: |.s.| < ((n * K) + 1) by PDIFF_8: 15, XREAL_1: 145;

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

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

          hence ||.(g /. y).|| < ((n * K) + 1) by A12, REAL_NS1: 1;

        end;

        hence g is bounded;

      end;

      assume

       A13: g is bounded;

      consider r be Real such that

       A14: for y be set st y in ( dom g) holds ||.(g /. y).|| < r by A13;

      let i;

      set P = ( proj (i,n));

      assume

       A15: i in ( Seg n);

      for y be set st y in ( dom (P * f)) holds |.((P * f) . y).| < r

      proof

        let y be set;

        assume

         A16: y in ( dom (P * f));

        ( dom P) = ( REAL n) by FUNCT_2:def 1;

        then ( rng f) c= ( dom P);

        then

         A17: y in ( dom f) by A16, RELAT_1: 27;

        then

         A18: ||.(g /. y).|| < r by A14, A1;

        set s = (f /. y);

        (g /. y) = (g . y) by A17, A1, PARTFUN1:def 6

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

        then

         A19: |.s.| < r by A18, REAL_NS1: 1;

         |.(s . i).| <= |.s.| by A15, REAL_NS1: 8;

        then

         A20: |.(s . i).| < r by A19, XXREAL_0: 2;

        (f . y) = s by A17, PARTFUN1:def 6;

        then ((P * f) . y) = (P . s) by A16, FUNCT_1: 12;

        hence |.((P * f) . y).| < r by A20, PDIFF_1:def 1;

      end;

      hence (P * f) is bounded by COMSEQ_2:def 3;

    end;

    theorem :: INTEGR19:35

    

     Th35: for X,Y be set, f1,f2 be PartFunc of REAL , ( REAL-NS n) st (f1 | X) is bounded & (f2 | Y) is bounded holds ((f1 + f2) | (X /\ Y)) is bounded & ((f1 - f2) | (X /\ Y)) is bounded

    proof

      let X,Y be set, f1,f2 be PartFunc of REAL , ( REAL-NS n);

      assume

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

      consider r1 be Real such that

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

      consider r2 be Real such that

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

      now

        let x be set;

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

        then

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

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

        then

         A5: x in ( dom f1) & x in ( dom f2) by XBOOLE_0:def 4;

        

         A6: x in X & x in Y by A4, XBOOLE_0:def 4;

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

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

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

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

        then

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

        x in ( dom (f1 | X)) by A5, A6, RELAT_1: 57;

        then

         A8: ||.((f1 | X) /. x).|| < r1 by A2;

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

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

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

      end;

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

      take (r1 + r2);

      let x be set;

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

      then

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

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

      then

       A10: x in ( dom f1) & x in ( dom f2) by XBOOLE_0:def 4;

      

       A11: x in X & x in Y by A9, XBOOLE_0:def 4;

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

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

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

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

      then

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

      x in ( dom (f1 | X)) by A10, A11, RELAT_1: 57;

      then

       A13: ||.((f1 | X) /. x).|| < r1 by A2;

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

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

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

    end;

    theorem :: INTEGR19:36

    

     Th36: for f be Function of A, ( REAL n), g be Function of A, ( REAL-NS n), D be Division of A, p be FinSequence of ( REAL n), q be FinSequence of ( REAL-NS n) st f = g & p = q holds p is middle_volume of f, D iff q is middle_volume of g, D

    proof

      let f be Function of A, ( REAL n), g be Function of A, ( REAL-NS n), D be Division of A, p be FinSequence of ( REAL n), q be FinSequence of ( REAL-NS n);

      assume

       A1: f = g & p = q;

      thus p is middle_volume of f, D implies q is middle_volume of g, D

      proof

        assume

         A2: p is middle_volume of f, D;

        then

         A3: ( len q) = ( len D) by A1, INTEGR15:def 5;

        for i be Nat st i in ( dom D) holds ex c be Point of ( REAL-NS n) st c in ( rng (g | ( divset (D,i)))) & (q . i) = (( vol ( divset (D,i))) * c)

        proof

          let i be Nat;

          assume i in ( dom D);

          then

          consider r be Element of ( REAL n) such that

           A4: r in ( rng (f | ( divset (D,i)))) & (p . i) = (( vol ( divset (D,i))) * r) by A2, INTEGR15:def 5;

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

          take c;

          thus thesis by A4, A1, REAL_NS1: 3;

        end;

        hence q is middle_volume of g, D by A3, INTEGR18:def 1;

      end;

      thus q is middle_volume of g, D implies p is middle_volume of f, D

      proof

        assume

         A5: q is middle_volume of g, D;

        then

         A6: ( len p) = ( len D) by A1, INTEGR18:def 1;

        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)))) & (p . i) = (( vol ( divset (D,i))) * r)

        proof

          let i be Nat;

          assume

           A7: i in ( dom D);

          consider c be Point of ( REAL-NS n) such that

           A8: c in ( rng (g | ( divset (D,i)))) & (q . i) = (( vol ( divset (D,i))) * c) by A5, A7, INTEGR18:def 1;

          reconsider r = c as Element of ( REAL n) by REAL_NS1:def 4;

          take r;

          thus thesis by A8, A1, REAL_NS1: 3;

        end;

        hence p is middle_volume of f, D by A6, INTEGR15:def 5;

      end;

    end;

    theorem :: INTEGR19:37

    

     Th37: for f be Function of A, ( REAL n), g be Function of A, ( REAL-NS n), D be Division of A, p be middle_volume of f, D, q be middle_volume of g, D st f = g & p = q holds ( middle_sum (f,p)) = ( middle_sum (g,q))

    proof

      let f be Function of A, ( REAL n), g be Function of A, ( REAL-NS n), D be Division of A, p be middle_volume of f, D, q be middle_volume of g, D;

      assume

       A1: f = g & p = q;

      for i be Element of NAT st i in ( Seg n) holds ex Pi be FinSequence of REAL st Pi = (( proj (i,n)) * p) & (( middle_sum (f,p)) . i) = ( Sum Pi) by INTEGR15:def 6;

      hence ( middle_sum (f,p)) = ( middle_sum (g,q)) by Lm16, A1;

    end;

    theorem :: INTEGR19:38

    

     Th38: for f be Function of A, ( REAL n), g be Function of A, ( REAL-NS n), T be DivSequence of A, p be sequence of (( REAL n) * ), q be sequence of (the carrier of ( REAL-NS n) * ) st f = g & p = q holds p is middle_volume_Sequence of f, T iff q is middle_volume_Sequence of g, T

    proof

      let f be Function of A, ( REAL n), g be Function of A, ( REAL-NS n), T be DivSequence of A, p be sequence of (( REAL n) * ), q be sequence of (the carrier of ( REAL-NS n) * );

      assume

       A1: f = g & p = q;

      hereby

        assume

         A2: p is middle_volume_Sequence of f, T;

        for k be Element of NAT holds (q . k) is middle_volume of g, (T . k)

        proof

          let k be Element of NAT ;

          

           A3: (p . k) is middle_volume of f, (T . k) by A2, INTEGR15:def 7;

          thus (q . k) is middle_volume of g, (T . k) by A1, A3, Th36;

        end;

        hence q is middle_volume_Sequence of g, T by INTEGR18:def 3;

      end;

      assume

       A4: q is middle_volume_Sequence of g, T;

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

      proof

        let k be Element of NAT ;

        

         A5: (q . k) is middle_volume of g, (T . k) by A4, INTEGR18:def 3;

        thus (p . k) is middle_volume of f, (T . k) by A1, A5, Th36;

      end;

      hence p is middle_volume_Sequence of f, T by INTEGR15:def 7;

    end;

    theorem :: INTEGR19:39

    

     Th39: for f be Function of A, ( REAL n), g be Function of A, ( REAL-NS n), T be DivSequence of A, S be middle_volume_Sequence of f, T, U be middle_volume_Sequence of g, T st f = g & S = U holds ( middle_sum (f,S)) = ( middle_sum (g,U))

    proof

      let f be Function of A, ( REAL n), g be Function of A, ( REAL-NS n), T be DivSequence of A, S be middle_volume_Sequence of f, T, U be middle_volume_Sequence of g, T;

      assume

       A1: f = g & S = U;

      

       A2: ( dom ( middle_sum (f,S))) = NAT by FUNCT_2:def 1

      .= ( dom ( middle_sum (g,U))) by FUNCT_2:def 1;

      now

        let x be object;

        assume x in ( dom ( middle_sum (f,S)));

        then

        reconsider n = x as Element of NAT ;

        

         A3: ( middle_sum (f,(S . n))) = ( middle_sum (g,(U . n))) by A1, Th37;

        

        thus (( middle_sum (f,S)) . x) = ( middle_sum (f,(S . n))) by INTEGR15:def 8

        .= (( middle_sum (g,U)) . x) by A3, INTEGR18:def 4;

      end;

      hence thesis by A2, FUNCT_1: 2;

    end;

    theorem :: INTEGR19:40

    

     Th40: for f be Function of A, ( REAL n), g be Function of A, ( REAL-NS n), I be Element of ( REAL n), J be Point of ( REAL-NS n) st f = g & I = J holds (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) iff (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))) = J)

    proof

      let f be Function of A, ( REAL n), g be Function of A, ( REAL-NS n), I be Element of ( REAL n), J be Point of ( REAL-NS n);

      assume

       A1: f = g & I = J;

      hereby

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

        

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

        thus for T be DivSequence of A, S0 be middle_volume_Sequence of g, T st ( delta T) is convergent & ( lim ( delta T)) = 0 holds ( middle_sum (g,S0)) is convergent & ( lim ( middle_sum (g,S0))) = J

        proof

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

          assume

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

          reconsider S = S0 as middle_volume_Sequence of f, T by A3, A1, Th38;

          ( middle_sum (f,S)) is convergent & ( lim ( middle_sum (f,S))) = I by A2, A4;

          hence thesis by A1, Th39;

        end;

      end;

      assume

       A5: 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))) = J;

      

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

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

      proof

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

        assume

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

        reconsider S = S0 as middle_volume_Sequence of g, T by A6, A1, Th38;

        ( middle_sum (g,S)) is convergent & ( lim ( middle_sum (g,S))) = I by A1, A5, A7;

        hence thesis by A1, Th39;

      end;

    end;

    theorem :: INTEGR19:41

    

     Th41: for f be Function of A, ( REAL n), g be Function of A, ( REAL-NS n) st f = g & f is bounded holds f is integrable iff g is integrable

    proof

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

      assume

       A1: f = g & f is bounded;

      hereby

        assume f is integrable;

        then

        consider I be Element of ( REAL n) such that

         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))) = I by A1, INTEGR15: 12;

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

        I = I0;

        then for T be DivSequence of A, S0 be middle_volume_Sequence of g, T st ( delta T) is convergent & ( lim ( delta T)) = 0 holds ( middle_sum (g,S0)) is convergent & ( lim ( middle_sum (g,S0))) = I0 by A2, A1, Th40;

        hence g is integrable;

      end;

      assume g is integrable;

      then

      consider I be Point of ( REAL-NS n) such that

       A3: 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))) = I;

      reconsider I0 = I as Element of ( REAL n) by REAL_NS1:def 4;

      I0 = I;

      then for T be DivSequence of A, S0 be middle_volume_Sequence of f, T st ( delta T) is convergent & ( lim ( delta T)) = 0 holds ( middle_sum (f,S0)) is convergent & ( lim ( middle_sum (f,S0))) = I0 by A3, A1, Th40;

      hence f is integrable by A1, INTEGR15: 12;

    end;

    theorem :: INTEGR19:42

    

     Th42: for f be Function of A, ( REAL n), g be Function of A, ( REAL-NS n) st f = g & f is bounded & f is integrable holds g is integrable & ( integral f) = ( integral g)

    proof

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

      assume

       A1: f = g & f is bounded & f is integrable;

      then

       A2: g is integrable by Th41;

      

       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))) = ( integral f) by A1, INTEGR15: 11;

      reconsider I0 = ( integral f) as Point of ( REAL-NS n) by REAL_NS1:def 4;

      ( integral f) = I0;

      then for T be DivSequence of A, S0 be middle_volume_Sequence of g, T st ( delta T) is convergent & ( lim ( delta T)) = 0 holds ( middle_sum (g,S0)) is convergent & ( lim ( middle_sum (g,S0))) = I0 by A3, A1, Th40;

      hence thesis by A2, INTEGR18:def 6;

    end;

    theorem :: INTEGR19:43

    

     Th43: for f be PartFunc of REAL , ( REAL n), g be PartFunc of REAL , ( REAL-NS n) st f = g & (f | A) is bounded & A c= ( dom f) holds f is_integrable_on A iff g is_integrable_on A

    proof

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

      assume

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

      reconsider h = (f | A) as Function of A, ( REAL n) by Lm3, A1;

      reconsider k = h as Function of A, ( REAL-NS n) by REAL_NS1:def 4;

      

       A2: h is bounded by A1;

      hereby

        assume f is_integrable_on A;

        then h is integrable by INTEGR15: 13;

        then k is integrable by A2, Th41;

        hence g is_integrable_on A by A1;

      end;

      assume g is_integrable_on A;

      then k is integrable by A1;

      then h is integrable by A2, Th41;

      hence thesis by INTEGR15: 13;

    end;

    theorem :: INTEGR19:44

    

     Th44: for f be PartFunc of REAL , ( REAL n), g be PartFunc of REAL , ( REAL-NS n) st f = g & (f | A) is bounded & A c= ( dom f) & f is_integrable_on A holds g is_integrable_on A & ( integral (f,A)) = ( integral (g,A))

    proof

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

      assume

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

      hence g is_integrable_on A by Th43;

      reconsider h = (f | A) as Function of A, ( REAL n) by Lm3, A1;

      reconsider k = h as Function of A, ( REAL-NS n) by REAL_NS1:def 4;

      

       A2: ( integral (f,A)) = ( integral h) by INTEGR15: 14;

      

       A3: h is bounded by A1;

      h is integrable by A1, INTEGR15: 13;

      then ( integral h) = ( integral k) by A3, Th42;

      hence thesis by A2, A1, INTEGR18: 9;

    end;

    theorem :: INTEGR19:45

    

     Th45: for f be PartFunc of REAL , ( REAL n), g be PartFunc of REAL , ( REAL-NS n) st f = g & a <= b & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & f is_integrable_on ['a, b'] holds ( integral (f,a,b)) = ( integral (g,a,b))

    proof

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

      assume

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

      

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

      

       A3: ( integral (g, ['a, b'])) = ( integral (f, ['a, b'])) by A1, Th44;

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

      hence thesis by A3, A2, INTEGR15: 19;

    end;

    theorem :: INTEGR19:46

    for f,g be PartFunc of REAL , ( REAL-NS n) st a <= b & f is_integrable_on ['a, b'] & g is_integrable_on ['a, b'] & ['a, b'] c= ( dom f) & ['a, b'] c= ( dom g) holds ( integral ((f + g),a,b)) = (( integral (f,a,b)) + ( integral (g,a,b))) & ( integral ((f - g),a,b)) = (( integral (f,a,b)) - ( integral (g,a,b)))

    proof

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

      assume

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

      

       A2: (f + g) is_integrable_on ['a, b'] & ( integral ((f + g), ['a, b'])) = (( integral (f, ['a, b'])) + ( integral (g, ['a, b']))) by A1, INTEGR18: 14;

      

       A3: (f - g) is_integrable_on ['a, b'] & ( integral ((f - g), ['a, b'])) = (( integral (f, ['a, b'])) - ( integral (g, ['a, b']))) by A1, INTEGR18: 15;

      

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

      

      thus ( integral ((f + g),a,b)) = ( integral ((f + g), ['a, b'])) by A4, INTEGR18: 16

      .= (( integral (f,a,b)) + ( integral (g, ['a, b']))) by A4, A2, INTEGR18: 16

      .= (( integral (f,a,b)) + ( integral (g,a,b))) by A4, INTEGR18: 16;

      

      thus ( integral ((f - g),a,b)) = ( integral ((f - g), ['a, b'])) by A4, INTEGR18: 16

      .= (( integral (f,a,b)) - ( integral (g, ['a, b']))) by A4, A3, INTEGR18: 16

      .= (( integral (f,a,b)) - ( integral (g,a,b))) by A4, INTEGR18: 16;

    end;

    theorem :: INTEGR19:47

    

     Th47: for f be PartFunc of REAL , ( REAL-NS n) st a <= b & ['a, b'] c= ( dom f) holds ( integral (f,b,a)) = ( - ( integral (f,a,b)))

    proof

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

      assume

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

      then

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

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

      hence thesis by A2, A1, INTEGR18: 18;

    end;

    theorem :: INTEGR19:48

    

     Th48: for f be PartFunc of REAL , ( REAL-NS n), g be PartFunc of REAL , ( REAL n) st f = g & a <= b & ['a, b'] c= ( dom f) & (f | ['a, b']) is bounded & f is_integrable_on ['a, b'] & c in ['a, b'] & d in ['a, b'] holds ( integral (f,c,d)) = ( integral (g,c,d))

    proof

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

      assume

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

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

      then

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

      

       A3: (g | ['a, b']) is bounded by A1, Th34;

      

       A4: g is_integrable_on ['a, b'] by Th43, A3, A1;

      per cases ;

        suppose

         A5: c <= d;

         ['c, d'] c= ( dom g) & (g | ['c, d']) is bounded & g is_integrable_on ['c, d'] by A3, A4, A1, Th9, A2, A5, Th2;

        hence ( integral (f,c,d)) = ( integral (g,c,d)) by A1, A5, Th45;

      end;

        suppose

         A6: not c <= d;

        

         A7: ['d, c'] c= ( dom g) & (g | ['d, c']) is bounded & g is_integrable_on ['d, c'] by A3, A4, A1, Th9, A2, A6, Th2;

        then

         A8: ( integral (f,d,c)) = ( integral (g,d,c)) by A1, A6, Th45;

        

        thus ( integral (g,c,d)) = ( - ( integral (g,d,c))) by Th33

        .= ( - ( integral (f,d,c))) by A8, REAL_NS1: 4

        .= ( integral (f,c,d)) by A6, A7, A1, Th47;

      end;

    end;

    theorem :: INTEGR19:49

    for f,g be PartFunc of REAL , ( REAL-NS n) st a <= b & f is_integrable_on ['a, b'] & g is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & (g | ['a, b']) is bounded & ['a, b'] c= ( dom f) & ['a, b'] c= ( dom g) & c in ['a, b'] & d in ['a, b'] holds ( integral ((f + g),c,d)) = (( integral (f,c,d)) + ( integral (g,c,d)))

    proof

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

      assume

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

      reconsider f1 = f, g1 = g as PartFunc of REAL , ( REAL n) by REAL_NS1:def 4;

      

       A2: (f1 | ['a, b']) is bounded by Th34, A1;

      

       A3: (g1 | ['a, b']) is bounded by Th34, A1;

      

       A4: f1 is_integrable_on ['a, b'] by Th43, A2, A1;

      

       A5: g1 is_integrable_on ['a, b'] by Th43, A3, A1;

      

       A6: (f1 + g1) = (f + g) by NFCONT_4: 5;

      

       A7: ( integral (f1,c,d)) = ( integral (f,c,d)) & ( integral (g1,c,d)) = ( integral (g,c,d)) by A1, Th48;

      

       A8: ['a, b'] c= ( dom (f + g)) by A1, A6, Th4;

      (f1 + g1) is_integrable_on ['a, b'] & ((f1 + g1) | ['a, b']) is bounded by A1, A2, A3, A4, A5, Th10;

      then (f + g) is_integrable_on ['a, b'] & ((f + g) | ['a, b']) is bounded by Th43, A6, A8, Th34;

      

      hence ( integral ((f + g),c,d)) = ( integral ((f1 + g1),c,d)) by A1, A8, Th48, NFCONT_4: 5

      .= (( integral (f1,c,d)) + ( integral (g1,c,d))) by A1, A2, A3, A4, A5, Th27

      .= (( integral (f,c,d)) + ( integral (g,c,d))) by A7, REAL_NS1: 2;

    end;

    theorem :: INTEGR19:50

    

     Th50: for f,g be PartFunc of REAL , ( REAL-NS n) st a <= b & f is_integrable_on ['a, b'] & g is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & (g | ['a, b']) is bounded & ['a, b'] c= ( dom f) & ['a, b'] c= ( dom g) & c in ['a, b'] & d in ['a, b'] holds ( integral ((f - g),c,d)) = (( integral (f,c,d)) - ( integral (g,c,d)))

    proof

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

      assume

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

      reconsider f1 = f, g1 = g as PartFunc of REAL , ( REAL n) by REAL_NS1:def 4;

      

       A2: (f1 | ['a, b']) is bounded by Th34, A1;

      

       A3: (g1 | ['a, b']) is bounded by Th34, A1;

      

       A4: f1 is_integrable_on ['a, b'] by Th43, A2, A1;

      

       A5: g1 is_integrable_on ['a, b'] by Th43, A3, A1;

      

       A6: (f1 - g1) = (f - g) by NFCONT_4: 10;

      

       A7: ( integral (f1,c,d)) = ( integral (f,c,d)) & ( integral (g1,c,d)) = ( integral (g,c,d)) by A1, Th48;

      

       A8: ['a, b'] c= ( dom (f - g)) by A1, A6, Th5;

      (f1 - g1) is_integrable_on ['a, b'] & ((f1 - g1) | ['a, b']) is bounded by A1, A2, A3, A4, A5, Th13;

      then (f - g) is_integrable_on ['a, b'] & ((f - g) | ['a, b']) is bounded by Th43, A6, A8, Th34;

      

      hence ( integral ((f - g),c,d)) = ( integral ((f1 - g1),c,d)) by A1, A8, Th48, NFCONT_4: 10

      .= (( integral (f1,c,d)) - ( integral (g1,c,d))) by A1, A2, A3, A4, A5, Th28

      .= (( integral (f,c,d)) - ( integral (g,c,d))) by A7, REAL_NS1: 5;

    end;

    theorem :: INTEGR19:51

    

     Th51: for E be Point of ( REAL-NS n), f be PartFunc of REAL , ( REAL-NS n) st (a <= b & ['a, b'] c= ( dom f) & for x be Real st x in ['a, b'] holds (f . x) = E) holds f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ( integral (f,a,b)) = ((b - a) * E)

    proof

      let e be Point of ( REAL-NS n), f be PartFunc of REAL , ( REAL-NS n);

      assume

       A1: a <= b & ['a, b'] c= ( dom f) & for x be Real st x in ['a, b'] holds (f . x) = e;

      reconsider f1 = f as PartFunc of REAL , ( REAL n) by REAL_NS1:def 4;

      reconsider e1 = e as Element of ( REAL n) by REAL_NS1:def 4;

      

       A2: for x be Real st x in ['a, b'] holds (f1 . x) = e1 by A1;

      

       A3: f1 is_integrable_on ['a, b'] & (f1 | ['a, b']) is bounded & ( integral (f1,a,b)) = ((b - a) * e1) by Th29, A1, A2;

      ( integral (f1,a,b)) = ( integral (f,a,b)) by A3, A1, Th45;

      hence thesis by A3, Th43, A1, Th34, REAL_NS1: 3;

    end;

    theorem :: INTEGR19:52

    

     Th52: for E be Point of ( REAL-NS n), f be PartFunc of REAL , ( REAL-NS n) st a <= b & ['a, b'] c= ( dom f) & (for x be Real st x in ['a, b'] holds (f . x) = E) & c in ['a, b'] & d in ['a, b'] holds ( integral (f,c,d)) = ((d - c) * E)

    proof

      let e be Point of ( REAL-NS n), f be PartFunc of REAL , ( REAL-NS n);

      assume

       A1: a <= b & ['a, b'] c= ( dom f) & (for x be Real st x in ['a, b'] holds (f . x) = e) & c in ['a, b'] & d in ['a, b'];

      reconsider f1 = f as PartFunc of REAL , ( REAL n) by REAL_NS1:def 4;

      reconsider e1 = e as Element of ( REAL n) by REAL_NS1:def 4;

      

       A2: for x be Real st x in ['a, b'] holds (f1 . x) = e1 by A1;

      

       A3: f1 is_integrable_on ['a, b'] & (f1 | ['a, b']) is bounded & ( integral (f1,a,b)) = ((b - a) * e1) by Th29, A1, A2;

      

       A4: ( integral (f1,c,d)) = ((d - c) * e1) by Th30, A1;

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

      then

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

      per cases ;

        suppose

         A6: c <= d;

        

         A7: ['c, d'] c= ( dom f1) & (f1 | ['c, d']) is bounded & f1 is_integrable_on ['c, d'] by A3, A1, Th9, A5, A6, Th2;

        ( integral (f1,c,d)) = ( integral (f,c,d)) by A7, A6, Th45;

        hence ( integral (f,c,d)) = ((d - c) * e) by A4, REAL_NS1: 3;

      end;

        suppose

         A8: not c <= d;

        

         A9: ['d, c'] c= ( dom f1) & (f1 | ['d, c']) is bounded & f1 is_integrable_on ['d, c'] by A3, A1, Th9, A5, A8, Th2;

        

         A10: ( integral (f1,d,c)) = ( integral (f,d,c)) by A9, A8, Th45;

        ( integral (f1,c,d)) = ( - ( integral (f1,d,c))) by Th33

        .= ( - ( integral (f,d,c))) by A10, REAL_NS1: 4

        .= ( integral (f,c,d)) by A8, A9, Th47;

        hence ( integral (f,c,d)) = ((d - c) * e) by A4, REAL_NS1: 3;

      end;

    end;

    theorem :: INTEGR19:53

    

     Th53: for f be PartFunc of REAL , ( REAL-NS n) st a <= b & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'] holds ( integral (f,a,d)) = (( integral (f,a,c)) + ( integral (f,c,d)))

    proof

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

      assume

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

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

      then

       A2: a in ['a, b'] & b in ['a, b'] by A1;

      reconsider f1 = f as PartFunc of REAL , ( REAL n) by REAL_NS1:def 4;

      

       A3: (f1 | ['a, b']) is bounded by A1, Th34;

      

       A4: f1 is_integrable_on ['a, b'] by Th43, A3, A1;

      

       A5: ( integral (f1,a,d)) = (( integral (f1,a,c)) + ( integral (f1,c,d))) by A3, A4, A1, Th31;

      

       A6: ( integral (f,a,d)) = ( integral (f1,a,d)) by A2, Th48, A1;

      

       A7: ( integral (f,a,c)) = ( integral (f1,a,c)) by A2, Th48, A1;

      ( integral (f,c,d)) = ( integral (f1,c,d)) by Th48, A1;

      hence ( integral (f,a,d)) = (( integral (f,a,c)) + ( integral (f,c,d))) by A7, A5, A6, REAL_NS1: 2;

    end;

    theorem :: INTEGR19:54

    

     Th54: for f be PartFunc of REAL , ( REAL-NS n) st (a <= b & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'] & for x be Real st x in ['( min (c,d)), ( max (c,d))'] holds ||.(f /. x).|| <= e) holds ||.( integral (f,c,d)).|| <= ((n * e) * |.(d - c).|)

    proof

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

      assume

       A1: (a <= b & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'] & for x be Real st x in ['( min (c,d)), ( max (c,d))'] holds ||.(f /. x).|| <= e);

      reconsider f1 = f as PartFunc of REAL , ( REAL n) by REAL_NS1:def 4;

      

       A2: (f1 | ['a, b']) is bounded by A1, Th34;

      

       A3: f1 is_integrable_on ['a, b'] by Th43, A2, A1;

      for x be Real st x in ['( min (c,d)), ( max (c,d))'] holds |.(f1 /. x).| <= e

      proof

        let x be Real;

        assume

         A4: x in ['( min (c,d)), ( max (c,d))'];

        then

         A5: ||.(f /. x).|| <= e by A1;

         ['( min (c,d)), ( max (c,d))'] c= ['a, b'] by A1, Lm2;

        then

         A6: x in ['a, b'] by A4;

        

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

        .= (f1 /. x) by A6, A1, PARTFUN1:def 6;

        hence |.(f1 /. x).| <= e by A5, REAL_NS1: 1;

      end;

      then |.( integral (f1,c,d)).| <= ((n * e) * |.(d - c).|) by A1, A2, A3, Th32;

      hence thesis by Th48, A1, REAL_NS1: 1;

    end;

    begin

    

     Lm17: for X be RealNormSpace, x be Point of X holds ||.((a " ) * x).|| = ( ||.x.|| / |.a.|)

    proof

      let X be RealNormSpace, x be Point of X;

      

      thus ||.((a " ) * x).|| = ( |.(a " ).| * ||.x.||) by NORMSP_1:def 1

      .= (( |.a.| " ) * ||.x.||) by COMPLEX1: 66

      .= ((1 / |.a.|) * ||.x.||) by XCMPLX_1: 215

      .= ( ||.x.|| / |.a.|) by XCMPLX_1: 99;

    end;

    theorem :: INTEGR19:55

    

     Th55: for n be non zero Element of NAT , F,f be PartFunc of REAL , ( REAL-NS n) st a <= b & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & ].a, b.[ c= ( dom F) & (for x be Real st x in ].a, b.[ holds (F . x) = ( integral (f,a,x))) & x0 in ].a, b.[ & f is_continuous_in x0 holds F is_differentiable_in x0 & ( diff (F,x0)) = (f /. x0)

    proof

      let n be non zero Element of NAT , F,f be PartFunc of REAL , ( REAL-NS n);

      deffunc F2( object) = ( 0. ( REAL-NS n));

      assume that

       A1: a <= b and

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

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

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

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

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

       A7: x0 in ].a, b.[ and

       A8: f is_continuous_in x0;

      defpred C1[ object] means (x0 + ( In ($1, REAL ))) in ].a, b.[;

      deffunc F0( Real) = ($1 * (f /. x0));

      consider L be Function of REAL , ( REAL-NS n) such that

       A9: for h be Element of REAL holds (L . h) = F0(h) from FUNCT_2:sch 4;

      

       A10: for h be Real holds (L . h) = F0(h)

      proof

        let h be Real;

        reconsider h as Element of REAL by XREAL_0:def 1;

        (L . h) = F0(h) by A9;

        hence thesis;

      end;

      

       A11: for h be Real holds (L /. h) = F0(h)

      proof

        let h be Real;

        reconsider h as Element of REAL by XREAL_0:def 1;

        (L /. h) = (L . h)

        .= F0(h) by A9;

        hence thesis;

      end;

      then

      reconsider L as LinearFunc of ( REAL-NS n) by NDIFF_3:def 2;

      deffunc F1( object) = (((F /. (x0 + ( In ($1, REAL )))) - (F /. x0)) - (L . ( In ($1, REAL ))));

      consider R be Function such that

       A12: ( dom R) = REAL & for x be object st x in REAL holds ( C1[x] implies (R . x) = F1(x)) & ( not C1[x] implies (R . x) = F2(x)) from PARTFUN1:sch 1;

      ( rng R) c= the carrier of ( REAL-NS n)

      proof

        let y be object;

        assume y in ( rng R);

        then

        consider x be object such that

         A13: x in ( dom R) and

         A14: y = (R . x) by FUNCT_1:def 3;

        

         A15: not C1[x] implies (R . x) = F2(x) by A12, A13;

         C1[x] implies (R . x) = F1(x) by A12, A13;

        hence thesis by A14, A15;

      end;

      then

      reconsider R as PartFunc of REAL , ( REAL-NS n) by A12, RELSET_1: 4;

      

       A16: R is total by A12, PARTFUN1:def 2;

      

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

      

       A18: for h be 0 -convergent non-zero Real_Sequence holds ((h " ) (#) (R /* h)) is convergent & ( lim ((h " ) (#) (R /* h))) = ( 0. ( REAL-NS n))

      proof

        let h be 0 -convergent non-zero Real_Sequence;

        set Z0 = ( 0. ( REAL-NS n));

        

         A19: for e be Real st 0 < e holds ex n be Nat st for m be Nat st n <= m holds ||.((((h " ) (#) (R /* h)) . m) - Z0).|| < e

        proof

          set g = ( REAL --> (f /. x0));

          let e0 be Real;

          set e = ((e0 / 2) / n);

          

           A20: h is convergent & ( lim h) = 0 ;

          assume

           A21: 0 < e0;

          then 0 < (e0 / 2) by XREAL_1: 215;

          then 0 < e by XREAL_1: 139;

          then

          consider p be Real such that

           A22: 0 < p and

           A23: for t be Real st t in ( dom f) & |.(t - x0).| < p holds ||.((f /. t) - (f /. x0)).|| < e by A8, NFCONT_3: 8;

          

           A24: 0 < (p / 2) by A22, XREAL_1: 215;

          

           A25: (p / 2) < p by A22, XREAL_1: 216;

          consider N be Neighbourhood of x0 such that

           A26: N c= ].a, b.[ by A7, RCOMP_1: 18;

          consider q be Real such that

           A27: 0 < q and

           A28: N = ].(x0 - q), (x0 + q).[ by RCOMP_1:def 6;

          

           A29: (q / 2) < q by A27, XREAL_1: 216;

          set r = ( min ((p / 2),(q / 2)));

           0 < (q / 2) by A27, XREAL_1: 215;

          then 0 < r by A24, XXREAL_0: 15;

          then

          consider n0 be Nat such that

           A30: for m be Nat st n0 <= m holds |.((h . m) - 0 ).| < r by A20, SEQ_2:def 7;

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

          take n0;

          let m be Nat;

          r <= (q / 2) by XXREAL_0: 17;

          then

           A31: ].(x0 - r), (x0 + r).[ c= ].(x0 - q), (x0 + q).[ by A29, INTEGRA6: 2, XXREAL_0: 2;

          assume n0 <= m;

          then

           A32: |.((h . m) - 0 ).| < r by A30;

          then |.((x0 + (h . m)) - x0).| < r;

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

          then

           A33: (x0 + (h . m)) in ].(x0 - q), (x0 + q).[ by A31;

          then

           A34: (x0 + (h . m)) in ].a, b.[ by A26, A28;

          then (x0 + ( In ((h . m), REAL ))) in ].a, b.[;

          then (R . (h . m)) = (((F /. (x0 + ( In ((h . m), REAL )))) - (F /. x0)) - (L . ( In ((h . m), REAL )))) by A12;

          then (R . (h . m)) = (((F /. (x0 + (h . m))) - (F /. x0)) - (L . ( In ((h . m), REAL ))));

          then

           A35: (R . (h . m)) = (((F /. (x0 + (h . m))) - (F /. x0)) - (L . (h . m)));

          

           A36: (F /. x0) = (F . x0) by A7, A5, PARTFUN1:def 6

          .= ( integral (f,a,x0)) by A6, A7;

          (F /. (x0 + (h . m))) = (F . (x0 + (h . m))) by A34, A5, PARTFUN1:def 6

          .= ( integral (f,a,(x0 + (h . m)))) by A6, A26, A28, A33;

          then

           A37: (R . (h . m)) = ((( integral (f,a,(x0 + (h . m)))) - ( integral (f,a,x0))) - ((h . m) * (f /. x0))) by A36, A10, A35;

          

           A38: ( dom g) = REAL by FUNCT_2:def 1;

          then ( ['a, b'] /\ ['a, b']) c= (( dom f) /\ ( dom g)) by A4, XBOOLE_1: 27;

          then

           A39: ['a, b'] c= ( dom (f - g)) by VFUNCT_1:def 2;

          

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

          then

           A41: ( integral (f,a,(x0 + (h . m)))) = (( integral (f,a,x0)) + ( integral (f,x0,(x0 + (h . m))))) by A1, A2, A3, A4, A7, A17, A34, Th53;

          

           A42: r <= (p / 2) by XXREAL_0: 17;

          

           A43: for x be Real st x in ['( min (x0,(x0 + (h . m)))), ( max (x0,(x0 + (h . m))))'] holds ||.((f - g) /. x).|| <= e

          proof

            let x be Real;

            

             A44: ( min (x0,(x0 + (h . m)))) <= x0 & x0 <= ( max (x0,(x0 + (h . m)))) by XXREAL_0: 17, XXREAL_0: 25;

            assume x in ['( min (x0,(x0 + (h . m)))), ( max (x0,(x0 + (h . m))))'];

            then

             A45: x in [.( min (x0,(x0 + (h . m)))), ( max (x0,(x0 + (h . m)))).] by A44, INTEGRA5:def 3, XXREAL_0: 2;

             |.(x - x0).| <= |.(h . m).|

            proof

              per cases ;

                suppose x0 <= (x0 + (h . m));

                then x0 = ( min (x0,(x0 + (h . m)))) & (x0 + (h . m)) = ( max (x0,(x0 + (h . m)))) by XXREAL_0:def 9, XXREAL_0:def 10;

                then

                 A46: ex z be Real st x = z & x0 <= z & z <= (x0 + (h . m)) by A45;

                then 0 <= (x - x0) by XREAL_1: 48;

                then

                 A47: |.(x - x0).| = (x - x0) by ABSVALUE:def 1;

                

                 A48: (x - x0) <= ((x0 + (h . m)) - x0) by A46, XREAL_1: 9;

                then 0 <= (h . m) by A46, XREAL_1: 48;

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

              end;

                suppose

                 A49: not x0 <= (x0 + (h . m));

                then x0 = ( max (x0,(x0 + (h . m)))) & (x0 + (h . m)) = ( min (x0,(x0 + (h . m)))) by XXREAL_0:def 9, XXREAL_0:def 10;

                then

                 A50: ex z be Real st x = z & (x0 + (h . m)) <= z & z <= x0 by A45;

                then

                 A51: ((x0 + (h . m)) - x0) <= (x - x0) by XREAL_1: 9;

                per cases ;

                  suppose

                   A52: (x - x0) <> 0 ;

                  ((x0 + (h . m)) - x0) < (x0 - x0) by A49, XREAL_1: 14;

                  then

                   A53: |.(h . m).| = ( - (h . m)) by ABSVALUE:def 1;

                  (x - x0) < 0 by A50, A52, XREAL_1: 47;

                  then |.(x - x0).| = ( - (x - x0)) by ABSVALUE:def 1;

                  hence thesis by A51, A53, XREAL_1: 24;

                end;

                  suppose (x - x0) = 0 ;

                  then |.(x - x0).| = 0 by ABSVALUE:def 1;

                  hence thesis by COMPLEX1: 46;

                end;

              end;

            end;

            then

             A54: |.(x - x0).| < r by A32, XXREAL_0: 2;

            then x in ].(x0 - r), (x0 + r).[ by RCOMP_1: 1;

            then x in ].(x0 - q), (x0 + q).[ by A31;

            then x in ].a, b.[ by A26, A28;

            then

             A55: x in [.a, b.] by A40;

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

             |.(x - x0).| < (p / 2) by A42, A54, XXREAL_0: 2;

            then |.(x - x0).| < p by A25, XXREAL_0: 2;

            then ||.((f /. x) - (f /. x0)).|| <= e by A4, A17, A23, A55;

            then ||.((f /. x) - (g /. xx)).|| <= e by FUNCOP_1: 7;

            hence thesis by A17, A39, A55, VFUNCT_1:def 2;

          end;

          

           A56: for x be Real st x in ['a, b'] holds (g . x) = (f /. x0) by FUNCOP_1: 7;

          then

           A57: (g | ['a, b']) is bounded by A1, A38, Th51;

          then

           A58: ((f - g) | ( ['a, b'] /\ ['a, b'])) is bounded by A3, Th35;

          

           A59: m in NAT by ORDINAL1:def 12;

          ( rng h) c= ( dom R) by A12;

          then (((h . m) " ) * (R /. (h . m))) = (((h . m) " ) * ((R /* h) . m)) by FUNCT_2: 109, A59;

          then (((h . m) " ) * (R /. (h . m))) = (((h " ) . m) * ((R /* h) . m)) by VALUED_1: 10;

          then

           A60: (((h . m) " ) * (R /. (h . m))) = (((h " ) (#) (R /* h)) . m) by NDIFF_1:def 2;

          (h . m) <> 0 by SEQ_1: 5;

          then

           A61: 0 < |.(h . m).| by COMPLEX1: 47;

          

           A62: g is_integrable_on ['a, b'] by A1, A38, A56, Th51;

          then

           A63: ||.( integral ((f - g),x0,(x0 + (h . m)))).|| <= ((n * e) * |.((x0 + (h . m)) - x0).|) by A1, A7, A17, A40, A34, A58, A39, A43, Th54, A2, A4, A38, INTEGR18: 15;

          

           A64: ( integral (g,x0,(x0 + (h . m)))) = (((x0 + (h . m)) - x0) * (f /. x0)) by A1, A7, A17, A40, A34, A38, A56, Th52

          .= ((h . m) * (f /. x0));

          

           A65: ( integral ((f - g),x0,(x0 + (h . m)))) = (( integral (f,x0,(x0 + (h . m)))) - ( integral (g,x0,(x0 + (h . m))))) by A1, A2, A3, A4, A7, A17, A40, A34, A38, A62, A57, Th50;

          (R . (h . m)) = ((( integral (f,x0,(x0 + (h . m)))) + (( integral (f,a,x0)) - ( integral (f,a,x0)))) - ((h . m) * (f /. x0))) by A37, A41, RLVECT_1: 28

          .= ((( integral (f,x0,(x0 + (h . m)))) + Z0) - ((h . m) * (f /. x0))) by RLVECT_1: 15

          .= (( integral (f,x0,(x0 + (h . m)))) - ( integral (g,x0,(x0 + (h . m))))) by A64, RLVECT_1:def 4;

          then (R /. (h . m)) = ( integral ((f - g),x0,(x0 + (h . m)))) by A65, A12, PARTFUN1:def 6;

          then ||.(((h . m) " ) * (R /. (h . m))).|| = ( ||.(R /. (h . m)).|| / |.(h . m).|) & ( ||.(R /. (h . m)).|| / |.(h . m).|) <= (((n * e) * |.(h . m).|) / |.(h . m).|) by A63, A61, Lm17, XREAL_1: 72;

          then ||.(((h . m) " ) * (R /. (h . m))).|| <= (n * e) by A61, XCMPLX_1: 89;

          then

           A66: ||.(((h . m) " ) * (R /. (h . m))).|| <= (e0 / 2) by XCMPLX_1: 87;

          (e0 / 2) < e0 by A21, XREAL_1: 216;

          then ||.(((h " ) (#) (R /* h)) . m).|| < e0 by A66, A60, XXREAL_0: 2;

          hence thesis by RLVECT_1: 13;

        end;

        hence ((h " ) (#) (R /* h)) is convergent by NORMSP_1:def 6;

        hence thesis by A19, NORMSP_1:def 7;

      end;

      consider N be Neighbourhood of x0 such that

       A67: N c= ].a, b.[ by A7, RCOMP_1: 18;

      reconsider R as RestFunc of ( REAL-NS n) by A16, A18, NDIFF_3:def 1;

      

       A68: for x be Real st x in N holds ((F /. x) - (F /. x0)) = ((L /. (x - x0)) + (R /. (x - x0)))

      proof

        let x be Real;

        assume x in N;

        then (x0 + (x - x0)) in N;

        then

         A69: (x0 + ( In ((x - x0), REAL ))) in N;

        then

         A70: (x0 + ( In ((x - x0), REAL ))) = (x0 + (x - x0)) & (R . (x - x0)) = F1(-) by A12, A67;

        (x0 + ( In ((x - x0), REAL ))) in ].a, b.[ by A69, A67;

        then

         A71: C1[(x - x0)];

        (R /. (x - x0)) = (R . (x - x0)) by A12, PARTFUN1:def 6, A70

        .= F1(-) by A12, A71

        .= (((F /. (x0 + ( In ((x - x0), REAL )))) - (F /. x0)) - (L . ( In ((x - x0), REAL ))))

        .= (((F /. (x0 + ( In ((x - x0), REAL )))) - (F /. x0)) - (L /. ( In ((x - x0), REAL ))))

        .= (((F /. x) - (F /. x0)) - (L /. (x - x0)));

        

        then ((R /. (x - x0)) + (L /. (x - x0))) = (((F /. x) - (F /. x0)) - ((L /. (x - x0)) - (L /. (x - x0)))) by RLVECT_1: 29

        .= (((F /. x) - (F /. x0)) - ( 0. ( REAL-NS n))) by RLVECT_1: 15

        .= ((F /. x) - (F /. x0)) by RLVECT_1: 13;

        hence thesis;

      end;

      

       A72: N c= ( dom F) by A5, A67;

      hence

       A73: F is_differentiable_in x0 by A68, NDIFF_3:def 3;

      reconsider N1 = 1 as Real;

      (L /. 1) = (N1 * (f /. x0)) by A11

      .= (f /. x0) by RLVECT_1:def 8;

      hence thesis by A72, A68, A73, NDIFF_3:def 4;

    end;

    

     Lm18: for f be PartFunc of REAL , ( REAL-NS n) holds ex F be PartFunc of REAL , ( REAL-NS n) st ].a, b.[ c= ( dom F) & for x be Real st x in ].a, b.[ holds (F . x) = ( integral (f,a,x))

    proof

      deffunc G( Real) = ( 0. ( REAL-NS n));

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

      defpred C[ set] means $1 in ].a, b.[;

      deffunc F( Real) = ( integral (f,a,$1));

      consider F be Function such that

       A1: ( dom F) = REAL & for x be Element of REAL holds ( C[x] implies (F . x) = F(x)) & ( not C[x] implies (F . x) = G(x)) from PARTFUN1:sch 4;

      now

        let y be object;

        assume y in ( rng F);

        then

        consider x be object such that

         A2: x in ( dom F) and

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

        reconsider x as Element of REAL by A1, A2;

         A4:

        now

          assume not x in ].a, b.[;

          then (F . x) = ( 0. ( REAL-NS n)) by A1;

          hence y in the carrier of ( REAL-NS n) by A3;

        end;

        now

          assume x in ].a, b.[;

          then (F . x) = ( integral (f,a,x)) by A1;

          hence y in the carrier of ( REAL-NS n) by A3;

        end;

        hence y in the carrier of ( REAL-NS n) by A4;

      end;

      then ( rng F) c= the carrier of ( REAL-NS n);

      then

      reconsider F as PartFunc of REAL , ( REAL-NS n) by A1, RELSET_1: 4;

      take F;

      thus thesis by A1;

    end;

    theorem :: INTEGR19:56

    for n be non zero Element of NAT , f be PartFunc of REAL , ( REAL-NS n) st a <= b & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & x0 in ].a, b.[ & f is_continuous_in x0 holds ex F be PartFunc of REAL , ( REAL-NS n) st ].a, b.[ c= ( dom F) & (for x be Real st x in ].a, b.[ holds (F . x) = ( integral (f,a,x))) & F is_differentiable_in x0 & ( diff (F,x0)) = (f /. x0)

    proof

      let n be non zero Element of NAT ;

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

      consider F be PartFunc of REAL , ( REAL-NS n) such that

       A1: ].a, b.[ c= ( dom F) & for x be Real st x in ].a, b.[ holds (F . x) = ( integral (f,a,x)) by Lm18;

      assume a <= b & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & x0 in ].a, b.[ & f is_continuous_in x0;

      then F is_differentiable_in x0 & ( diff (F,x0)) = (f /. x0) by A1, Th55;

      hence thesis by A1;

    end;