integr20.miz



    begin

    reserve s1,s2,q1 for Real_Sequence;

    definition

      let X be RealNormSpace;

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

      :: INTEGR20:def1

      attr f is uniformly_continuous means for r be Real st 0 < r holds ex s be Real st 0 < s & for x1,x2 be Real st x1 in ( dom f) & x2 in ( dom f) & |.(x1 - x2).| < s holds ||.((f /. x1) - (f /. x2)).|| < r;

    end

    theorem :: INTEGR20:1

    

     Th1: for X be set, Y be RealNormSpace, f be PartFunc of REAL , the carrier of Y holds (f | X) is uniformly_continuous iff for r be Real st 0 < r holds ex s be Real st 0 < s & for x1,x2 be Real st x1 in ( dom (f | X)) & x2 in ( dom (f | X)) & |.(x1 - x2).| < s holds ||.((f /. x1) - (f /. x2)).|| < r

    proof

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

      thus (f | X) is uniformly_continuous implies for r be Real st 0 < r holds ex s be Real st 0 < s & for x1,x2 be Real st x1 in ( dom (f | X)) & x2 in ( dom (f | X)) & |.(x1 - x2).| < s holds ||.((f /. x1) - (f /. x2)).|| < r

      proof

        assume

         A1: (f | X) is uniformly_continuous;

        let r be Real;

        assume 0 < r;

        then

        consider s be Real such that

         A2: 0 < s and

         A3: for x1,x2 be Real st x1 in ( dom (f | X)) & x2 in ( dom (f | X)) & |.(x1 - x2).| < s holds ||.(((f | X) /. x1) - ((f | X) /. x2)).|| < r by A1;

        take s;

        thus 0 < s by A2;

        let x1,x2 be Real;

        assume

         A4: x1 in ( dom (f | X)) & x2 in ( dom (f | X));

        then ((f | X) /. x1) = (f /. x1) & ((f | X) /. x2) = (f /. x2) by PARTFUN1: 80;

        hence thesis by A3, A4;

      end;

      assume

       A5: for r be Real st 0 < r holds ex s be Real st 0 < s & for x1,x2 be Real st x1 in ( dom (f | X)) & x2 in ( dom (f | X)) & |.(x1 - x2).| < s holds ||.((f /. x1) - (f /. x2)).|| < r;

      let r be Real;

      assume 0 < r;

      then

      consider s be Real such that

       A6: 0 < s and

       A7: for x1,x2 be Real st x1 in ( dom (f | X)) & x2 in ( dom (f | X)) & |.(x1 - x2).| < s holds ||.((f /. x1) - (f /. x2)).|| < r by A5;

      take s;

      thus 0 < s by A6;

      let x1,x2 be Real;

      assume

       A8: x1 in ( dom (f | X)) & x2 in ( dom (f | X));

      then ((f | X) /. x1) = (f /. x1) & ((f | X) /. x2) = (f /. x2) by PARTFUN1: 80;

      hence thesis by A7, A8;

    end;

    theorem :: INTEGR20:2

    for X,X1 be set, Y be RealNormSpace, f be PartFunc of REAL , the carrier of Y holds (f | X) is uniformly_continuous & X1 c= X implies (f | X1) is uniformly_continuous

    proof

      let X,X1 be set, Y be RealNormSpace, f be PartFunc of REAL , the carrier of Y;

      assume that

       A1: (f | X) is uniformly_continuous and

       A2: X1 c= X;

      now

        let r be Real;

        assume 0 < r;

        then

        consider s be Real such that

         A3: 0 < s and

         A4: for x1,x2 be Real st x1 in ( dom (f | X)) & x2 in ( dom (f | X)) & |.(x1 - x2).| < s holds ||.((f /. x1) - (f /. x2)).|| < r by A1, Th1;

        take s;

        thus 0 < s by A3;

        let x1,x2 be Real;

        assume that

         A5: x1 in ( dom (f | X1)) & x2 in ( dom (f | X1)) & |.(x1 - x2).| < s;

        (f | X1) c= (f | X) by A2, RELAT_1: 75;

        then ( dom (f | X1)) c= ( dom (f | X)) by RELAT_1: 11;

        hence ||.((f /. x1) - (f /. x2)).|| < r by A4, A5;

      end;

      hence thesis by Th1;

    end;

    theorem :: INTEGR20:3

    

     Th3: for X be RealNormSpace, f be PartFunc of REAL , the carrier of X, Z be Subset of REAL st Z c= ( dom f) & Z is compact & (f | Z) is continuous holds (f | Z) is uniformly_continuous

    proof

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

      assume that

       A1: Z c= ( dom f) and

       A2: Z is compact and

       A3: (f | Z) is continuous;

      assume not thesis;

      then

      consider r be Real such that

       A4: 0 < r and

       A5: for s be Real st 0 < s holds ex x1,x2 be Real st x1 in ( dom (f | Z)) & x2 in ( dom (f | Z)) & |.(x1 - x2).| < s & not ||.((f /. x1) - (f /. x2)).|| < r by Th1;

      defpred P[ Element of NAT , Real] means $2 in Z & ex x2 be Element of REAL st x2 in Z & |.($2 - x2).| < (1 / ($1 + 1)) & not ||.((f /. $2) - (f /. x2)).|| < r;

       A6:

      now

        let n be Element of NAT ;

        consider x1 be Real such that

         A7: ex x2 be Real st x1 in ( dom (f | Z)) & x2 in ( dom (f | Z)) & |.(x1 - x2).| < (1 / (n + 1)) & not ||.((f /. x1) - (f /. x2)).|| < r by A5;

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

        take x1;

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

        hence P[n, x1] by A7;

      end;

      consider s1 such that

       A8: for n be Element of NAT holds P[n, (s1 . n)] from FUNCT_2:sch 3( A6);

       A9:

      now

        let x be object;

        assume x in ( rng s1);

        then ex n be Element of NAT st x = (s1 . n) by FUNCT_2: 113;

        hence x in Z by A8;

      end;

      then ( rng s1) c= Z;

      then

      consider q1 such that

       A10: q1 is subsequence of s1 & q1 is convergent & ( lim q1) in Z by A2;

      

       A11: (f | Z) is_continuous_in ( lim q1) by A3, A1, A10, RELAT_1: 57;

      ( rng q1) c= ( rng s1) by A10, VALUED_0: 21;

      then ( rng q1) c= Z & ( rng q1) c= ( dom f) by A1, A9;

      then ( rng q1) c= (( dom f) /\ Z) by XBOOLE_1: 19;

      then

       A12: ( rng q1) c= ( dom (f | Z)) by RELAT_1: 61;

      then

       A13: ((f | Z) /. ( lim q1)) = ( lim ((f | Z) /* q1)) & ((f | Z) /* q1) is convergent by A10, A11;

      defpred P[ Element of NAT , Real] means $2 in Z & |.((s1 . $1) - $2).| < (1 / ($1 + 1)) & not ||.((f /. (s1 . $1)) - (f /. $2)).|| < r;

      

       A14: for n be Element of NAT holds ex x2 be Element of REAL st P[n, x2] by A8;

      consider s2 such that

       A15: for n be Element of NAT holds P[n, (s2 . n)] from FUNCT_2:sch 3( A14);

       A16:

      now

        let x be object;

        assume x in ( rng s2);

        then ex n be Element of NAT st x = (s2 . n) by FUNCT_2: 113;

        hence x in Z by A15;

      end;

      consider Ns1 be increasing sequence of NAT such that

       A17: q1 = (s1 * Ns1) by A10, VALUED_0:def 17;

      set q2 = (q1 - ((s1 - s2) * Ns1));

      now

        let n be Element of NAT ;

        

        thus (q2 . n) = (((s1 * Ns1) . n) - (((s1 - s2) * Ns1) . n)) by A17, RFUNCT_2: 1

        .= ((s1 . (Ns1 . n)) - (((s1 - s2) * Ns1) . n)) by FUNCT_2: 15

        .= ((s1 . (Ns1 . n)) - ((s1 - s2) . (Ns1 . n))) by FUNCT_2: 15

        .= ((s1 . (Ns1 . n)) - ((s1 . (Ns1 . n)) - (s2 . (Ns1 . n)))) by RFUNCT_2: 1

        .= ((s2 * Ns1) . n) by FUNCT_2: 15;

      end;

      then

       A18: q2 = (s2 * Ns1) & q2 is subsequence of s2 by FUNCT_2: 63;

      then ( rng q2) c= ( rng s2) by VALUED_0: 21;

      then ( rng q2) c= Z & ( rng q2) c= ( dom f) by A1, A16;

      then ( rng q2) c= (( dom f) /\ Z) by XBOOLE_1: 19;

      then

       A19: ( rng q2) c= ( dom (f | Z)) by RELAT_1: 61;

       A20:

      now

        let p be Real;

        assume

         A21: 0 < p;

        consider k be Nat such that

         A22: (p " ) < k by SEQ_4: 3;

        take k;

        let m be Nat;

        

         A23: m in NAT by ORDINAL1:def 12;

        assume k <= m;

        then (k + 1) <= (m + 1) by XREAL_1: 6;

        then (1 / (m + 1)) <= (1 / (k + 1)) by XREAL_1: 118;

        then

         A24: |.((s1 . m) - (s2 . m)).| < (1 / (k + 1)) by A15, XXREAL_0: 2, A23;

        k < (k + 1) by NAT_1: 13;

        then (p " ) < (k + 1) by A22, XXREAL_0: 2;

        then

         A25: (1 / (k + 1)) < (1 / (p " )) by A21, XREAL_1: 76;

         |.(((s1 - s2) . m) - 0 ).| = |.((s1 . m) - (s2 . m)).| by RFUNCT_2: 1;

        hence |.(((s1 - s2) . m) - 0 ).| < p by A25, A24, XXREAL_0: 2;

      end;

      then

       A26: (s1 - s2) is convergent by SEQ_2:def 6;

      

       A27: ((s1 - s2) * Ns1) is convergent by A20, SEQ_2:def 6, SEQ_4: 16;

      then

       A28: q2 is convergent by A10, SEQ_2: 11;

      ( lim (s1 - s2)) = 0 by A20, A26, SEQ_2:def 7;

      then ( lim ((s1 - s2) * Ns1)) = 0 by A20, SEQ_2:def 6, SEQ_4: 17;

      then ( lim q2) = (( lim q1) - 0 ) by A10, A27, SEQ_2: 12;

      then

       A29: ((f | Z) /* q2) is convergent & ((f | Z) /. ( lim q1)) = ( lim ((f | Z) /* q2)) by A11, A28, A19;

      then

       A30: (((f | Z) /* q1) - ((f | Z) /* q2)) is convergent by A13, NORMSP_1: 20;

      ( lim (((f | Z) /* q1) - ((f | Z) /* q2))) = (((f | Z) /. ( lim q1)) - ((f | Z) /. ( lim q1))) by A13, A29, NORMSP_1: 26;

      then

       A31: ( lim (((f | Z) /* q1) - ((f | Z) /* q2))) = ( 0. X) by RLVECT_1: 15;

      now

        let n be Nat;

        consider k be Nat such that

         A32: for m be Nat st k <= m holds ||.(((((f | Z) /* q1) - ((f | Z) /* q2)) . m) - ( 0. X)).|| < r by A4, A30, A31, NORMSP_1:def 7;

        

         A33: (q1 . k) in ( dom (f | Z)) & (q2 . k) in ( dom (f | Z)) by A12, A19, VALUED_0: 28;

        

         A34: k in NAT by ORDINAL1:def 12;

        

         A35: ||.(((((f | Z) /* q1) - ((f | Z) /* q2)) . k) - ( 0. X)).|| = ||.((((f | Z) /* q1) . k) - (((f | Z) /* q2) . k)).|| by NORMSP_1:def 3;

        (((f | Z) /* q1) . k) = ((f | Z) /. (q1 . k)) & (((f | Z) /* q2) . k) = ((f | Z) /. (q2 . k)) by A12, A19, FUNCT_2: 109, A34;

        then (((f | Z) /* q1) . k) = (f /. (q1 . k)) & (((f | Z) /* q2) . k) = (f /. (q2 . k)) by A33, PARTFUN1: 80;

        

        then ||.((((f | Z) /* q1) . k) - (((f | Z) /* q2) . k)).|| = ||.((f /. (s1 . (Ns1 . k))) - (f /. ((s2 * Ns1) . k))).|| by A17, A18, FUNCT_2: 15, ORDINAL1:def 12

        .= ||.((f /. (s1 . (Ns1 . k))) - (f /. (s2 . (Ns1 . k)))).|| by FUNCT_2: 15, ORDINAL1:def 12;

        hence contradiction by A15, A32, A35;

      end;

      hence contradiction;

    end;

    begin

    theorem :: INTEGR20:4

    

     Th4: for X be RealNormSpace, n,m be Nat, a be Function of [:( Seg n), ( Seg m):], X holds for p,q be FinSequence of X st (( dom p) = ( Seg n) & for i be Nat st i in ( dom p) holds ex r be FinSequence of X st (( dom r) = ( Seg m) & (p . i) = ( Sum r) & for j be Nat st j in ( dom r) holds (r . j) = (a . (i,j)))) & (( dom q) = ( Seg m) & for j be Nat st j in ( dom q) holds ex s be FinSequence of X st (( dom s) = ( Seg n) & (q . j) = ( Sum s) & for i be Nat st i in ( dom s) holds (s . i) = (a . (i,j)))) holds ( Sum p) = ( Sum q)

    proof

      let X be RealNormSpace;

      defpred P[ Nat] means for m be Nat, a be Function of [:( Seg $1), ( Seg m):], X holds for p,q be FinSequence of X st (( dom p) = ( Seg $1) & for i be Nat st i in ( dom p) holds ex r be FinSequence of X st (( dom r) = ( Seg m) & (p . i) = ( Sum r) & for j be Nat st j in ( dom r) holds (r . j) = (a . (i,j)))) & (( dom q) = ( Seg m) & for j be Nat st j in ( dom q) holds ex s be FinSequence of X st (( dom s) = ( Seg $1) & (q . j) = ( Sum s) & for i be Nat st i in ( dom s) holds (s . i) = (a . (i,j)))) holds ( Sum p) = ( Sum q);

      

       A1: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat such that

         A2: P[n];

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

        

         A3: ( Seg n) c= ( Seg (n + 1)) by FINSEQ_1: 5, NAT_1: 11;

        now

          let m be Nat, a be Function of [:( Seg (n + 1)), ( Seg m):], X;

          let p,q be FinSequence of X such that

           A4: ( dom p) = ( Seg (n + 1)) & for i be Nat st i in ( dom p) holds ex r be FinSequence of X st (( dom r) = ( Seg m) & (p . i) = ( Sum r) & for j be Nat st j in ( dom r) holds (r . j) = (a . (i,j))) and

           A5: ( dom q) = ( Seg m) & for j be Nat st j in ( dom q) holds ex s be FinSequence of X st (( dom s) = ( Seg (n + 1)) & (q . j) = ( Sum s) & for i be Nat st i in ( dom s) holds (s . i) = (a . (i,j)));

          

           A6: ( len p) = (n + 1) by A4, FINSEQ_1:def 3;

          set a0 = (a | [:( Seg n), ( Seg m):]);

           [:( Seg n), ( Seg m):] c= [:( Seg (n + 1)), ( Seg m):] by A3, ZFMISC_1: 95;

          then

          reconsider a0 as Function of [:( Seg n), ( Seg m):], X by FUNCT_2: 32;

          

           A7: ( dom a0) = [:( Seg n), ( Seg m):] by FUNCT_2:def 1;

          deffunc F( Nat) = (a . [(n + 1), $1]);

          reconsider p0 = (p | ( Seg n)) as FinSequence of X by FINSEQ_1: 18;

          

           A8: ( dom p0) = ( Seg n) by A4, A3, RELAT_1: 62;

          then

           A9: ( len p0) = n by FINSEQ_1:def 3;

           A10:

          now

            let i be Nat;

            assume

             A11: i in ( dom p0);

            then

            consider r be FinSequence of X such that

             A12: ( dom r) = ( Seg m) & (p . i) = ( Sum r) & for j be Nat st j in ( dom r) holds (r . j) = (a . (i,j)) by A4, A8, FINSEQ_2: 8;

            take r;

            thus ( dom r) = ( Seg m) & (p0 . i) = ( Sum r) by A11, A12, FUNCT_1: 47;

            thus for j be Nat st j in ( dom r) holds (r . j) = (a0 . (i,j))

            proof

              let j be Nat;

              assume

               A13: j in ( dom r);

              then (r . j) = (a . (i,j)) by A12;

              hence (r . j) = (a0 . (i,j)) by A8, A11, A12, A13, ZFMISC_1: 87, A7, FUNCT_1: 47;

            end;

          end;

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

          consider an be FinSequence such that

           A14: ( len an) = m & for j be Nat st j in ( dom an) holds (an . j) = F(j) from FINSEQ_1:sch 2;

          

           A15: ( dom an) = ( Seg m) by A14, FINSEQ_1:def 3;

          now

            let i be Nat;

            assume

             A16: i in ( dom an);

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

            then [(n + 1), i] in [:( Seg (n + 1)), ( Seg m):] by A16, A15, ZFMISC_1: 87;

            then (a . ((n + 1),i)) in the carrier of X by FUNCT_2: 5;

            hence (an . i) in the carrier of X by A16, A14;

          end;

          then

          reconsider an as FinSequence of X by FINSEQ_2: 12;

          

           A17: ( Sum an) = (p . (n + 1))

          proof

            consider r be FinSequence of X such that

             A18: ( dom r) = ( Seg m) & (p . (n + 1)) = ( Sum r) & for j be Nat st j in ( dom r) holds (r . j) = (a . ((n + 1),j)) by A4, FINSEQ_1: 4;

            now

              let j be Nat;

              assume

               A19: j in ( dom r);

              then (r . j) = (a . ((n + 1),j)) by A18;

              hence (r . j) = (an . j) by A14, A15, A18, A19;

            end;

            hence thesis by A14, FINSEQ_1:def 3, A18, FINSEQ_1: 13;

          end;

          set q0 = (q - an);

          

           A20: ( dom q0) = (( dom q) /\ ( dom an)) by VFUNCT_1:def 2;

          then

          reconsider q0 = (q - an) as FinSequence by A15, A5, FINSEQ_1:def 2;

          for i be Nat st i in ( dom q0) holds (q0 . i) in the carrier of X

          proof

            let i be Nat;

            assume i in ( dom q0);

            then (q0 . i) = ((q - an) /. i) by PARTFUN1:def 6;

            hence thesis;

          end;

          then

          reconsider q0 as FinSequence of the carrier of X by FINSEQ_2: 12;

          

           A21: ( len q0) = m by A5, A15, A20, FINSEQ_1:def 3;

           A22:

          now

            let j be Nat such that

             A23: j in ( dom q0);

            consider s be FinSequence of X such that

             A24: ( dom s) = ( Seg (n + 1)) & (q . j) = ( Sum s) & for i be Nat st i in ( dom s) holds (s . i) = (a . (i,j)) by A5, A15, A20, A23;

            

             A25: (s . (n + 1)) = (a . ((n + 1),j)) by A24, FINSEQ_1: 4;

            reconsider sn = (s | ( Seg n)) as FinSequence of X by FINSEQ_1: 18;

            take sn;

            

             A26: ( len s) = (n + 1) by A24, FINSEQ_1:def 3;

            (an /. j) = (an . j) by A23, A15, A5, A20, PARTFUN1:def 6;

            then (an /. j) = (s . (n + 1)) by A25, A14, A15, A5, A20, A23;

            then

             A27: (an /. j) = (s . ( len s)) by A24, FINSEQ_1:def 3;

            thus

             A28: ( dom sn) = ( Seg n) by A24, A3, RELAT_1: 62;

            then

             A29: ( len s) = (( len sn) + 1) by A26, FINSEQ_1:def 3;

            (q /. j) = ( Sum s) by A24, A23, A5, A15, A20, PARTFUN1:def 6;

            

            then ((q /. j) - (an /. j)) = ((( Sum sn) + (an /. j)) - (an /. j)) by A29, A28, RLVECT_1: 38, A27

            .= (( Sum sn) + ((an /. j) - (an /. j))) by RLVECT_1:def 3;

            then ((q /. j) - (an /. j)) = (( Sum sn) + ( 0. X)) by RLVECT_1: 15;

            then (q0 /. j) = ( Sum sn) by A23, VFUNCT_1:def 2;

            hence (q0 . j) = ( Sum sn) by A23, PARTFUN1:def 6;

            thus for i be Nat st i in ( dom sn) holds (sn . i) = (a0 . (i,j))

            proof

              let i be Nat such that

               A30: i in ( dom sn);

              (sn . i) = (s . i) by A30, FUNCT_1: 47;

              then (sn . i) = (a . (i,j)) by A24, A28, A30, A3;

              hence (sn . i) = (a0 . (i,j)) by A5, A15, A20, A23, A28, A30, ZFMISC_1: 87, A7, FUNCT_1: 47;

            end;

          end;

          for i be Nat st 1 <= i & i <= ( len q) holds (q /. i) = ((q0 /. i) + (an /. i))

          proof

            let i be Nat;

            assume 1 <= i & i <= ( len q);

            then i in ( dom q) by FINSEQ_3: 25;

            

            then ((q0 /. i) + (an /. i)) = (((q /. i) - (an /. i)) + (an /. i)) by A5, A15, A20, VFUNCT_1:def 2

            .= ((q /. i) - ((an /. i) - (an /. i))) by RLVECT_1: 29;

            then ((q0 /. i) + (an /. i)) = ((q /. i) - ( 0. X)) by RLVECT_1: 15;

            hence thesis;

          end;

          then

           A31: (q0 + an) = q by A5, A15, A20, BINOM:def 1;

          ( Sum p) = (( Sum p0) + ( Sum an)) by A8, A6, A9, RLVECT_1: 38, A17;

          then ( Sum p) = (( Sum q0) + ( Sum an)) by A2, A10, A8, A5, A15, A20, A22;

          hence ( Sum p) = ( Sum q) by A31, INTEGR18: 1, A14, A21;

        end;

        hence thesis;

      end;

      now

        let m be Nat, a be Function of [:( Seg 0 ), ( Seg m):], X;

        let p,q be FinSequence of X such that

         A32: ( dom p) = ( Seg 0 ) and for i be Nat st i in ( dom p) holds ex r be FinSequence of X st (( dom r) = ( Seg m) & (p . i) = ( Sum r) & for j be Nat st j in ( dom r) holds (r . j) = (a . (i,j))) and ( dom q) = ( Seg m) and

         A33: for j be Nat st j in ( dom q) holds ex s be FinSequence of X st (( dom s) = ( Seg 0 ) & (q . j) = ( Sum s) & for i be Nat st i in ( dom s) holds (s . i) = (a . (i,j)));

         A34:

        now

          let z be object;

          assume

           A35: z in ( dom q);

          then

          reconsider j = z as Nat;

          consider s be FinSequence of X such that

           A36: ( dom s) = ( Seg 0 ) & (q . j) = ( Sum s) & for i be Nat st i in ( dom s) holds (s . i) = (a . (i,j)) by A33, A35;

          s = ( <*> the carrier of X) by A36;

          hence (q . z) = ( 0. X) by A36, RLVECT_1: 43;

        end;

        

         A37: p = ( <*> the carrier of X) by A32;

        

         A38: ( len q) = ( len q);

        now

          let k be Nat, v be Element of X;

          assume

           A39: k in ( dom q) & v = (q . k);

          then (q . k) = ( 0. X) by A34;

          hence (q . k) = ( - v) by A39;

        end;

        then ( Sum q) = ( - ( Sum q)) by A38, RLVECT_1: 40;

        then ( Sum q) = ( 0. X) by RLVECT_1: 19;

        hence ( Sum p) = ( Sum q) by RLVECT_1: 43, A37;

      end;

      then

       A40: P[ 0 ];

      thus for n be Nat holds P[n] from NAT_1:sch 2( A40, A1);

    end;

    definition

      let A be Subset of REAL ;

      :: INTEGR20:def2

      func xvol A -> Real equals

      : Def2: 0 if A is empty

      otherwise ( vol A);

      correctness ;

    end

    reserve n for Element of NAT ;

    reserve a,b for Real;

    

     Lm1: 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 :: INTEGR20:5

    

     Th5: for A be real-bounded Subset of REAL holds 0 <= ( xvol A)

    proof

      let A be real-bounded Subset of REAL ;

      per cases ;

        suppose A <> {} ;

        then 0 <= ( vol A) by INTEGRA1: 9;

        hence 0 <= ( xvol A) by Def2;

      end;

        suppose A = {} ;

        hence 0 <= ( xvol A) by Def2;

      end;

    end;

    theorem :: INTEGR20:6

    

     Th6: for A be non empty closed_interval Subset of REAL , D be Division of A, q be FinSequence of REAL st ( dom q) = ( Seg ( len D)) & for i be Nat st i in ( Seg ( len D)) holds (q . i) = ( vol ( divset (D,i))) holds ( Sum q) = ( vol A)

    proof

      let A be non empty closed_interval Subset of REAL , D be Division of A, q be FinSequence of REAL ;

      assume

       A1: ( dom q) = ( Seg ( len D)) & for i be Nat st i in ( Seg ( len D)) holds (q . i) = ( vol ( divset (D,i)));

      set p = ( lower_volume (( chi (A,A)),D));

      ( dom q) = ( Seg ( len D)) by A1

      .= ( Seg ( len p)) by INTEGRA1:def 7;

      then

       A2: ( dom q) = ( dom p) by FINSEQ_1:def 3;

      for k be Nat st k in ( dom q) holds (q . k) = (p . k)

      proof

        let k be Nat;

        assume

         A3: k in ( dom q);

        then

         A4: (q . k) = ( vol ( divset (D,k))) by A1;

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

        hence thesis by A4, INTEGRA1: 19;

      end;

      then q = ( lower_volume (( chi (A,A)),D)) by A2, FINSEQ_1: 13;

      hence thesis by INTEGRA1: 23;

    end;

    theorem :: INTEGR20:7

    

     Th7: for Y be RealNormSpace, E be Point of Y, q be FinSequence of REAL , S be FinSequence of Y st ( len S) = ( len q) & for i be Nat st i in ( dom S) holds ex r be Real st r = (q . i) & (S . i) = (r * E) holds ( Sum S) = (( Sum q) * E)

    proof

      let Y be RealNormSpace, E be Point of Y;

      defpred P[ Nat] means for q be FinSequence of REAL , S be FinSequence of Y st $1 = ( len S) & ( len S) = ( len q) & for i be Nat st i in ( dom S) holds ex r be Real st r = (q . i) & (S . i) = (r * E) holds ( Sum S) = (( Sum q) * E);

      

       A1: P[ 0 ]

      proof

        let q be FinSequence of REAL , S be FinSequence of Y;

        assume 0 = ( len S) & ( len S) = ( len q) & for i be Nat st i in ( dom S) holds ex r be Real st r = (q . i) & (S . i) = (r * E);

        then

         A2: ( <*> the carrier of Y) = S & ( <*> REAL ) = q;

        then (( Sum q) * E) = ( 0. Y) by RLVECT_1: 10, RVSUM_1: 72;

        hence thesis by A2, RLVECT_1: 43;

      end;

       A3:

      now

        let i be Nat;

        assume

         A4: P[i];

        now

          let q be FinSequence of REAL , S be FinSequence of Y;

          set S0 = (S | i), q0 = (q | i);

          assume

           A5: (i + 1) = ( len S) & ( len S) = ( len q) & for i be Nat st i in ( dom S) holds ex r be Real st r = (q . i) & (S . i) = (r * E);

          

           A6: for k be Nat st k in ( dom S0) holds ex r be Real st r = (q0 . k) & (S0 . k) = (r * E)

          proof

            let k be Nat;

            assume k in ( dom S0);

            then

             A7: k in ( Seg i) & k in ( dom S) by RELAT_1: 57;

            then

            consider r be Real such that

             A8: r = (q . k) & (S . k) = (r * E) by A5;

            take r;

            thus thesis by A8, A7, FUNCT_1: 49;

          end;

          ( dom S) = ( Seg (i + 1)) by A5, FINSEQ_1:def 3;

          then

          consider r be Real such that

           A9: r = (q . (i + 1)) & (S . (i + 1)) = (r * E) by A5, FINSEQ_1: 4;

          

           A10: 1 <= (i + 1) & (i + 1) <= ( len q) by A5, NAT_1: 11;

          q = ((q | i) ^ <*(q /. (i + 1))*>) by A5, FINSEQ_5: 21;

          then q = (q0 ^ <*(q . (i + 1))*>) by A10, FINSEQ_4: 15;

          then (( Sum q) * E) = ((( Sum q0) + (q . (i + 1))) * E) by RVSUM_1: 74;

          then

           A11: (( Sum q) * E) = ((( Sum q0) * E) + ((q . (i + 1)) * E)) by RLVECT_1:def 6;

          

           A12: i = ( len S0) & i = ( len q0) by FINSEQ_1: 59, A5, NAT_1: 11;

          reconsider v = (S . (i + 1)) as Point of Y by A9;

          S0 = (S | ( dom S0)) by FINSEQ_1:def 3, A12;

          then ( Sum S) = (( Sum S0) + v) by A5, A12, RLVECT_1: 38;

          hence ( Sum S) = (( Sum q) * E) by A9, A4, A6, A12, A11;

        end;

        hence P[(i + 1)];

      end;

      for i be Nat holds P[i] from NAT_1:sch 2( A1, A3);

      hence thesis;

    end;

    theorem :: INTEGR20:8

    

     Th8: for A be non empty closed_interval Subset of REAL , D be Division of A, B be non empty closed_interval Subset of REAL , v be FinSequence of REAL st B c= A & ( len D) = ( len v) & for i be Nat st i in ( dom v) holds (v . i) = ( xvol (B /\ ( divset (D,i)))) holds ( Sum v) = ( vol B)

    proof

      defpred P[ Nat] means for A be non empty closed_interval Subset of REAL , D be Division of A, B be non empty closed_interval Subset of REAL , v be FinSequence of REAL st $1 = ( len D) & B c= A & ( len D) = ( len v) & for k be Nat st k in ( dom v) holds (v . k) = ( xvol (B /\ ( divset (D,k)))) holds ( Sum v) = ( vol B);

      

       A1: P[ 0 ];

      

       A2: for i be Nat st P[i] holds P[(i + 1)]

      proof

        let i be Nat;

        assume

         A3: P[i];

        let A be non empty closed_interval Subset of REAL , D be Division of A, B be non empty closed_interval Subset of REAL , v be FinSequence of REAL ;

        set D1 = (D | i), v1 = (v | i);

        assume

         A4: (i + 1) = ( len D) & B c= A & ( len D) = ( len v) & for k be Nat st k in ( dom v) holds (v . k) = ( xvol (B /\ ( divset (D,k))));

        

         A5: ( dom D) = ( Seg (i + 1)) & ( dom D) = ( dom v) by A4, FINSEQ_1:def 3, FINSEQ_3: 29;

        then

         A6: (v . (i + 1)) = ( xvol (B /\ ( divset (D,(i + 1))))) by A4, FINSEQ_1: 4;

        

         A7: 1 <= (i + 1) & (i + 1) <= ( len v) by A4, NAT_1: 11;

        v = ((v | i) ^ <*(v /. (i + 1))*>) by A4, FINSEQ_5: 21;

        then

         A8: v = (v1 ^ <*(v . (i + 1))*>) by A7, FINSEQ_4: 15;

        

         A9: ( lower_bound A) <= ( lower_bound B) & ( upper_bound B) <= ( upper_bound A) by A4, SEQ_4: 47, SEQ_4: 48;

        

         A10: ( rng D) c= A by INTEGRA1:def 2;

        

         A11: ( rng D1) c= ( rng D) by RELAT_1: 70;

        

         A12: ( Seg i) c= ( dom D) by A5, FINSEQ_1: 5, NAT_1: 11;

        

         A13: i = ( len D1) & i = ( len v1) by FINSEQ_1: 59, A4, NAT_1: 11;

        then

         A14: ( dom v1) = ( Seg i) by FINSEQ_1:def 3;

        per cases ;

          suppose

           A15: i <> 0 ;

          then

           A16: i in ( dom D) by A12, FINSEQ_1: 3;

          then

          consider A1,A2 be non empty closed_interval Subset of REAL such that

           A17: A1 = [.( lower_bound A), (D . i).] & A2 = [.(D . i), ( upper_bound A).] & A = (A1 \/ A2) by INTEGRA1: 32;

          for y be object st y in ( rng D1) holds y in A1

          proof

            let y be object;

            assume

             A18: y in ( rng D1);

            then y in A by A11, A10;

            then y in [.( lower_bound A), ( upper_bound A).] by INTEGRA1: 4;

            then

            consider y1 be Real such that

             A19: y = y1 & ( lower_bound A) <= y1 & y1 <= ( upper_bound A);

            consider x be object such that

             A20: x in ( dom D1) & y1 = (D1 . x) by A18, A19, FUNCT_1:def 3;

            reconsider x as Nat by A20;

            

             A21: x in ( Seg i) by A13, FINSEQ_1:def 3, A20;

            then

             A22: x <= i by FINSEQ_1: 1;

            now

              assume x <> i;

              then x < i by A22, XXREAL_0: 1;

              hence (D . x) <= (D . i) by A16, A12, A21, VALUED_0:def 13;

            end;

            then y1 <= (D . i) by A20, A21, FUNCT_1: 49;

            hence y in A1 by A19, A17;

          end;

          then

           A23: ( rng D1) c= A1;

          

           A24: (D1 . i) = (D . i) by A15, FINSEQ_1: 3, FUNCT_1: 49;

          for e1,e2 be ExtReal st e1 in ( dom D1) & e2 in ( dom D1) & e1 < e2 holds (D1 . e1) < (D1 . e2)

          proof

            let e1,e2 be ExtReal;

            assume

             A25: e1 in ( dom D1) & e2 in ( dom D1) & e1 < e2;

            then

             A26: e1 in ( Seg i) & e2 in ( Seg i) by A13, FINSEQ_1:def 3;

            then (D1 . e1) = (D . e1) & (D1 . e2) = (D . e2) by FUNCT_1: 49;

            hence thesis by A25, VALUED_0:def 13, A26, A12;

          end;

          then

          reconsider D1 as non empty increasing FinSequence of REAL by A15, VALUED_0:def 13;

          

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

          then (D1 . ( len D1)) = ( upper_bound A1) by A13, A24, A17, INTEGRA1: 5;

          then

          reconsider D1 as Division of A1 by A23, INTEGRA1:def 2;

          

           A28: 1 < (i + 1) by A15, NAT_1: 16;

          (i + 1) in ( dom D) by A5, FINSEQ_1: 4;

          then

           A29: ( lower_bound ( divset (D,(i + 1)))) = (D . ((i + 1) - 1)) & ( upper_bound ( divset (D,(i + 1)))) = (D . (i + 1)) by A28, INTEGRA1:def 4;

          then

           A30: B = [.( lower_bound B), ( upper_bound B).] & ( divset (D,(i + 1))) = [.(D . i), (D . (i + 1)).] by INTEGRA1: 4;

          

           A31: (D . i) <= (D . (i + 1)) by A29, SEQ_4: 11;

          per cases ;

            suppose

             A32: ( upper_bound B) <= (D . i);

            then [.( lower_bound B), ( upper_bound B).] c= [.( lower_bound A), (D . i).] by A9, XXREAL_1: 34;

            then

             A33: B c= A1 by A17, INTEGRA1: 4;

            for k be Nat st k in ( dom v1) holds (v1 . k) = ( xvol (B /\ ( divset (D1,k))))

            proof

              let k be Nat;

              assume

               A34: k in ( dom v1);

              then

               A35: k in ( Seg i) & k in ( dom v) by RELAT_1: 57;

              then

               A36: (v . k) = (v1 . k) by FUNCT_1: 49;

              

               A37: k in ( dom D) & k in ( dom D1) by A34, A35, A13, A4, FINSEQ_3: 29;

              

               A38: ( divset (D,k)) = [.( lower_bound ( divset (D,k))), ( upper_bound ( divset (D,k))).] & ( divset (D1,k)) = [.( lower_bound ( divset (D1,k))), ( upper_bound ( divset (D1,k))).] by INTEGRA1: 4;

              ( divset (D,k)) = ( divset (D1,k))

              proof

                per cases ;

                  suppose k = 1;

                  then

                   A39: ( lower_bound ( divset (D,k))) = ( lower_bound A) & ( upper_bound ( divset (D,k))) = (D . k) & ( lower_bound ( divset (D1,k))) = ( lower_bound A1) & ( upper_bound ( divset (D1,k))) = (D1 . k) by A37, INTEGRA1:def 4;

                  ( lower_bound A) = ( lower_bound A1) by A17, A27, INTEGRA1: 5;

                  hence ( divset (D,k)) = ( divset (D1,k)) by A39, A35, A38, FUNCT_1: 49;

                end;

                  suppose

                   A40: k <> 1;

                  then

                   A41: ( lower_bound ( divset (D,k))) = (D . (k - 1)) & ( upper_bound ( divset (D,k))) = (D . k) & ( lower_bound ( divset (D1,k))) = (D1 . (k - 1)) & ( upper_bound ( divset (D1,k))) = (D1 . k) by A37, INTEGRA1:def 4;

                  

                   A42: 1 <= k by A35, FINSEQ_1: 1;

                  then (k - 1) in NAT by INT_1: 5;

                  then

                  reconsider k1 = (k - 1) as Nat;

                  1 < k by A40, A42, XXREAL_0: 1;

                  then (D . k1) = (D1 . k1) by A35, FINSEQ_3: 12, FUNCT_1: 49;

                  hence ( divset (D,k)) = ( divset (D1,k)) by A41, A35, A38, FUNCT_1: 49;

                end;

              end;

              hence thesis by A4, A35, A36;

            end;

            then

             A43: ( Sum v1) = ( vol B) by A3, A33, A13;

            

             A44: [.(D . i), ( upper_bound B).] c= {(D . i)} by A32, XXREAL_1: 85;

            ( lower_bound B) <= ( upper_bound B) by SEQ_4: 11;

            then ( lower_bound B) <= (D . i) & ( upper_bound B) <= (D . (i + 1)) by A32, A31, XXREAL_0: 2;

            then

             A45: (B /\ ( divset (D,(i + 1)))) c= {(D . i)} by A44, A30, XXREAL_1: 143;

            reconsider BD = (B /\ ( divset (D,(i + 1)))) as real-bounded Subset of REAL by XBOOLE_1: 17, XXREAL_2: 45;

            

             A46: ( xvol (B /\ ( divset (D,(i + 1))))) <= ( xvol {(D . i)})

            proof

              per cases ;

                suppose (B /\ ( divset (D,(i + 1)))) = {} ;

                then ( xvol (B /\ ( divset (D,(i + 1))))) = 0 by Def2;

                hence ( xvol (B /\ ( divset (D,(i + 1))))) <= ( xvol {(D . i)}) by Th5;

              end;

                suppose (B /\ ( divset (D,(i + 1)))) <> {} ;

                then

                reconsider BD = (B /\ ( divset (D,(i + 1)))) as non empty real-bounded Subset of REAL by XBOOLE_1: 17, XXREAL_2: 45;

                reconsider Di = {(D . i)} as non empty real-bounded Subset of REAL ;

                

                 A47: ( xvol BD) = ( vol BD) & ( xvol {(D . i)}) = ( vol {(D . i)}) by Def2;

                ( lower_bound Di) <= ( lower_bound BD) & ( upper_bound BD) <= ( upper_bound Di) by A45, SEQ_4: 47, SEQ_4: 48;

                hence ( xvol (B /\ ( divset (D,(i + 1))))) <= ( xvol {(D . i)}) by A47, XREAL_1: 13;

              end;

            end;

            

             A48: ( vol {(D . i)}) = (( upper_bound {(D . i)}) - ( upper_bound {(D . i)})) by SEQ_4: 10;

             0 <= ( xvol BD) by Th5;

            then (v . (i + 1)) = 0 by A6, A46, A48, Def2;

            then ( Sum v) = (( vol B) + 0 ) by A43, A8, RVSUM_1: 74;

            hence ( Sum v) = ( vol B);

          end;

            suppose

             A49: (D . i) < ( upper_bound B);

            per cases ;

              suppose

               A50: ( lower_bound B) <= (D . i);

              then

              reconsider B1 = [.( lower_bound B), (D . i).], B2 = [.(D . i), ( upper_bound B).] as non empty closed_interval Subset of REAL by XXREAL_1: 30, A49, MEASURE5:def 3;

              (B1 \/ B2) = [.( lower_bound B), ( upper_bound B).] by A50, A49, XXREAL_1: 165;

              then

               A51: (B1 \/ B2) = B by INTEGRA1: 4;

              B1 = [.( lower_bound B1), ( upper_bound B1).] & B2 = [.( lower_bound B2), ( upper_bound B2).] by INTEGRA1: 4;

              then

               A52: ( lower_bound B) = ( lower_bound B1) & (D . i) = ( upper_bound B1) & (D . i) = ( lower_bound B2) & ( upper_bound B) = ( upper_bound B2) by INTEGRA1: 5;

              for k be Nat st k in ( dom v1) holds (v1 . k) = ( xvol (B1 /\ ( divset (D1,k))))

              proof

                let k be Nat;

                assume

                 A53: k in ( dom v1);

                then

                 A54: k in ( Seg i) & k in ( dom v) by RELAT_1: 57;

                then

                 A55: (v . k) = ( xvol (B /\ ( divset (D,k)))) by A4;

                

                 A56: (v . k) = (v1 . k) by A54, FUNCT_1: 49;

                

                 A57: k in ( dom D) & k in ( dom D1) by A53, A54, A4, A13, FINSEQ_3: 29;

                

                 A58: ( divset (D,k)) = [.( lower_bound ( divset (D,k))), ( upper_bound ( divset (D,k))).] & ( divset (D1,k)) = [.( lower_bound ( divset (D1,k))), ( upper_bound ( divset (D1,k))).] by INTEGRA1: 4;

                

                 A59: ( divset (D,k)) = ( divset (D1,k))

                proof

                  per cases ;

                    suppose k = 1;

                    then

                     A60: ( lower_bound ( divset (D,k))) = ( lower_bound A) & ( upper_bound ( divset (D,k))) = (D . k) & ( lower_bound ( divset (D1,k))) = ( lower_bound A1) & ( upper_bound ( divset (D1,k))) = (D1 . k) by A57, INTEGRA1:def 4;

                    ( lower_bound A) = ( lower_bound A1) by A27, A17, INTEGRA1: 5;

                    hence ( divset (D,k)) = ( divset (D1,k)) by A60, A54, A58, FUNCT_1: 49;

                  end;

                    suppose

                     A61: k <> 1;

                    then

                     A62: ( lower_bound ( divset (D,k))) = (D . (k - 1)) & ( upper_bound ( divset (D,k))) = (D . k) & ( lower_bound ( divset (D1,k))) = (D1 . (k - 1)) & ( upper_bound ( divset (D1,k))) = (D1 . k) by A57, INTEGRA1:def 4;

                    

                     A63: 1 <= k by A54, FINSEQ_1: 1;

                    then (k - 1) in NAT by INT_1: 5;

                    then

                    reconsider k1 = (k - 1) as Nat;

                    1 < k by A61, A63, XXREAL_0: 1;

                    then (D . k1) = (D1 . k1) by A54, FINSEQ_3: 12, FUNCT_1: 49;

                    hence ( divset (D,k)) = ( divset (D1,k)) by A62, A54, A58, FUNCT_1: 49;

                  end;

                end;

                then

                 A64: (B1 /\ ( divset (D1,k))) c= (B /\ ( divset (D,k))) by A51, XBOOLE_1: 7, XBOOLE_1: 26;

                for x be object st x in (B /\ ( divset (D,k))) holds x in (B1 /\ ( divset (D1,k)))

                proof

                  let x be object;

                  assume

                   A65: x in (B /\ ( divset (D,k)));

                  then

                  reconsider r = x as Real;

                  

                   A66: x in B & x in ( divset (D,k)) by A65, XBOOLE_0:def 4;

                  then

                   A67: ex r0 be Real st r = r0 & ( lower_bound B) <= r0 & r0 <= ( upper_bound B) by A30;

                  

                   A68: ex r1 be Real st r = r1 & ( lower_bound ( divset (D,k))) <= r1 & r1 <= ( upper_bound ( divset (D,k))) by A58, A66;

                  

                   A69: k <= i by A54, FINSEQ_1: 1;

                   A70:

                  now

                    assume k <> i;

                    then k < i by A69, XXREAL_0: 1;

                    hence (D . k) <= (D . i) by A16, A57, VALUED_0:def 13;

                  end;

                  k = 1 or k <> 1;

                  then ( upper_bound ( divset (D,k))) <= (D . i) by A70, A57, INTEGRA1:def 4;

                  then r <= (D . i) by A68, XXREAL_0: 2;

                  then r in B1 by A67;

                  hence x in (B1 /\ ( divset (D1,k))) by XBOOLE_0:def 4, A59, A66;

                end;

                then (B /\ ( divset (D,k))) c= (B1 /\ ( divset (D1,k)));

                hence thesis by A55, A56, A64, XBOOLE_0:def 10;

              end;

              then

               A71: ( Sum v1) = ( vol B1) by A3, A17, A9, XXREAL_1: 34, A13;

              (B /\ ( divset (D,(i + 1)))) = ((B1 /\ ( divset (D,(i + 1)))) \/ (B2 /\ ( divset (D,(i + 1))))) by A51, XBOOLE_1: 23;

              then (B /\ ( divset (D,(i + 1)))) = ( [.(D . i), (D . i).] \/ (B2 /\ [.(D . i), (D . (i + 1)).])) by A30, A50, A31, XXREAL_1: 143;

              then

               A72: (B /\ ( divset (D,(i + 1)))) = (( [.(D . i), (D . i).] \/ [.(D . i), ( upper_bound B).]) /\ ( [.(D . i), (D . i).] \/ [.(D . i), (D . (i + 1)).])) by XBOOLE_1: 24;

              (D . i) <= ( upper_bound B) by A52, SEQ_4: 11;

              then

               A73: ( [.(D . i), (D . i).] \/ [.(D . i), ( upper_bound B).]) = B2 by XXREAL_1: 165;

              ( [.(D . i), (D . i).] \/ [.(D . i), (D . (i + 1)).]) = [.(D . i), (D . (i + 1)).] by A31, XXREAL_1: 165;

              then

               A74: ( [.(D . i), (D . i).] \/ [.(D . i), (D . (i + 1)).]) = ( divset (D,(i + 1))) by A29, INTEGRA1: 4;

              

               A75: ( upper_bound B) <= (D . (i + 1)) by A4, A9, INTEGRA1:def 2;

              for x be object st x in B2 holds x in ( divset (D,(i + 1)))

              proof

                let x be object;

                assume

                 A76: x in B2;

                then

                reconsider r = x as Real;

                

                 A77: ex r0 be Real st r = r0 & (D . i) <= r0 & r0 <= ( upper_bound B) by A76;

                r <= (D . (i + 1)) by A75, XXREAL_0: 2, A77;

                hence x in ( divset (D,(i + 1))) by A30, A77;

              end;

              then

               A78: B2 c= ( divset (D,(i + 1)));

              (v . (i + 1)) = ( xvol (B /\ ( divset (D,(i + 1))))) by A4, A5, FINSEQ_1: 4;

              then (v . (i + 1)) = ( xvol B2) by A78, A74, A72, A73, XBOOLE_1: 28;

              then (v . (i + 1)) = ( vol B2) by Def2;

              then ( Sum v) = (( vol B1) + ( vol B2)) by A8, RVSUM_1: 74, A71;

              hence ( Sum v) = ( vol B) by A52;

            end;

              suppose

               A79: (D . i) < ( lower_bound B);

              then

               A80: [.( lower_bound B), (D . i).] = {} by XXREAL_1: 29;

              reconsider B1 = [.( lower_bound B), (D . i).] as Subset of REAL ;

              reconsider B2 = B as non empty closed_interval Subset of REAL ;

              now

                let k0 be object;

                assume

                 A81: k0 in ( dom v1);

                then

                 A82: k0 in ( Seg i) & k0 in ( dom v) by RELAT_1: 57;

                reconsider k = k0 as Nat by A81;

                

                 A83: k in ( dom D) & k in ( dom D1) by A81, A82, A4, A13, FINSEQ_3: 29;

                

                 A84: ( divset (D,k)) = [.( lower_bound ( divset (D,k))), ( upper_bound ( divset (D,k))).] & ( divset (D1,k)) = [.( lower_bound ( divset (D1,k))), ( upper_bound ( divset (D1,k))).] by INTEGRA1: 4;

                

                 A85: ( divset (D,k)) = ( divset (D1,k))

                proof

                  per cases ;

                    suppose k = 1;

                    then

                     A86: ( lower_bound ( divset (D,k))) = ( lower_bound A) & ( upper_bound ( divset (D,k))) = (D . k) & ( lower_bound ( divset (D1,k))) = ( lower_bound A1) & ( upper_bound ( divset (D1,k))) = (D1 . k) by A83, INTEGRA1:def 4;

                    ( lower_bound A) = ( lower_bound A1) by A27, A17, INTEGRA1: 5;

                    hence ( divset (D,k)) = ( divset (D1,k)) by A84, A86, A82, FUNCT_1: 49;

                  end;

                    suppose

                     A87: k <> 1;

                    then

                     A88: ( lower_bound ( divset (D,k))) = (D . (k - 1)) & ( upper_bound ( divset (D,k))) = (D . k) & ( lower_bound ( divset (D1,k))) = (D1 . (k - 1)) & ( upper_bound ( divset (D1,k))) = (D1 . k) by A83, INTEGRA1:def 4;

                    

                     A89: 1 <= k by A82, FINSEQ_1: 1;

                    then (k - 1) in NAT by INT_1: 5;

                    then

                    reconsider k1 = (k - 1) as Nat;

                    1 < k by A87, A89, XXREAL_0: 1;

                    then (D . k1) = (D1 . k1) by A82, FINSEQ_3: 12, FUNCT_1: 49;

                    hence ( divset (D,k)) = ( divset (D1,k)) by A88, A82, A84, FUNCT_1: 49;

                  end;

                end;

                for x be object st x in (B /\ ( divset (D,k))) holds x in (B1 /\ ( divset (D1,k)))

                proof

                  let x be object;

                  assume

                   A90: x in (B /\ ( divset (D,k)));

                  then

                  reconsider r = x as Real;

                  

                   A91: x in B & x in ( divset (D,k)) by A90, XBOOLE_0:def 4;

                  then

                   A92: (ex r0 be Real st r = r0 & ( lower_bound B) <= r0 & r0 <= ( upper_bound B)) & (ex r1 be Real st r = r1 & ( lower_bound ( divset (D,k))) <= r1 & r1 <= ( upper_bound ( divset (D,k)))) by A30, A84;

                  k in ( Seg i) by A81, RELAT_1: 57;

                  then

                   A93: k <= i by FINSEQ_1: 1;

                   A94:

                  now

                    assume k <> i;

                    then k < i by A93, XXREAL_0: 1;

                    hence (D . k) <= (D . i) by A16, A83, VALUED_0:def 13;

                  end;

                  k = 1 or k <> 1;

                  then ( upper_bound ( divset (D,k))) <= (D . i) by A94, A83, INTEGRA1:def 4;

                  then r <= (D . i) by A92, XXREAL_0: 2;

                  then r in B1 by A92;

                  hence x in (B1 /\ ( divset (D1,k))) by XBOOLE_0:def 4, A85, A91;

                end;

                then

                 A95: (B /\ ( divset (D,k))) c= (B1 /\ ( divset (D1,k)));

                (v . k) = ( xvol (B /\ ( divset (D,k)))) by A82, A4;

                then (v . k0) = 0 by Def2, A80, A95;

                hence (v1 . k0) = 0 by A82, FUNCT_1: 49;

              end;

              then v1 = (( dom v1) --> 0 ) by FUNCOP_1: 11;

              then v1 = (i |-> 0 ) by A14, FINSEQ_2:def 2;

              then

               A96: ( Sum v1) = 0 by RVSUM_1: 81;

              

               A97: ( upper_bound B) <= (D . (i + 1)) by A4, A9, INTEGRA1:def 2;

              for x be object st x in B2 holds x in ( divset (D,(i + 1)))

              proof

                let x be object;

                assume

                 A98: x in B2;

                then

                reconsider r = x as Real;

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

                then ex r0 be Real st r = r0 & ( lower_bound B) <= r0 & r0 <= ( upper_bound B) by A98;

                then (D . i) <= r & r <= (D . (i + 1)) by A97, XXREAL_0: 2, A79;

                hence x in ( divset (D,(i + 1))) by A30;

              end;

              then

               A99: B2 c= ( divset (D,(i + 1)));

              (v . (i + 1)) = ( xvol (B /\ ( divset (D,(i + 1))))) by A4, A5, FINSEQ_1: 4;

              then (v . (i + 1)) = ( xvol B) by A99, XBOOLE_1: 28;

              then (v . (i + 1)) = ( vol B) by Def2;

              then ( Sum v) = ( 0 + ( vol B)) by A8, RVSUM_1: 74, A96;

              hence ( Sum v) = ( vol B);

            end;

          end;

        end;

          suppose

           A100: i = 0 ;

          then

           A101: (D . 1) = ( upper_bound A) by A4, INTEGRA1:def 2;

          ( dom D) = ( Seg 1) by A100, A4, FINSEQ_1:def 3;

          then 1 in ( dom D);

          then ( lower_bound ( divset (D,1))) = ( lower_bound A) & ( upper_bound ( divset (D,1))) = (D . 1) by INTEGRA1:def 4;

          then ( divset (D,1)) = [.( lower_bound A), ( upper_bound A).] by A101, INTEGRA1: 4;

          then

           A102: ( divset (D,1)) = A by INTEGRA1: 4;

          (v . 1) = ( xvol (B /\ ( divset (D,1)))) by A100, A4, A5, FINSEQ_1: 4;

          then (v . 1) = ( xvol B) by A102, A4, XBOOLE_1: 28;

          then

           A103: (v . 1) = ( vol B) by Def2;

          ( Sum v) = (( Sum v1) + (v . 1)) by A100, A8, RVSUM_1: 74;

          then ( Sum v) = ( 0 + ( vol B)) by A100, RVSUM_1: 72, A103;

          hence ( Sum v) = ( vol B);

        end;

      end;

      for i be Nat holds P[i] from NAT_1:sch 2( A1, A2);

      hence thesis;

    end;

    

     Lm2: for Y be RealNormSpace, xseq,yseq be FinSequence of Y st ( len xseq) = (( len yseq) + 1) & (xseq | ( len yseq)) = yseq holds ex v be Point of Y st v = (xseq /. ( len xseq)) & ( Sum xseq) = (( Sum yseq) + v)

    proof

      let Y be RealNormSpace;

      let xseq,yseq be FinSequence of Y;

      assume

       A1: ( len xseq) = (( len yseq) + 1) & (xseq | ( len yseq)) = yseq;

      take v = (xseq /. ( len xseq));

      ( len xseq) in ( Seg ( len xseq)) by A1, FINSEQ_1: 4;

      then ( len xseq) in ( dom xseq) by FINSEQ_1:def 3;

      then

       A2: v = (xseq . ( len xseq)) by PARTFUN1:def 6;

      (xseq | ( len yseq)) = (xseq | ( dom yseq)) by FINSEQ_1:def 3;

      hence thesis by A1, A2, RLVECT_1: 38;

    end;

    theorem :: INTEGR20:9

    

     Th9: for Y be RealNormSpace, xseq be FinSequence of Y, yseq be FinSequence of REAL st ( len xseq) = ( len yseq) & (for i be Element of NAT st i in ( dom xseq) holds ex v be Point of Y st v = (xseq /. i) & (yseq . i) = ||.v.||) holds ||.( Sum xseq).|| <= ( Sum yseq)

    proof

      let Y be RealNormSpace;

      defpred P[ Nat] means for xseq be FinSequence of Y, yseq be FinSequence of REAL st $1 = ( len xseq) & ( len xseq) = ( len yseq) & (for i be Element of NAT st i in ( dom xseq) holds ex v be Point of Y st v = (xseq /. i) & (yseq . i) = ||.v.||) holds ||.( Sum xseq).|| <= ( Sum yseq);

      

       A1: P[ 0 ]

      proof

        let xseq be FinSequence of Y, yseq be FinSequence of REAL ;

        assume

         A2: 0 = ( len xseq) & ( len xseq) = ( len yseq) & (for i be Element of NAT st i in ( dom xseq) holds ex v be Point of Y st v = (xseq /. i) & (yseq . i) = ||.v.||);

        then ( <*> the carrier of Y) = xseq;

        then ( Sum xseq) = ( 0. Y) & ( <*> REAL ) = yseq by A2, RLVECT_1: 43;

        hence thesis by RVSUM_1: 72;

      end;

       A3:

      now

        let i be Nat;

        assume

         A4: P[i];

        now

          let xseq be FinSequence of Y, yseq be FinSequence of REAL ;

          set xseq0 = (xseq | i), yseq0 = (yseq | i);

          assume

           A5: (i + 1) = ( len xseq) & ( len xseq) = ( len yseq) & (for i be Element of NAT st i in ( dom xseq) holds ex v be Point of Y st v = (xseq /. i) & (yseq . i) = ||.v.||);

          

           A6: for k be Element of NAT st k in ( dom xseq0) holds ex v be Point of Y st v = (xseq0 /. k) & (yseq0 . k) = ||.v.||

          proof

            let k be Element of NAT ;

            assume

             A7: k in ( dom xseq0);

            then

             A8: k in ( Seg i) & k in ( dom xseq) by RELAT_1: 57;

            then

            consider v be Point of Y such that

             A9: v = (xseq /. k) & (yseq . k) = ||.v.|| by A5;

            take v;

            (xseq /. k) = (xseq . k) by A8, PARTFUN1:def 6;

            then (xseq /. k) = (xseq0 . k) by A8, FUNCT_1: 49;

            hence thesis by A9, A8, A7, PARTFUN1:def 6, FUNCT_1: 49;

          end;

          ( dom xseq) = ( Seg (i + 1)) by A5, FINSEQ_1:def 3;

          then

          consider w be Point of Y such that

           A10: w = (xseq /. (i + 1)) & (yseq . (i + 1)) = ||.w.|| by A5, FINSEQ_1: 4;

          

           A11: 1 <= (i + 1) & (i + 1) <= ( len yseq) by A5, NAT_1: 11;

          yseq = ((yseq | i) ^ <*(yseq /. (i + 1))*>) by A5, FINSEQ_5: 21;

          then yseq = (yseq0 ^ <*(yseq . (i + 1))*>) by A11, FINSEQ_4: 15;

          then

           A12: ( Sum yseq) = (( Sum yseq0) + (yseq . (i + 1))) by RVSUM_1: 74;

          

           A13: i = ( len xseq0) by A5, FINSEQ_1: 59, NAT_1: 11;

          then

           A14: ex v be Point of Y st v = (xseq /. ( len xseq)) & ( Sum xseq) = (( Sum xseq0) + v) by A5, Lm2;

          

           A15: ||.(( Sum xseq0) + w).|| <= ( ||.( Sum xseq0).|| + ||.w.||) by NORMSP_1:def 1;

          ( len xseq0) = ( len yseq0) by A5, A13, FINSEQ_1: 59, NAT_1: 11;

          then ( ||.( Sum xseq0).|| + ||.w.||) <= (( Sum yseq0) + (yseq . (i + 1))) by A10, XREAL_1: 6, A4, A6, A13;

          hence ||.( Sum xseq).|| <= ( Sum yseq) by A5, A10, A12, A14, A15, XXREAL_0: 2;

        end;

        hence P[(i + 1)];

      end;

      for i be Nat holds P[i] from NAT_1:sch 2( A1, A3);

      hence thesis;

    end;

    theorem :: INTEGR20:10

    

     Th10: for Y be RealNormSpace, p be FinSequence of Y, q be FinSequence of REAL st ( len p) = ( len q) & (for j be Nat st j in ( dom p) holds ||.(p /. j).|| <= (q . j)) holds ||.( Sum p).|| <= ( Sum q)

    proof

      let Y be RealNormSpace;

      let p be FinSequence of Y, 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));

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

      

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

        reconsider w = ||.(p /. i).|| as Element of REAL ;

        take w;

        thus thesis;

      end;

      consider u be FinSequence of REAL such that

       A3: ( 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( A2);

      

       A4: for i be Element of NAT st i in ( dom p) holds ex v be Point of Y st v = (p /. i) & (u . i) = ||.v.||

      proof

        let i be Element of NAT ;

        assume i in ( dom p);

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

        hence ex v be Point of Y st v = (p /. i) & (u . i) = ||.v.|| by A3;

      end;

      

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

      then

       A6: ||.( Sum p).|| <= ( Sum u) by A4, Th9;

      set i = ( len p);

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

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

      now

        let j be Nat;

        assume j in ( Seg i);

        then

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

        then ex v be Point of Y st v = (p /. j) & (u . j) = ||.v.|| by A4;

        hence (uu . j) <= (qq . j) by A7, A1;

      end;

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

      hence thesis by A6, XXREAL_0: 2;

    end;

    theorem :: INTEGR20:11

    

     Th11: for j be Element of NAT holds for A be non empty closed_interval Subset of REAL holds for D1 be Division of A st j in ( dom D1) holds ( vol ( divset (D1,j))) <= ( delta D1)

    proof

      let j be Element of NAT ;

      let A be non empty closed_interval Subset of REAL ;

      let D1 be Division of A;

      assume

       A1: j in ( dom D1);

      then j in ( Seg ( len D1)) by FINSEQ_1:def 3;

      then j in ( Seg ( len ( upper_volume (( chi (A,A)),D1)))) by INTEGRA1:def 6;

      then j in ( dom ( upper_volume (( chi (A,A)),D1))) by FINSEQ_1:def 3;

      then (( upper_volume (( chi (A,A)),D1)) . j) in ( rng ( upper_volume (( chi (A,A)),D1))) by FUNCT_1:def 3;

      then (( upper_volume (( chi (A,A)),D1)) . j) <= ( max ( rng ( upper_volume (( chi (A,A)),D1)))) by XXREAL_2:def 8;

      hence ( vol ( divset (D1,j))) <= ( delta D1) by A1, INTEGRA1: 20;

    end;

    theorem :: INTEGR20:12

    

     Th12: for A be non empty closed_interval Subset of REAL , D be Division of A, r be Real st ( delta D) < r holds for i be Nat, s,t be Real st i in ( dom D) & s in ( divset (D,i)) & t in ( divset (D,i)) holds |.(s - t).| < r

    proof

      let A be non empty closed_interval Subset of REAL , D be Division of A, r be Real;

      assume

       A1: ( delta D) < r;

      let i be Nat, s,t be Real;

      assume

       A2: i in ( dom D) & s in ( divset (D,i)) & t in ( divset (D,i));

      then ( vol ( divset (D,i))) <= ( delta D) by Th11;

      then

       A3: (( upper_bound ( divset (D,i))) - ( lower_bound ( divset (D,i)))) < r by A1, XXREAL_0: 2;

      s <= ( upper_bound ( divset (D,i))) & t <= ( upper_bound ( divset (D,i))) & ( lower_bound ( divset (D,i))) <= s & ( lower_bound ( divset (D,i))) <= t by A2, SEQ_4:def 1, SEQ_4:def 2;

      then

       A4: (t - s) <= (( upper_bound ( divset (D,i))) - ( lower_bound ( divset (D,i)))) & (s - t) <= (( upper_bound ( divset (D,i))) - ( lower_bound ( divset (D,i)))) by XREAL_1: 13;

      per cases ;

        suppose s < t;

        then (s - t) < (t - t) by XREAL_1: 14;

        then |.(s - t).| = ( - (s - t)) by ABSVALUE:def 1;

        hence |.(s - t).| < r by A3, A4, XXREAL_0: 2;

      end;

        suppose not s < t;

        then (t - t) <= (s - t) by XREAL_1: 9;

        then |.(s - t).| = (s - t) by ABSVALUE:def 1;

        hence |.(s - t).| < r by A3, A4, XXREAL_0: 2;

      end;

    end;

    theorem :: INTEGR20:13

    

     Th13: for X be RealBanachSpace, A be non empty closed_interval Subset of REAL , h be Function of A, the carrier of X st for r be Real st 0 < r holds ex s be Real st 0 < s & for x1,x2 be Real st x1 in ( dom h) & x2 in ( dom h) & |.(x1 - x2).| < s holds ||.((h /. x1) - (h /. x2)).|| < r holds for T be DivSequence of A, S be middle_volume_Sequence of h, T st ( delta T) is convergent & ( lim ( delta T)) = 0 holds ( middle_sum (h,S)) is convergent

    proof

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

      assume

       A1: for r be Real st 0 < r holds ex s be Real st 0 < s & for x1,x2 be Real st x1 in ( dom h) & x2 in ( dom h) & |.(x1 - x2).| < s holds ||.((h /. x1) - (h /. x2)).|| < r;

      thus for T be DivSequence of A, S be middle_volume_Sequence of h, T st ( delta T) is convergent & ( lim ( delta T)) = 0 holds ( middle_sum (h,S)) is convergent

      proof

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

        assume

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

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

        

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

        proof

          let k be Element of NAT ;

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

          

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

          

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

          proof

            let i be Nat;

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

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

            then

            consider c be Point of X such that

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

            consider x be object such that

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

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

            then

            reconsider x as Element of REAL ;

            take x;

            thus thesis by A6, A7;

          end;

          consider p be FinSequence of REAL such that

           A8: ( 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( A5);

          take p;

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

          hence thesis by A8, A4, FINSEQ_1:def 11;

        end;

        consider Fn be sequence of ( REAL * ) such that

         A9: for x be Element of NAT holds P[x, (Fn . x)] from FUNCT_2:sch 3( A3);

        consider Fm be sequence of ( REAL * ) such that

         A10: for x be Element of NAT holds P[x, (Fm . x)] from FUNCT_2:sch 3( A3);

        

         A11: 0 <= ( vol A) by INTEGRA1: 9;

        now

          let p be Real;

          set pp2 = (p / 2);

          set pv = (pp2 / (( vol A) + 1));

          assume p > 0 ;

          then

           A12: 0 < pp2 & pp2 < p by XREAL_1: 215, XREAL_1: 216;

          then

           A13: 0 < pv by A11, XREAL_1: 139;

          then (pv * ( vol A)) < (pv * (( vol A) + 1)) by XREAL_1: 29, XREAL_1: 68;

          then (pv * ( vol A)) < pp2 by A11, XCMPLX_1: 87;

          then

           A14: (pv * ( vol A)) < p by A12, XXREAL_0: 2;

          set p2v = (pv / 2);

          consider sk be Real such that

           A15: 0 < sk & for x1,x2 be Real st x1 in ( dom h) & x2 in ( dom h) & |.(x1 - x2).| < sk holds ||.((h /. x1) - (h /. x2)).|| < p2v by A1, A13, XREAL_1: 215;

          consider k be Nat such that

           A16: for i be Nat st k <= i holds |.((( delta T) . i) - 0 ).| < sk by A15, A2, SEQ_2:def 7;

          take k;

          let n,m be Nat;

          

           A17: n in NAT & m in NAT by ORDINAL1:def 12;

          assume n >= k & m >= k;

          then |.((( delta T) . n) - 0 ).| < sk & |.((( delta T) . m) - 0 ).| < sk by A16;

          then |.( delta (T . n)).| < sk & |.( delta (T . m)).| < sk by INTEGRA3:def 2, A17;

          then

           A18: ( delta (T . n)) < sk & ( delta (T . m)) < sk by INTEGRA3: 9, ABSVALUE:def 1;

          

           A19: (( middle_sum (h,S)) . n) = ( middle_sum (h,(S . n))) & (( middle_sum (h,S)) . m) = ( middle_sum (h,(S . m))) by INTEGR18:def 4;

          consider p1 be FinSequence of REAL such that

           A20: p1 = (Fn . n) & ( len p1) = ( len (T . n)) & for i be Nat st i in ( dom (T . n)) holds (p1 . i) in ( dom (h | ( divset ((T . n),i)))) & ex z be Point of X st z = ((h | ( divset ((T . n),i))) . (p1 . i)) & ((S . n) . i) = (( vol ( divset ((T . n),i))) * z) by A9, A17;

          consider p2 be FinSequence of REAL such that

           A21: p2 = (Fm . m) & ( len p2) = ( len (T . m)) & for i be Nat st i in ( dom (T . m)) holds (p2 . i) in ( dom (h | ( divset ((T . m),i)))) & ex z be Point of X st z = ((h | ( divset ((T . m),i))) . (p2 . i)) & ((S . m) . i) = (( vol ( divset ((T . m),i))) * z) by A10, A17;

          defpred H1[ object, object, object] means ex i,j be Nat, z be Point of X st $1 = i & $2 = j & z = ((h | ( divset ((T . n),i))) . (p1 . i)) & $3 = (( xvol (( divset ((T . n),i)) /\ ( divset ((T . m),j)))) * z);

          

           A22: for x,y be object st x in ( Seg ( len (T . n))) & y in ( Seg ( len (T . m))) holds ex w be object st w in the carrier of X & H1[x, y, w]

          proof

            let x,y be object;

            assume

             A23: x in ( Seg ( len (T . n))) & y in ( Seg ( len (T . m)));

            then

            reconsider i = x, j = y as Nat;

            i in ( dom (T . n)) by FINSEQ_1:def 3, A23;

            then

            consider z be Point of X such that

             A24: z = ((h | ( divset ((T . n),i))) . (p1 . i)) & ((S . n) . i) = (( vol ( divset ((T . n),i))) * z) by A20;

            (( xvol (( divset ((T . n),i)) /\ ( divset ((T . m),j)))) * z) in the carrier of X;

            hence thesis by A24;

          end;

          consider Snm be Function of [:( Seg ( len (T . n))), ( Seg ( len (T . m))):], the carrier of X such that

           A25: for x,y be object st x in ( Seg ( len (T . n))) & y in ( Seg ( len (T . m))) holds H1[x, y, (Snm . (x,y))] from BINOP_1:sch 1( A22);

          

           A26: for i,j be Nat st i in ( Seg ( len (T . n))) & j in ( Seg ( len (T . m))) holds ex z be Point of X st z = ((h | ( divset ((T . n),i))) . (p1 . i)) & (Snm . (i,j)) = (( xvol (( divset ((T . n),i)) /\ ( divset ((T . m),j)))) * z)

          proof

            let i,j be Nat;

            assume i in ( Seg ( len (T . n))) & j in ( Seg ( len (T . m)));

            then ex i1,j1 be Nat, z be Point of X st i = i1 & j = j1 & z = ((h | ( divset ((T . n),i1))) . (p1 . i1)) & (Snm . (i,j)) = (( xvol (( divset ((T . n),i1)) /\ ( divset ((T . m),j1)))) * z) by A25;

            hence thesis;

          end;

          defpred P1[ Nat, object] means ex r be FinSequence of X st ( dom r) = ( Seg ( len (T . m))) & $2 = ( Sum r) & for j be Nat st j in ( dom r) holds (r . j) = (Snm . ($1,j));

          

           A27: for k be Nat st k in ( Seg ( len (T . n))) holds ex x be object st P1[k, x]

          proof

            let k be Nat;

            assume

             A28: k in ( Seg ( len (T . n)));

            deffunc G( set) = (Snm . (k,$1));

            consider r be FinSequence such that

             A29: ( len r) = ( len (T . m)) and

             A30: for j be Nat st j in ( dom r) holds (r . j) = G(j) from FINSEQ_1:sch 2;

            

             A31: ( dom r) = ( Seg ( len (T . m))) by A29, FINSEQ_1:def 3;

            for j be Nat st j in ( dom r) holds (r . j) in the carrier of X

            proof

              let j be Nat;

              assume

               A32: j in ( dom r);

              then [k, j] in [:( Seg ( len (T . n))), ( Seg ( len (T . m))):] by A31, A28, ZFMISC_1: 87;

              then (Snm . (k,j)) in the carrier of X by FUNCT_2: 5;

              hence thesis by A30, A32;

            end;

            then

            reconsider r as FinSequence of X by FINSEQ_2: 12;

            take x = ( Sum r);

            thus thesis by A30, A31;

          end;

          consider Xp be FinSequence such that

           A33: ( dom Xp) = ( Seg ( len (T . n))) & for k be Nat st k in ( Seg ( len (T . n))) holds P1[k, (Xp . k)] from FINSEQ_1:sch 1( A27);

          for i be Nat st i in ( dom Xp) holds (Xp . i) in the carrier of X

          proof

            let i be Nat;

            assume i in ( dom Xp);

            then ex r be FinSequence of X st ( dom r) = ( Seg ( len (T . m))) & (Xp . i) = ( Sum r) & for j be Nat st j in ( dom r) holds (r . j) = (Snm . (i,j)) by A33;

            hence thesis;

          end;

          then

          reconsider Xp as FinSequence of X by FINSEQ_2: 12;

          

           A34: ( len Xp) = ( len (T . n)) by FINSEQ_1:def 3, A33;

          for k be Nat st 1 <= k & k <= ( len Xp) holds (Xp . k) = ((S . n) . k)

          proof

            let k be Nat;

            assume 1 <= k & k <= ( len Xp);

            then

             A35: k in ( Seg ( len Xp)) & k in ( Seg ( len (T . n))) by A34;

            then

             A36: k in ( dom Xp) & k in ( dom (T . n)) by FINSEQ_1:def 3;

            then

            consider z be Point of X such that

             A37: z = ((h | ( divset ((T . n),k))) . (p1 . k)) & ((S . n) . k) = (( vol ( divset ((T . n),k))) * z) by A20;

            consider r be FinSequence of X such that

             A38: ( dom r) = ( Seg ( len (T . m))) & (Xp . k) = ( Sum r) & for j be Nat st j in ( dom r) holds (r . j) = (Snm . (k,j)) by A35, A33;

            defpred P11[ Nat, set] means $2 = ( xvol (( divset ((T . n),k)) /\ ( divset ((T . m),$1))));

            

             A39: for i be Nat st i in ( Seg ( len r)) holds ex x be Element of REAL st P11[i, x]

            proof

              let i be Nat;

              assume i in ( Seg ( len r));

              ( xvol (( divset ((T . n),k)) /\ ( divset ((T . m),i)))) in REAL by XREAL_0:def 1;

              hence thesis;

            end;

            consider vtntm be FinSequence of REAL such that

             A40: ( dom vtntm) = ( Seg ( len r)) & for i be Nat st i in ( Seg ( len r)) holds P11[i, (vtntm . i)] from FINSEQ_1:sch 5( A39);

            

             A41: ( dom vtntm) = ( dom r) & for j be Nat st j in ( dom vtntm) holds (vtntm . j) = ( xvol (( divset ((T . n),k)) /\ ( divset ((T . m),j)))) by A40, FINSEQ_1:def 3;

            

             A42: ( len vtntm) = ( len r) & ( len (T . m)) = ( len r) by A38, A40, FINSEQ_1:def 3;

            then

             A43: ( Sum vtntm) = ( vol ( divset ((T . n),k))) by Th8, A40, A36, INTEGRA1: 8;

            for j be Nat st j in ( dom r) holds ex x be Real st x = (vtntm . j) & (r . j) = (x * z)

            proof

              let j be Nat;

              assume

               A44: j in ( dom r);

              then

               A45: ex w be Point of X st w = ((h | ( divset ((T . n),k))) . (p1 . k)) & (Snm . (k,j)) = (( xvol (( divset ((T . n),k)) /\ ( divset ((T . m),j)))) * w) by A26, A35, A38;

              take (vtntm . j);

              (r . j) = (( xvol (( divset ((T . n),k)) /\ ( divset ((T . m),j)))) * z) by A37, A45, A44, A38;

              hence thesis by A41, A44;

            end;

            hence thesis by A37, A38, A43, Th7, A42;

          end;

          then

           A46: Xp = (S . n) by INTEGR18:def 1, A34;

          defpred P2[ Nat, object] means ex s be FinSequence of X st ( dom s) = ( Seg ( len (T . n))) & $2 = ( Sum s) & for i be Nat st i in ( dom s) holds (s . i) = (Snm . (i,$1));

          

           A47: for k be Nat st k in ( Seg ( len (T . m))) holds ex x be object st P2[k, x]

          proof

            let k be Nat;

            assume

             A48: k in ( Seg ( len (T . m)));

            deffunc G( set) = (Snm . ($1,k));

            consider s be FinSequence such that

             A49: ( len s) = ( len (T . n)) and

             A50: for i be Nat st i in ( dom s) holds (s . i) = G(i) from FINSEQ_1:sch 2;

            

             A51: ( dom s) = ( Seg ( len (T . n))) by A49, FINSEQ_1:def 3;

            for i be Nat st i in ( dom s) holds (s . i) in the carrier of X

            proof

              let i be Nat;

              assume

               A52: i in ( dom s);

              then [i, k] in [:( Seg ( len (T . n))), ( Seg ( len (T . m))):] by A51, A48, ZFMISC_1: 87;

              then (Snm . (i,k)) in the carrier of X by FUNCT_2: 5;

              hence thesis by A50, A52;

            end;

            then

            reconsider s as FinSequence of X by FINSEQ_2: 12;

            take x = ( Sum s);

            thus thesis by A50, A51;

          end;

          consider Xq be FinSequence such that

           A53: ( dom Xq) = ( Seg ( len (T . m))) & for k be Nat st k in ( Seg ( len (T . m))) holds P2[k, (Xq . k)] from FINSEQ_1:sch 1( A47);

          for j be Nat st j in ( dom Xq) holds (Xq . j) in the carrier of X

          proof

            let j be Nat;

            assume j in ( dom Xq);

            then ex s be FinSequence of X st ( dom s) = ( Seg ( len (T . n))) & (Xq . j) = ( Sum s) & for i be Nat st i in ( dom s) holds (s . i) = (Snm . (i,j)) by A53;

            hence thesis;

          end;

          then

          reconsider Xq as FinSequence of X by FINSEQ_2: 12;

          defpred H2[ object, object, object] means ex i,j be Nat, z be Point of X st $1 = i & $2 = j & z = ((h | ( divset ((T . m),j))) . (p2 . j)) & $3 = (( xvol (( divset ((T . n),i)) /\ ( divset ((T . m),j)))) * z);

          

           A54: for x,y be object st x in ( Seg ( len (T . n))) & y in ( Seg ( len (T . m))) holds ex w be object st w in the carrier of X & H2[x, y, w]

          proof

            let x,y be object;

            assume

             A55: x in ( Seg ( len (T . n))) & y in ( Seg ( len (T . m)));

            then

            reconsider i = x, j = y as Nat;

            j in ( dom (T . m)) by FINSEQ_1:def 3, A55;

            then

            consider z be Point of X such that

             A56: z = ((h | ( divset ((T . m),j))) . (p2 . j)) & ((S . m) . j) = (( vol ( divset ((T . m),j))) * z) by A21;

            (( xvol (( divset ((T . n),i)) /\ ( divset ((T . m),j)))) * z) in the carrier of X;

            hence thesis by A56;

          end;

          consider Smn be Function of [:( Seg ( len (T . n))), ( Seg ( len (T . m))):], the carrier of X such that

           A57: for x,y be object st x in ( Seg ( len (T . n))) & y in ( Seg ( len (T . m))) holds H2[x, y, (Smn . (x,y))] from BINOP_1:sch 1( A54);

          

           A58: for i,j be Nat st i in ( Seg ( len (T . n))) & j in ( Seg ( len (T . m))) holds ex z be Point of X st z = ((h | ( divset ((T . m),j))) . (p2 . j)) & (Smn . (i,j)) = (( xvol (( divset ((T . n),i)) /\ ( divset ((T . m),j)))) * z)

          proof

            let i,j be Nat;

            assume i in ( Seg ( len (T . n))) & j in ( Seg ( len (T . m)));

            then ex i1,j1 be Nat, z be Point of X st i = i1 & j = j1 & z = ((h | ( divset ((T . m),j1))) . (p2 . j1)) & (Smn . (i,j)) = (( xvol (( divset ((T . n),i1)) /\ ( divset ((T . m),j1)))) * z) by A57;

            hence thesis;

          end;

          defpred P3[ Nat, object] means ex s be FinSequence of X st ( dom s) = ( Seg ( len (T . n))) & $2 = ( Sum s) & for i be Nat st i in ( dom s) holds (s . i) = (Smn . (i,$1));

          

           A59: for k be Nat st k in ( Seg ( len (T . m))) holds ex x be object st P3[k, x]

          proof

            let k be Nat;

            assume

             A60: k in ( Seg ( len (T . m)));

            deffunc G( set) = (Smn . ($1,k));

            consider s be FinSequence such that

             A61: ( len s) = ( len (T . n)) and

             A62: for i be Nat st i in ( dom s) holds (s . i) = G(i) from FINSEQ_1:sch 2;

            

             A63: ( dom s) = ( Seg ( len (T . n))) by A61, FINSEQ_1:def 3;

            for i be Nat st i in ( dom s) holds (s . i) in the carrier of X

            proof

              let i be Nat;

              assume

               A64: i in ( dom s);

              then [i, k] in [:( Seg ( len (T . n))), ( Seg ( len (T . m))):] by A63, A60, ZFMISC_1: 87;

              then (Smn . (i,k)) in the carrier of X by FUNCT_2: 5;

              hence thesis by A62, A64;

            end;

            then

            reconsider s as FinSequence of X by FINSEQ_2: 12;

            take x = ( Sum s);

            thus thesis by A62, A63;

          end;

          consider Zq be FinSequence such that

           A65: ( dom Zq) = ( Seg ( len (T . m))) & for k be Nat st k in ( Seg ( len (T . m))) holds P3[k, (Zq . k)] from FINSEQ_1:sch 1( A59);

          for j be Nat st j in ( dom Zq) holds (Zq . j) in the carrier of X

          proof

            let j be Nat;

            assume j in ( dom Zq);

            then ex s be FinSequence of X st ( dom s) = ( Seg ( len (T . n))) & (Zq . j) = ( Sum s) & for i be Nat st i in ( dom s) holds (s . i) = (Smn . (i,j)) by A65;

            hence thesis;

          end;

          then

          reconsider Zq as FinSequence of X by FINSEQ_2: 12;

          

           A66: ( len Zq) = ( len (T . m)) by FINSEQ_1:def 3, A65;

          for k be Nat st 1 <= k & k <= ( len Zq) holds (Zq . k) = ((S . m) . k)

          proof

            let k be Nat;

            assume

             A67: 1 <= k & k <= ( len Zq);

            then

            consider s be FinSequence of X such that

             A68: ( dom s) = ( Seg ( len (T . n))) & (Zq . k) = ( Sum s) & for i be Nat st i in ( dom s) holds (s . i) = (Smn . (i,k)) by A65, FINSEQ_3: 25;

            

             A69: k in ( Seg ( len (T . m))) by A67, A66;

            

             A70: k in ( dom (T . m)) by A67, A66, FINSEQ_3: 25;

            then

            consider z be Point of X such that

             A71: z = ((h | ( divset ((T . m),k))) . (p2 . k)) & ((S . m) . k) = (( vol ( divset ((T . m),k))) * z) by A21;

            defpred P11[ Nat, set] means $2 = ( xvol (( divset ((T . n),$1)) /\ ( divset ((T . m),k))));

            

             A72: for i be Nat st i in ( Seg ( len s)) holds ex x be Element of REAL st P11[i, x]

            proof

              let i be Nat;

              assume i in ( Seg ( len s));

              ( xvol (( divset ((T . n),i)) /\ ( divset ((T . m),k)))) in REAL by XREAL_0:def 1;

              hence thesis;

            end;

            consider vtntm be FinSequence of REAL such that

             A73: ( dom vtntm) = ( Seg ( len s)) & for i be Nat st i in ( Seg ( len s)) holds P11[i, (vtntm . i)] from FINSEQ_1:sch 5( A72);

            

             A74: ( dom vtntm) = ( dom s) & ( len vtntm) = ( len s) by A73, FINSEQ_1:def 3;

            

             A75: for j be Nat st j in ( dom vtntm) holds (vtntm . j) = ( xvol (( divset ((T . m),k)) /\ ( divset ((T . n),j)))) by A73;

            ( len s) = ( len (T . n)) by A68, FINSEQ_1:def 3;

            then

             A76: ( Sum vtntm) = ( vol ( divset ((T . m),k))) by Th8, A75, A74, A70, INTEGRA1: 8;

            for j be Nat st j in ( dom s) holds ex x be Real st x = (vtntm . j) & (s . j) = (x * z)

            proof

              let j be Nat;

              assume

               A77: j in ( dom s);

              then

               A78: ex w be Point of X st w = ((h | ( divset ((T . m),k))) . (p2 . k)) & (Smn . (j,k)) = (( xvol (( divset ((T . n),j)) /\ ( divset ((T . m),k)))) * w) by A58, A69, A68;

              take (vtntm . j);

              (s . j) = (( xvol (( divset ((T . n),j)) /\ ( divset ((T . m),k)))) * z) by A71, A78, A77, A68;

              hence thesis by A77, A73, A74;

            end;

            hence thesis by A71, A68, A76, Th7, A74;

          end;

          then Zq = (S . m) by INTEGR18:def 1, A66;

          then

           A79: (( Sum (S . n)) - ( Sum (S . m))) = (( Sum Xq) - ( Sum Zq)) by Th4, A33, A53, A46;

          set XZq = (Xq - Zq);

          

           A80: ( dom XZq) = (( dom Xq) /\ ( dom Zq)) by VFUNCT_1:def 2;

          then

          reconsider XZq = (Xq - Zq) as FinSequence by A53, A65, FINSEQ_1:def 2;

          now

            let i be Nat;

            assume i in ( dom XZq);

            then (XZq . i) = ((Xq - Zq) /. i) by PARTFUN1:def 6;

            hence (XZq . i) in the carrier of X;

          end;

          then

          reconsider XZq = (Xq - Zq) as FinSequence of X by FINSEQ_2: 12;

          ( len Xq) = ( len Zq) by FINSEQ_3: 29, A53, A65;

          then

           A81: (( Sum (S . n)) - ( Sum (S . m))) = ( Sum XZq) by A79, INTEGR18: 2;

          

           A82: for i,j be Nat, Snmij,Smnij be Point of X st i in ( Seg ( len (T . n))) & j in ( Seg ( len (T . m))) & Snmij = (Snm . (i,j)) & Smnij = (Smn . (i,j)) holds ||.(Snmij - Smnij).|| <= (( xvol (( divset ((T . n),i)) /\ ( divset ((T . m),j)))) * pv)

          proof

            let i,j be Nat, Snmij,Smnij be Point of X;

            assume

             A83: i in ( Seg ( len (T . n))) & j in ( Seg ( len (T . m))) & Snmij = (Snm . (i,j)) & Smnij = (Smn . (i,j));

            then

            consider z1 be Point of X such that

             A84: z1 = ((h | ( divset ((T . n),i))) . (p1 . i)) & (Snm . (i,j)) = (( xvol (( divset ((T . n),i)) /\ ( divset ((T . m),j)))) * z1) by A26;

            consider z2 be Point of X such that

             A85: z2 = ((h | ( divset ((T . m),j))) . (p2 . j)) & (Smn . (i,j)) = (( xvol (( divset ((T . n),i)) /\ ( divset ((T . m),j)))) * z2) by A58, A83;

            

             A86: i in ( dom (T . n)) & j in ( dom (T . m)) by A83, FINSEQ_1:def 3;

            then

             A87: (p1 . i) in ( dom (h | ( divset ((T . n),i)))) & (p2 . j) in ( dom (h | ( divset ((T . m),j)))) by A20, A21;

            then (p1 . i) in (( dom h) /\ ( divset ((T . n),i))) & (p2 . j) in (( dom h) /\ ( divset ((T . m),j))) by RELAT_1: 61;

            then

             A88: (p1 . i) in ( dom h) & (p1 . i) in ( divset ((T . n),i)) & (p2 . j) in ( dom h) & (p2 . j) in ( divset ((T . m),j)) by XBOOLE_0:def 4;

            z1 = (h . (p1 . i)) & z2 = (h . (p2 . j)) by A84, A85, A87, FUNCT_1: 47;

            then

             A89: z1 = (h /. (p1 . i)) & z2 = (h /. (p2 . j)) by A88, PARTFUN1:def 6;

            per cases ;

              suppose

               A90: (( divset ((T . n),i)) /\ ( divset ((T . m),j))) = {} ;

              then

               A91: ( xvol (( divset ((T . n),i)) /\ ( divset ((T . m),j)))) = 0 qua Real by Def2;

              Snmij = ( 0. X) & Smnij = ( 0. X) by A83, A84, A85, A90, Def2, RLVECT_1: 10;

              hence ||.(Snmij - Smnij).|| <= (( xvol (( divset ((T . n),i)) /\ ( divset ((T . m),j)))) * pv) by A91;

            end;

              suppose (( divset ((T . n),i)) /\ ( divset ((T . m),j))) <> {} ;

              then

              consider t be object such that

               A92: t in (( divset ((T . n),i)) /\ ( divset ((T . m),j))) by XBOOLE_0:def 1;

              reconsider t as Real by A92;

              

               A93: ( dom h) = A by FUNCT_2:def 1;

              

               A94: ( divset ((T . m),j)) c= A by A86, INTEGRA1: 8;

              

               A95: t in ( divset ((T . n),i)) & t in ( divset ((T . m),j)) by A92, XBOOLE_0:def 4;

              then |.((p1 . i) - t).| < sk & |.(t - (p2 . j)).| < sk by A86, A88, Th12, A18;

              then

               A96: ||.((h /. (p1 . i)) - (h /. t)).|| < p2v & ||.((h /. t) - (h /. (p2 . j))).|| < p2v by A94, A95, A93, A88, A15;

              reconsider DMN = (( divset ((T . n),i)) /\ ( divset ((T . m),j))) as real-bounded Subset of REAL by XBOOLE_1: 17, XXREAL_2: 45;

              (Snmij - Smnij) = (( xvol DMN) * (((h /. (p1 . i)) - ( 0. X)) - (h /. (p2 . j)))) by A83, A84, A89, A85, RLVECT_1: 34;

              then (Snmij - Smnij) = (( xvol DMN) * (((h /. (p1 . i)) - ((h /. t) - (h /. t))) - (h /. (p2 . j)))) by RLVECT_1: 15;

              then (Snmij - Smnij) = (( xvol DMN) * ((((h /. (p1 . i)) - (h /. t)) + (h /. t)) - (h /. (p2 . j)))) by RLVECT_1: 29;

              then (Snmij - Smnij) = (( xvol DMN) * (((h /. (p1 . i)) - (h /. t)) + ((h /. t) - (h /. (p2 . j))))) by RLVECT_1: 28;

              then (Snmij - Smnij) = ((( xvol DMN) * ((h /. (p1 . i)) - (h /. t))) + (( xvol DMN) * ((h /. t) - (h /. (p2 . j))))) by RLVECT_1:def 5;

              then

               A97: ||.(Snmij - Smnij).|| <= ( ||.(( xvol DMN) * ((h /. (p1 . i)) - (h /. t))).|| + ||.(( xvol DMN) * ((h /. t) - (h /. (p2 . j)))).||) by NORMSP_1:def 1;

               ||.(( xvol DMN) * ((h /. (p1 . i)) - (h /. t))).|| = ( |.( xvol DMN).| * ||.((h /. (p1 . i)) - (h /. t)).||) & ||.(( xvol DMN) * ((h /. t) - (h /. (p2 . j)))).|| = ( |.( xvol DMN).| * ||.((h /. t) - (h /. (p2 . j))).||) by NORMSP_1:def 1;

              then

               A98: ||.(( xvol DMN) * ((h /. (p1 . i)) - (h /. t))).|| = (( xvol DMN) * ||.((h /. (p1 . i)) - (h /. t)).||) & ||.(( xvol DMN) * ((h /. t) - (h /. (p2 . j)))).|| = (( xvol DMN) * ||.((h /. t) - (h /. (p2 . j))).||) by Th5, ABSVALUE:def 1;

               0 <= ( xvol DMN) by Th5;

              then ||.(( xvol DMN) * ((h /. (p1 . i)) - (h /. t))).|| <= (( xvol DMN) * p2v) & ||.(( xvol DMN) * ((h /. t) - (h /. (p2 . j)))).|| <= (( xvol DMN) * p2v) by A98, A96, XREAL_1: 64;

              then ( ||.(( xvol DMN) * ((h /. (p1 . i)) - (h /. t))).|| + ||.(( xvol DMN) * ((h /. t) - (h /. (p2 . j)))).||) <= ((( xvol DMN) * p2v) + (( xvol DMN) * p2v)) by XREAL_1: 7;

              hence ||.(Snmij - Smnij).|| <= (( xvol (( divset ((T . n),i)) /\ ( divset ((T . m),j)))) * pv) by A97, XXREAL_0: 2;

            end;

          end;

          

           A99: for j be Nat st j in ( dom XZq) holds ||.(XZq /. j).|| <= (( vol ( divset ((T . m),j))) * pv)

          proof

            let j be Nat;

            assume

             A100: j in ( dom XZq);

            then

             A101: (XZq /. j) = ((Xq /. j) - (Zq /. j)) by VFUNCT_1:def 2;

            

             A102: (Xq /. j) = (Xq . j) & (Zq /. j) = (Zq . j) by A100, A65, A53, A80, PARTFUN1:def 6;

            

             A103: ( dom XZq) = (( dom Xq) /\ ( dom Zq)) by VFUNCT_1:def 2;

            consider Xsq be FinSequence of X such that

             A104: ( dom Xsq) = ( Seg ( len (T . n))) & (Xq . j) = ( Sum Xsq) & for i be Nat st i in ( dom Xsq) holds (Xsq . i) = (Snm . (i,j)) by A100, A53, A65, A80;

            consider Zsq be FinSequence of X such that

             A105: ( dom Zsq) = ( Seg ( len (T . n))) & (Zq . j) = ( Sum Zsq) & for i be Nat st i in ( dom Zsq) holds (Zsq . i) = (Smn . (i,j)) by A100, A65, A53, A80;

            set XZsq = (Xsq - Zsq);

            

             A106: ( dom XZsq) = (( dom Xsq) /\ ( dom Zsq)) by VFUNCT_1:def 2;

            then

            reconsider XZsq as FinSequence by A104, A105, FINSEQ_1:def 2;

            now

              let i be Nat;

              assume i in ( dom XZsq);

              then (XZsq . i) = ((Xsq - Zsq) /. i) by PARTFUN1:def 6;

              hence (XZsq . i) in the carrier of X;

            end;

            then

            reconsider XZsq as FinSequence of X by FINSEQ_2: 12;

            defpred P11[ Nat, set] means $2 = ( xvol (( divset ((T . n),$1)) /\ ( divset ((T . m),j))));

            

             A107: for i be Nat st i in ( Seg ( len XZsq)) holds ex x be Element of REAL st P11[i, x]

            proof

              let i be Nat;

              assume i in ( Seg ( len XZsq));

              ( xvol (( divset ((T . n),i)) /\ ( divset ((T . m),j)))) in REAL by XREAL_0:def 1;

              hence thesis;

            end;

            consider vtntm be FinSequence of REAL such that

             A108: ( dom vtntm) = ( Seg ( len XZsq)) & for i be Nat st i in ( Seg ( len XZsq)) holds P11[i, (vtntm . i)] from FINSEQ_1:sch 5( A107);

            

             A109: for i be Nat st i in ( dom vtntm) holds (vtntm . i) = ( xvol (( divset ((T . m),j)) /\ ( divset ((T . n),i)))) by A108;

            

             A110: ( len vtntm) = ( len XZsq) by A108, FINSEQ_1:def 3;

            

             A111: ( len XZsq) = ( len (T . n)) by A104, A105, A106, FINSEQ_1:def 3;

            reconsider pvtntm = (pv * vtntm) as FinSequence of REAL ;

            j in ( dom (T . m)) by A100, A103, A53, A65, FINSEQ_1:def 3;

            then ( divset ((T . m),j)) c= A by INTEGRA1: 8;

            then ( Sum vtntm) = ( vol ( divset ((T . m),j))) by Th8, A109, A110, A104, A105, A106, FINSEQ_1:def 3;

            then

             A112: ( Sum pvtntm) = (pv * ( vol ( divset ((T . m),j)))) by RVSUM_1: 87;

            ( dom pvtntm) = ( dom vtntm) by VALUED_1:def 5;

            then ( dom pvtntm) = ( Seg ( len (T . n))) by A104, A105, A106, A108, FINSEQ_1:def 3;

            then

             A113: ( len pvtntm) = ( len (T . n)) by FINSEQ_1:def 3;

            for i be Nat st i in ( dom XZsq) holds ||.(XZsq /. i).|| <= (pvtntm . i)

            proof

              let i be Nat;

              assume

               A114: i in ( dom XZsq);

              then

               A115: (XZsq /. i) = ((Xsq /. i) - (Zsq /. i)) by VFUNCT_1:def 2;

              (Xsq /. i) = (Xsq . i) & (Zsq /. i) = (Zsq . i) by PARTFUN1:def 6, A114, A105, A106, A104;

              then

               A116: (Xsq /. i) = (Snm . (i,j)) & (Zsq /. i) = (Smn . (i,j)) by A114, A104, A106, A105;

              ( dom vtntm) = ( dom XZsq) by A108, FINSEQ_1:def 3;

              then (pv * (vtntm . i)) = (pv * ( xvol (( divset ((T . n),i)) /\ ( divset ((T . m),j))))) by A108, A114;

              then ((pv (#) vtntm) . i) = (pv * ( xvol (( divset ((T . n),i)) /\ ( divset ((T . m),j))))) by VALUED_1: 6;

              hence thesis by A115, A116, A82, A114, A104, A105, A106, A100, A103, A53, A65;

            end;

            then

             A117: ||.( Sum XZsq).|| <= (( vol ( divset ((T . m),j))) * pv) by A112, Th10, A111, A113;

            ( len Xsq) = ( len Zsq) by FINSEQ_3: 29, A104, A105;

            hence thesis by A101, A102, A104, A105, A117, INTEGR18: 2;

          end;

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

          

           A118: for i be Nat st i in ( Seg ( len XZq)) holds ex x be Element of REAL st P12[i, x]

          proof

            let i be Nat;

            assume i in ( Seg ( len XZq));

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

            hence thesis;

          end;

          consider vtm be FinSequence of REAL such that

           A119: ( dom vtm) = ( Seg ( len XZq)) & for i be Nat st i in ( Seg ( len XZq)) holds P12[i, (vtm . i)] from FINSEQ_1:sch 5( A118);

          

           A120: ( len XZq) = ( len (T . m)) by A53, A65, A80, FINSEQ_1:def 3;

          

           A121: ( Seg ( len XZq)) = ( dom XZq) by FINSEQ_1:def 3;

          

           A122: ( Sum vtm) = ( vol A) by A119, Th6, A120;

          reconsider pvtm = (pv * vtm) as FinSequence of REAL ;

          ( dom pvtm) = ( dom vtm) by VALUED_1:def 5;

          then ( dom pvtm) = ( Seg ( len (T . m))) by A53, A65, A80, A119, FINSEQ_1:def 3;

          then

           A123: ( len pvtm) = ( len (T . m)) by FINSEQ_1:def 3;

          

           A124: ( Sum pvtm) = (pv * ( vol A)) by RVSUM_1: 87, A122;

          for j be Nat st j in ( dom XZq) holds ||.(XZq /. j).|| <= (pvtm . j)

          proof

            let j be Nat;

            assume

             A125: j in ( dom XZq);

            then (vtm . j) = ( vol ( divset ((T . m),j))) by A119, A121;

            then (pvtm . j) = (( vol ( divset ((T . m),j))) * pv) by VALUED_1: 6;

            hence ||.(XZq /. j).|| <= (pvtm . j) by A125, A99;

          end;

          then ||.( Sum XZq).|| <= (( vol A) * pv) by A124, A120, A123, Th10;

          hence ||.((( middle_sum (h,S)) . n) - (( middle_sum (h,S)) . m)).|| < p by A19, A81, XXREAL_0: 2, A14;

        end;

        hence ( middle_sum (h,S)) is convergent by RSSPACE3: 8, LOPBAN_1:def 15;

      end;

    end;

    scheme :: INTEGR20:sch1

    ExRealSeq2X { D() -> non empty set , F,G( set) -> Element of D() } :

ex s be sequence of D() st for n be Nat holds (s . (2 * n)) = F(n) & (s . ((2 * n) + 1)) = G(n);

      defpred X[ set] means ex m be Nat st $1 = (2 * m);

      consider N be Subset of NAT such that

       A1: for n be Element of NAT holds n in N iff X[n] from SUBSET_1:sch 3;

      defpred Y[ set] means ex m be Nat st $1 = ((2 * m) + 1);

      consider M be Subset of NAT such that

       A2: for n be Element of NAT holds n in M iff Y[n] from SUBSET_1:sch 3;

      defpred X[ Nat, set] means ($1 in N implies $2 = F(/)) & ($1 in M implies $2 = G(/));

      

       A3: for n holds ex r be Element of D() st X[n, r]

      proof

        let n be Element of NAT ;

        now

          assume

           A4: n in N;

          reconsider r = F(/) as Element of D();

          take r;

          hereby

            assume n in M;

            then

             A5: ex k be Nat st n = ((2 * k) + 1) by A2;

            ex m be Nat st n = (2 * m) by A1, A4;

            hence contradiction by A5;

          end;

        end;

        hence thesis;

      end;

      consider f be sequence of D() such that

       A6: for n be Element of NAT holds X[n, (f . n)] from FUNCT_2:sch 3( A3);

      reconsider f as sequence of D();

      take f;

      let n be Nat;

      reconsider m = (2 * n) as Nat;

      

       A7: m in NAT by ORDINAL1:def 12;

      (f . ((2 * n) + 1)) = G(/) by A6, A2;

      hence (f . (2 * n)) = F(n) & (f . ((2 * n) + 1)) = G(n) by A1, A6, A7;

    end;

    theorem :: INTEGR20:14

    

     Th14: for n be Nat holds ex k be Nat st n = (2 * k) or n = ((2 * k) + 1)

    proof

      let n be Nat;

      per cases ;

        suppose n is even;

        then

        consider k be Nat such that

         A1: n = (2 * k);

        take k;

        thus n = (2 * k) or n = ((2 * k) + 1) by A1;

      end;

        suppose n is odd;

        then (n + 1) is even;

        then

        consider k1 be Nat such that

         A2: (n + 1) = (2 * k1);

         0 <> k1 by A2;

        then

        reconsider k = (k1 - 1) as Nat;

        take k;

        thus n = (2 * k) or n = ((2 * k) + 1) by A2;

      end;

    end;

    theorem :: INTEGR20:15

    

     Th15: for A be non empty closed_interval Subset of REAL , T0,T be DivSequence of A holds ex T1 be DivSequence of A st for i be Nat holds (T1 . (2 * i)) = (T0 . i) & (T1 . ((2 * i) + 1)) = (T . i)

    proof

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

      

       A1: ( dom T0) = NAT & ( dom T) = NAT by FUNCT_2:def 1;

      now

        let i be object;

        assume i in NAT ;

        then

        reconsider i1 = i as Nat;

        ( rng (T0 . i1)) c= REAL ;

        hence (T0 . i) in ( REAL * ) by FINSEQ_1:def 11;

      end;

      then

      reconsider S0 = T0 as sequence of ( REAL * ) by A1, FUNCT_2: 3;

      now

        let i be object;

        assume i in NAT ;

        then

        reconsider i1 = i as Nat;

        ( rng (T . i1)) c= REAL ;

        hence (T . i) in ( REAL * ) by FINSEQ_1:def 11;

      end;

      then

      reconsider S = T as sequence of ( REAL * ) by A1, FUNCT_2: 3;

      deffunc F( Nat) = (S0 /. $1);

      deffunc G( Nat) = (S /. $1);

      consider T1 be sequence of ( REAL * ) such that

       A2: for n be Nat holds (T1 . (2 * n)) = F(n) & (T1 . ((2 * n) + 1)) = G(n) from ExRealSeq2X;

      

       A3: ( dom T1) = NAT by FUNCT_2:def 1;

      now

        let i be object;

        assume i in NAT ;

        then

        reconsider j = i as Nat;

        consider k be Nat such that

         A4: j = (2 * k) or j = ((2 * k) + 1) by Th14;

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

        per cases by A4;

          suppose j = (2 * k);

          

          then (T1 . j) = (S0 /. k) by A2

          .= (T0 . k);

          hence (T1 . i) in ( divs A) by INTEGRA1:def 3;

        end;

          suppose j = ((2 * k) + 1);

          

          then (T1 . j) = (S /. k) by A2

          .= (T . k);

          hence (T1 . i) in ( divs A) by INTEGRA1:def 3;

        end;

      end;

      then

      reconsider T1 as DivSequence of A by A3, FUNCT_2: 3;

      take T1;

      let i be Nat;

      i in NAT by ORDINAL1:def 12;

      then

       A5: i in ( dom S0) & i in ( dom S) by FUNCT_2:def 1;

      

       A6: (T1 . (2 * i)) = (S0 /. i) by A2

      .= (T0 . i) by A5, PARTFUN1:def 6;

      (T1 . ((2 * i) + 1)) = (S /. i) by A2

      .= (T . i) by A5, PARTFUN1:def 6;

      hence thesis by A6;

    end;

    theorem :: INTEGR20:16

    

     Th16: for A be non empty closed_interval Subset of REAL , T0,T,T1 be DivSequence of A st ( delta T0) is convergent & ( lim ( delta T0)) = 0 & ( delta T) is convergent & ( lim ( delta T)) = 0 & for i be Nat holds (T1 . (2 * i)) = (T0 . i) & (T1 . ((2 * i) + 1)) = (T . i) holds ( delta T1) is convergent & ( lim ( delta T1)) = 0

    proof

      let A be non empty closed_interval Subset of REAL , T0,T,T1 be DivSequence of A;

      assume that

       A1: ( delta T0) is convergent & ( lim ( delta T0)) = 0 and

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

       A3: for i be Nat holds (T1 . (2 * i)) = (T0 . i) & (T1 . ((2 * i) + 1)) = (T . i);

       A4:

      now

        let p be Real;

        assume

         A5: 0 < p;

        then

        consider n1 be Nat such that

         A6: for m be Nat st n1 <= m holds |.((( delta T0) . m) - 0 ).| < p by A1, SEQ_2:def 7;

        consider n2 be Nat such that

         A7: for m be Nat st n2 <= m holds |.((( delta T) . m) - 0 ).| < p by A5, A2, SEQ_2:def 7;

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

        

         A8: n1 <= n3 & n2 <= n3 by XXREAL_0: 25;

        reconsider n = ((2 * n3) + 1) as Nat;

        take n;

        let m be Nat;

        assume

         A9: n <= m;

        consider k be Nat such that

         A10: m = (2 * k) or m = ((2 * k) + 1) by Th14;

        reconsider k1 = k, m1 = m as Element of NAT by ORDINAL1:def 12;

        per cases by A10;

          suppose

           A11: m = (2 * k);

          (( delta T1) . m1) = ( delta (T1 . m1)) by INTEGRA3:def 2;

          then (( delta T1) . m1) = ( delta (T0 . k1)) by A11, A3;

          then

           A12: (( delta T1) . m1) = (( delta T0) . k1) by INTEGRA3:def 2;

          

           A13: (2 * n3) <= ((2 * k) - 1) by XREAL_1: 19, A9, A11;

          ((2 * k) - 1) < (((2 * k) - 1) + 1) by XREAL_1: 145;

          then (2 * n3) <= (2 * k) by A13, XXREAL_0: 2;

          then ((2 * n3) / 2) <= ((2 * k) / 2) by XREAL_1: 72;

          then n1 <= k by A8, XXREAL_0: 2;

          hence |.((( delta T1) . m) - 0 ).| < p by A12, A6;

        end;

          suppose

           A14: m = ((2 * k) + 1);

          (( delta T1) . m1) = ( delta (T1 . m1)) by INTEGRA3:def 2;

          then (( delta T1) . m1) = ( delta (T . k1)) by A14, A3;

          then

           A15: (( delta T1) . m1) = (( delta T) . k1) by INTEGRA3:def 2;

          (((2 * n3) + 1) - 1) <= (((2 * k) + 1) - 1) by XREAL_1: 13, A9, A14;

          then ((2 * n3) / 2) <= ((2 * k) / 2) by XREAL_1: 72;

          then n2 <= k by A8, XXREAL_0: 2;

          hence |.((( delta T1) . m) - 0 ).| < p by A15, A7;

        end;

      end;

      hence ( delta T1) is convergent by SEQ_2:def 6;

      hence ( lim ( delta T1)) = 0 by A4, SEQ_2:def 7;

    end;

    theorem :: INTEGR20:17

    

     Th17: for X be RealNormSpace, A be non empty closed_interval Subset of REAL , h be Function of A, the carrier of X, T0,T,T1 be DivSequence of A, S0 be middle_volume_Sequence of h, T0, S be middle_volume_Sequence of h, T st for i be Nat holds (T1 . (2 * i)) = (T0 . i) & (T1 . ((2 * i) + 1)) = (T . i) holds ex S1 be middle_volume_Sequence of h, T1 st for i be Nat holds (S1 . (2 * i)) = (S0 . i) & (S1 . ((2 * i) + 1)) = (S . i)

    proof

      let X be RealNormSpace, A be non empty closed_interval Subset of REAL , h be Function of A, the carrier of X, T0,T,T1 be DivSequence of A, S0 be middle_volume_Sequence of h, T0, S be middle_volume_Sequence of h, T;

      assume

       A1: for k be Nat holds (T1 . (2 * k)) = (T0 . k) & (T1 . ((2 * k) + 1)) = (T . k);

      reconsider SS0 = S0, SS = S as sequence of (the carrier of X * );

      deffunc F( Nat) = (SS0 /. $1);

      deffunc G( Nat) = (SS /. $1);

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

       A2: for n be Nat holds (S1 . (2 * n)) = F(n) & (S1 . ((2 * n) + 1)) = G(n) from ExRealSeq2X;

      for i be Element of NAT holds (S1 . i) is middle_volume of h, (T1 . i)

      proof

        let i be Element of NAT ;

        consider k be Nat such that

         A3: i = (2 * k) or i = ((2 * k) + 1) by Th14;

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

        per cases by A3;

          suppose

           A4: i = (2 * k);

          

          then (S1 . i) = (SS0 /. k) by A2

          .= (S0 . k);

          hence (S1 . i) is middle_volume of h, (T1 . i) by A4, A1;

        end;

          suppose

           A5: i = ((2 * k) + 1);

          

          then (S1 . i) = (SS /. k) by A2

          .= (S . k);

          hence (S1 . i) is middle_volume of h, (T1 . i) by A5, A1;

        end;

      end;

      then

      reconsider S1 as middle_volume_Sequence of h, T1 by INTEGR18:def 3;

      take S1;

      let i be Nat;

      i in NAT by ORDINAL1:def 12;

      then

       A6: i in ( dom SS0) & i in ( dom SS) by FUNCT_2:def 1;

      

       A7: (S1 . (2 * i)) = (SS0 /. i) by A2

      .= (S0 . i) by PARTFUN1:def 6, A6;

      (S1 . ((2 * i) + 1)) = (SS /. i) by A2

      .= (S . i) by PARTFUN1:def 6, A6;

      hence thesis by A7;

    end;

    theorem :: INTEGR20:18

    

     Th18: for X be RealNormSpace, Sq0,Sq,Sq1 be sequence of X st Sq1 is convergent & for i be Nat holds (Sq1 . (2 * i)) = (Sq0 . i) & (Sq1 . ((2 * i) + 1)) = (Sq . i) holds Sq0 is convergent & ( lim Sq0) = ( lim Sq1) & Sq is convergent & ( lim Sq) = ( lim Sq1)

    proof

      let X be RealNormSpace, Sq0,Sq,Sq1 be sequence of X;

      assume that

       A1: Sq1 is convergent and

       A2: for i be Nat holds (Sq1 . (2 * i)) = (Sq0 . i) & (Sq1 . ((2 * i) + 1)) = (Sq . i);

      

       A3: for r be Real st 0 < r holds ex m1 be Nat st for i be Nat st m1 <= i holds ||.((Sq0 . i) - ( lim Sq1)).|| < r

      proof

        let r be Real;

        assume 0 < r;

        then

        consider m be Nat such that

         A4: for n be Nat st m <= n holds ||.((Sq1 . n) - ( lim Sq1)).|| < r by A1, NORMSP_1:def 7;

        consider k be Nat such that

         A5: m = (2 * k) or m = ((2 * k) + 1) by Th14;

        ((2 * k) + 1) <= (((2 * k) + 1) + 1) by NAT_1: 11;

        then

         A6: m <= ((2 * k) + 2) by A5, XREAL_1: 31;

        reconsider m1 = (k + 1) as Nat;

        take m1;

        thus for i be Nat st m1 <= i holds ||.((Sq0 . i) - ( lim Sq1)).|| < r

        proof

          let i be Nat;

          assume m1 <= i;

          then (2 * m1) <= (2 * i) by XREAL_1: 64;

          then m <= (2 * i) by A6, XXREAL_0: 2;

          then ||.((Sq1 . (2 * i)) - ( lim Sq1)).|| < r by A4;

          hence ||.((Sq0 . i) - ( lim Sq1)).|| < r by A2;

        end;

      end;

      hence Sq0 is convergent;

      hence ( lim Sq0) = ( lim Sq1) by A3, NORMSP_1:def 7;

      

       A7: for r be Real st 0 < r holds ex m1 be Nat st for i be Nat st m1 <= i holds ||.((Sq . i) - ( lim Sq1)).|| < r

      proof

        let r be Real;

        assume 0 < r;

        then

        consider m be Nat such that

         A8: for n be Nat st m <= n holds ||.((Sq1 . n) - ( lim Sq1)).|| < r by A1, NORMSP_1:def 7;

        consider k be Nat such that

         A9: m = (2 * k) or m = ((2 * k) + 1) by Th14;

        ((2 * k) + 1) <= (((2 * k) + 1) + 1) by NAT_1: 11;

        then

         A10: m <= ((2 * k) + 2) by A9, XREAL_1: 31;

        reconsider m1 = (k + 1) as Nat;

        take m1;

        thus for i be Nat st m1 <= i holds ||.((Sq . i) - ( lim Sq1)).|| < r

        proof

          let i be Nat;

          assume m1 <= i;

          then (2 * m1) <= (2 * i) by XREAL_1: 64;

          then m <= (2 * i) by A10, XXREAL_0: 2;

          then m <= ((2 * i) + 1) by XREAL_1: 145;

          then ||.((Sq1 . ((2 * i) + 1)) - ( lim Sq1)).|| < r by A8;

          hence ||.((Sq . i) - ( lim Sq1)).|| < r by A2;

        end;

      end;

      hence Sq is convergent;

      hence ( lim Sq) = ( lim Sq1) by NORMSP_1:def 7, A7;

    end;

    theorem :: INTEGR20:19

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

    proof

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

      set A = ['a, b'];

      assume

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

      then

      reconsider h = (f | A) as Function of A, the carrier of X by Lm1;

      

       A2: (f | A) is uniformly_continuous by A1, Th3;

      consider T0 be DivSequence of A such that

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

      set S0 = the middle_volume_Sequence of h, T0;

      set I = ( lim ( middle_sum (h,S0)));

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

      proof

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

        assume

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

        hence ( middle_sum (h,S)) is convergent by A2, Th13;

        consider T1 be DivSequence of A such that

         A5: for i be Nat holds (T1 . (2 * i)) = (T0 . i) & (T1 . ((2 * i) + 1)) = (T . i) by Th15;

        consider S1 be middle_volume_Sequence of h, T1 such that

         A6: for i be Nat holds (S1 . (2 * i)) = (S0 . i) & (S1 . ((2 * i) + 1)) = (S . i) by A5, Th17;

        ( delta T1) is convergent & ( lim ( delta T1)) = 0 by A4, A5, A3, Th16;

        then

         A7: ( middle_sum (h,S1)) is convergent by A2, Th13;

        

         A8: for i be Nat holds (( middle_sum (h,S1)) . (2 * i)) = (( middle_sum (h,S0)) . i) & (( middle_sum (h,S1)) . ((2 * i) + 1)) = (( middle_sum (h,S)) . i)

        proof

          let i be Nat;

          reconsider S1 as middle_volume_Sequence of h, T1;

          (( middle_sum (h,S1)) . (2 * i)) = ( middle_sum (h,(S1 . (2 * i)))) & (( middle_sum (h,S1)) . ((2 * i) + 1)) = ( middle_sum (h,(S1 . ((2 * i) + 1)))) by INTEGR18:def 4;

          then (( middle_sum (h,S1)) . (2 * i)) = ( middle_sum (h,(S0 . i))) & (( middle_sum (h,S1)) . ((2 * i) + 1)) = ( middle_sum (h,(S . i))) by A6;

          hence thesis by INTEGR18:def 4;

        end;

        ( lim ( middle_sum (h,S))) = ( lim ( middle_sum (h,S1))) by A7, A8, Th18;

        hence ( lim ( middle_sum (h,S))) = ( lim ( middle_sum (h,S0))) by A7, A8, Th18;

      end;

      then h is integrable;

      hence thesis;

    end;