integr23.miz



    begin

    theorem :: INTEGR23:1

    

     Th1: for E be Real, q be FinSequence of REAL , S be FinSequence of REAL 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 E be Real;

      defpred P[ Nat] means for q be FinSequence of REAL , S be FinSequence of REAL 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 REAL ;

        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 ( <*> REAL ) = S & ( <*> REAL ) = q;

        hence thesis by RVSUM_1: 72;

      end;

       A3:

      now

        let i be Nat;

        assume

         A4: P[i];

        now

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

          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 A7, A8, 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));

          

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

          reconsider v = (S . (i + 1)) as Real;

          S = ((S | i) ^ <*(S /. ( len S))*>) by A5, FINSEQ_5: 21;

          then S = (S0 ^ <*v*>) by A5, A10, FINSEQ_4: 15;

          then ( Sum S) = (( Sum S0) + v) by RVSUM_1: 74;

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

        end;

        hence P[(i + 1)];

      end;

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

      hence thesis;

    end;

    

     Lm1: for xseq,yseq be FinSequence of REAL st ( len xseq) = (( len yseq) + 1) & (xseq | ( len yseq)) = yseq holds ex v be Real st v = (xseq . ( len xseq)) & ( Sum xseq) = (( Sum yseq) + v)

    proof

      let xseq,yseq be FinSequence of REAL ;

      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 v = (xseq /. ( len xseq)) by PARTFUN1:def 6;

      then xseq = ((xseq | ( len yseq)) ^ <*v*>) by A1, FINSEQ_5: 21;

      hence thesis by A1, RVSUM_1: 74;

    end;

    theorem :: INTEGR23:2

    

     Th2: for xseq,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 Real st v = (xseq . i) & (yseq . i) = |.v.|) holds |.( Sum xseq).| <= ( Sum yseq)

    proof

      defpred P[ Nat] means for xseq,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 Real st v = (xseq . i) & (yseq . i) = |.v.|) holds |.( Sum xseq).| <= ( Sum yseq);

      

       A1: P[ 0 ]

      proof

        let xseq be FinSequence of REAL , 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 Real st v = (xseq . i) & (yseq . i) = |.v.|);

        then ( <*> REAL ) = xseq;

        then ( Sum xseq) = 0 & ( <*> REAL ) = yseq by A2, RVSUM_1: 72;

        hence thesis by COMPLEX1: 44, RVSUM_1: 72;

      end;

       A3:

      now

        let i be Nat;

        assume

         A4: P[i];

        now

          let xseq be FinSequence of REAL , 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 Real st v = (xseq . i) & (yseq . i) = |.v.|;

          

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

          proof

            let k be Element of NAT ;

            assume k in ( dom xseq0);

            then

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

            then

            consider v be Real such that

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

            take v;

            thus thesis by A8, A9, FUNCT_1: 49;

          end;

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

          then

          consider w be Real 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 Real st v = (xseq . ( len xseq)) & ( Sum xseq) = (( Sum xseq0) + v) by A5, Lm1;

          

           A15: |.(( Sum xseq0) + w).| <= ( |.( Sum xseq0).| + |.w.|) by COMPLEX1: 56;

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

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

          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 :: INTEGR23:3

    

     Th3: for p,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 p,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 Real 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 by XREAL_0:def 1;

        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 Real 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 Real 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, Th2;

      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 Real st v = (p . j) & (u . j) = |.v.| by A4;

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

      end;

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

      hence thesis by A6, XXREAL_0: 2;

    end;

    theorem :: INTEGR23:4

    

     Th4: for n be Nat, a be object holds ( len (n |-> a)) = n

    proof

      let n be Nat, a be object;

      set x = (n |-> a);

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

      hence thesis by FINSEQ_1: 6, FUNCOP_1: 13;

    end;

    theorem :: INTEGR23:5

    

     Th5: for p be FinSequence, a be object holds p = (( len p) |-> a) iff (for k be object st k in ( dom p) holds (p . k) = a)

    proof

      let p be FinSequence, a be object;

      thus p = (( len p) |-> a) implies for k be object st k in ( dom p) holds (p . k) = a

      proof

        assume

         A2: p = (( len p) |-> a);

        let k be object;

        assume k in ( dom p);

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

        hence thesis by A2, FINSEQ_2: 57;

      end;

      assume for k be object st k in ( dom p) holds (p . k) = a;

      then p = (( dom p) --> a) by FUNCOP_1: 11;

      hence thesis by FINSEQ_1:def 3;

    end;

    theorem :: INTEGR23:6

    

     Th8: for p be FinSequence of REAL , i be Nat, r be Real st i in ( dom p) & (p . i) = r & for k be Nat st k in ( dom p) & k <> i holds (p . k) = 0 holds ( Sum p) = r

    proof

      defpred P[ Nat] means for p be FinSequence of REAL , i be Nat, r be Real st ( len p) = $1 & i in ( dom p) & (p . i) = r & (for k be Nat st k in ( dom p) & k <> i holds (p . k) = 0 ) holds ( Sum p) = r;

      

       A1: P[ 0 ]

      proof

        let p be FinSequence of REAL , i be Nat, r be Real;

        assume that

         A2: ( len p) = 0 and

         A3: i in ( dom p) and (p . i) = r and for k be Nat st k in ( dom p) & k <> i holds (p . k) = 0 ;

        p = ( <*> REAL ) by A2;

        hence thesis by A3;

      end;

      

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

      proof

        let n be Nat;

        assume

         A5: P[n];

         P[(n + 1)]

        proof

          let p be FinSequence of REAL , i be Nat, r be Real;

          assume that

           A6: ( len p) = (n + 1) and

           A7: i in ( dom p) and

           A8: (p . i) = r and

           A9: for k be Nat st k in ( dom p) & k <> i holds (p . k) = 0 ;

          consider q be FinSequence of REAL , a be Element of REAL such that

           A10: p = (q ^ <*a*>) by A6, FINSEQ_2: 19;

          

           A11: ( len p) = (( len q) + 1) by A10, FINSEQ_2: 16;

          

           A12: 1 <= i <= (n + 1) by A6, A7, FINSEQ_3: 25;

          per cases ;

            suppose

             A13: i <> (n + 1);

            then 1 <= i < (n + 1) by A12, XXREAL_0: 1;

            then

             A14: 1 <= i <= n by INT_1: 7;

            

             A15: (q . i) = r

            proof

              q = (p | ( dom q)) by A10, FINSEQ_1: 21;

              hence thesis by A6, A8, A11, A14, FUNCT_1: 47, FINSEQ_3: 25;

            end;

            

             A17: for k be Nat st k in ( dom q) & k <> i holds (q . k) = 0

            proof

              let k be Nat;

              assume that

               A18: k in ( dom q) and

               A19: k <> i;

              

               A20: ( dom q) c= ( dom p) by A10, FINSEQ_1: 26;

              (q . k) = (p . k) by A10, A18, FINSEQ_1:def 7

              .= 0 by A9, A18, A19, A20;

              hence thesis;

            end;

            

             A21: 1 <= (n + 1) <= (n + 1) by XREAL_1: 31;

            a = (p . (n + 1)) by A6, A10, A11, FINSEQ_1: 42

            .= 0 by A6, A9, A13, A21, FINSEQ_3: 25;

            

            then ( Sum p) = (( Sum q) + 0 ) by A10, RVSUM_1: 74

            .= r by A5, A6, A11, A14, A15, A17, FINSEQ_3: 25;

            hence thesis;

          end;

            suppose

             A22: i = (n + 1);

            for k be object st k in ( dom q) holds (q . k) = 0

            proof

              let k be object;

              assume

               A23: k in ( dom q);

              then

              reconsider k as Nat;

              

               A24: 1 <= k <= n by A6, A11, A23, FINSEQ_3: 25;

              

               A25: ( dom q) c= ( dom p) by A10, FINSEQ_1: 26;

              

               A26: (k + 0 ) < (n + 1) by A24, XREAL_1: 8;

              (q . k) = (p . k) by A10, A23, FINSEQ_1:def 7

              .= 0 by A9, A22, A23, A25, A26;

              hence thesis;

            end;

            then

             A27: q = (n |-> 0 qua Real) by A6, A11, Th5;

            

             A28: a = r by A6, A8, A10, A11, A22, FINSEQ_1: 42;

            ( Sum p) = (( Sum q) + a) by A10, RVSUM_1: 74

            .= ( 0 + r) by A27, A28, RVSUM_1: 81;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      

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

      let p be FinSequence of REAL , i be Nat, r be Real;

      assume

       A30: i in ( dom p) & (p . i) = r & for k be Nat st k in ( dom p) & k <> i holds (p . k) = 0 ;

      ( len p) is Nat;

      hence thesis by A29, A30;

    end;

    theorem :: INTEGR23:7

    

     Th9: for p,q be FinSequence of REAL st ( len p) <= ( len q) & for i be Nat st i in ( dom q) holds (i <= ( len p) implies (q . i) = (p . i)) & (( len p) < i implies (q . i) = 0 ) holds ( Sum q) = ( Sum p)

    proof

      let p,q be FinSequence of REAL ;

      assume that

       A1: ( len p) <= ( len q) and

       A2: for i be Nat st i in ( dom q) holds (i <= ( len p) implies (q . i) = (p . i)) & (( len p) < i implies (q . i) = 0 );

      (( len q) - ( len p)) is Nat by A1, NAT_1: 21;

      then

      consider ix be Nat such that

       A3: ix = (( len q) - ( len p));

      set x = (ix |-> 0 qua Real);

      

       A5: ( Sum x) = 0 by RVSUM_1: 81;

      q = (p ^ x)

      proof

        

         A6: ( len x) = ix by Th4;

        then

         A7: ( len q) = (( len p) + ( len x)) by A3;

        

         A8: ( dom q) = ( Seg (( len p) + ( len x))) by A3, A6, FINSEQ_1:def 3;

        

         A9: for i be Nat st i in ( dom p) holds (q . i) = (p . i)

        proof

          let i be Nat;

          assume i in ( dom p);

          then

           A10: 1 <= i <= ( len p) by FINSEQ_3: 25;

          then 1 <= i <= ( len q) by A1, XXREAL_0: 2;

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

          hence thesis by A2, A10;

        end;

        for i be Nat st i in ( dom x) holds (q . (( len p) + i)) = (x . i)

        proof

          let i be Nat;

          assume i in ( dom x);

          then

           A11: i in ( Seg ix) by FUNCOP_1: 13;

          then

           A12: (x . i) = 0 by FINSEQ_2: 57;

          consider j be Nat such that

           A13: j = (( len p) + i);

          

           A14: i >= 1 by A11, FINSEQ_1: 1;

          then

           A15: ( len p) < j by A13, NAT_1: 19;

          

           A16: ( 0 + 1) <= j by A13, A14, INT_1: 7;

          i <= ( len x) by A6, A11, FINSEQ_1: 1;

          then j <= ( len q) by A7, A13, XREAL_1: 6;

          then j in ( dom q) by A16, FINSEQ_3: 25;

          hence thesis by A2, A12, A13, A15;

        end;

        hence thesis by A8, A9, FINSEQ_1:def 7;

      end;

      

      then ( Sum q) = (( Sum p) + ( Sum x)) by RVSUM_1: 75

      .= ( Sum p) by A5;

      hence thesis;

    end;

    theorem :: INTEGR23:8

    

     Th10: for a,b,c,d be Real st b <= c holds ( [.a, b.] /\ [.c, d.]) c= [.b, b.]

    proof

      let a,b,c,d be Real;

      assume

       A1: b <= c;

      per cases ;

        suppose

         A2: a <= b;

        per cases ;

          suppose c <= d;

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

          then ( [.a, b.] /\ [.b, d.]) = [.b, b.] by A2, XXREAL_1: 143;

          hence ( [.a, b.] /\ [.c, d.]) c= [.b, b.] by A1, XBOOLE_1: 26, XXREAL_1: 34;

        end;

          suppose d < c;

          then [.c, d.] = {} by XXREAL_1: 29;

          hence ( [.a, b.] /\ [.c, d.]) c= [.b, b.];

        end;

      end;

        suppose b < a;

        then [.a, b.] = {} by XXREAL_1: 29;

        hence ( [.a, b.] /\ [.c, d.]) c= [.b, b.];

      end;

    end;

    theorem :: INTEGR23:9

    

     Th11: for a be Real, A be Subset of REAL , rho be real-valued Function st A c= [.a, a.] holds ( vol (A,rho)) = 0

    proof

      let a be Real, A be Subset of REAL , rho be real-valued Function;

      assume A c= [.a, a.];

      then A c= {a} by XXREAL_1: 17;

      per cases by ZFMISC_1: 33;

        suppose A = {} ;

        hence ( vol (A,rho)) = 0 by INTEGR22:def 1;

      end;

        suppose A = {a};

        

        hence ( vol (A,rho)) = ((rho . ( upper_bound {a})) - (rho . ( lower_bound {a}))) by INTEGR22:def 1

        .= ((rho . ( upper_bound {a})) - (rho . ( upper_bound {a}))) by SEQ_4: 10

        .= 0 ;

      end;

    end;

    theorem :: INTEGR23:10

    

     Th12: for s be non empty increasing FinSequence of REAL , m be Nat st m in ( dom s) holds (s | m) is non empty increasing FinSequence of REAL

    proof

      let s be non empty increasing FinSequence of REAL , m be Nat;

      assume

       a0: m in ( dom s);

      then 1 <= m <= ( len s) by FINSEQ_3: 25;

      then

       A2: ( len (s | m)) = m by FINSEQ_1: 59;

      set H = (s | m);

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

      proof

        let e1,e2 be ExtReal;

        assume

         A3: e1 in ( dom H) & e2 in ( dom H) & e1 < e2;

        then

         A5: e1 in ( dom s) & e2 in ( dom s) by RELAT_1: 57;

        (s . e1) = (H . e1) & (s . e2) = (H . e2) by A3, FUNCT_1: 47;

        hence (H . e1) < (H . e2) by A3, A5, VALUED_0:def 13;

      end;

      hence thesis by A2, VALUED_0:def 13, a0, FINSEQ_3: 25;

    end;

    theorem :: INTEGR23:11

    

     Th13: for s,t be non empty increasing FinSequence of REAL st (s . ( len s)) < (t . 1) holds (s ^ t) is non empty increasing FinSequence of REAL

    proof

      let s,t be non empty increasing FinSequence of REAL ;

      assume

       A1: (s . ( len s)) < (t . 1);

      set H = (s ^ t);

      

       A2: ( len H) = (( len s) + ( len t)) by FINSEQ_1: 22;

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

      proof

        let e1,e2 be ExtReal;

        assume

         A3: e1 in ( dom H) & e2 in ( dom H) & e1 < e2;

        then

        reconsider ie1 = e1, ie2 = e2 as Nat;

        

         A5: 1 <= ie1 <= (( len s) + ( len t)) & 1 <= ie2 <= (( len s) + ( len t)) by A2, A3, FINSEQ_3: 25;

        per cases ;

          suppose

           A6: ie2 <= ( len s);

          then

           A7: ie1 <= ( len s) by A3, XXREAL_0: 2;

          

           A8: ie1 in ( dom s) & ie2 in ( dom s) by A5, A6, A7, FINSEQ_3: 25;

          then (H . e1) = (s . e1) & (H . e2) = (s . e2) by FINSEQ_1:def 7;

          hence (H . e1) < (H . e2) by A3, A8, VALUED_0:def 13;

        end;

          suppose

           A9: ( len s) < ie2;

          per cases ;

            suppose

             A10: ( len s) < ie1;

            then

             a10: ( len s) < ie2 by A3, XXREAL_0: 2;

            

             A11: not ie1 in ( dom s) & not ie2 in ( dom s) by A10, FINSEQ_3: 25, a10;

            then

            consider n1 be Nat such that

             A12: n1 in ( dom t) & ie1 = (( len s) + n1) by A3, FINSEQ_1: 25;

            consider n2 be Nat such that

             A13: n2 in ( dom t) & ie2 = (( len s) + n2) by A3, A11, FINSEQ_1: 25;

            

             A14: (H . e1) = (t . n1) by A12, FINSEQ_1:def 7;

            

             A15: (H . e2) = (t . n2) by A13, FINSEQ_1:def 7;

            (ie1 - ( len s)) < (ie2 - ( len s)) by A3, XREAL_1: 14;

            hence (H . e1) < (H . e2) by A12, A13, A14, A15, VALUED_0:def 13;

          end;

            suppose

             A16: ie1 <= ( len s);

             not ie2 in ( dom s) by FINSEQ_3: 25, A9;

            then

            consider n2 be Nat such that

             A17: n2 in ( dom t) & ie2 = (( len s) + n2) by A3, FINSEQ_1: 25;

            

             A18: 1 <= n2 <= ( len t) by A17, FINSEQ_3: 25;

            1 <= ( len t) by A18, XXREAL_0: 2;

            then 1 in ( dom t) by FINSEQ_3: 25;

            then

             A19: (t . 1) <= (t . n2) by A17, A18, VALUED_0:def 15;

            

             A20: (H . e2) = (t . n2) by A17, FINSEQ_1:def 7;

            

             A21: ie1 in ( dom s) by A5, A16, FINSEQ_3: 25;

            then

             A22: (H . e1) = (s . ie1) by FINSEQ_1:def 7;

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

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

            then (s . ie1) <= (s . ( len s)) by A16, A21, VALUED_0:def 15;

            then (s . ie1) < (t . 1) by A1, XXREAL_0: 2;

            hence (H . e1) < (H . e2) by A19, A20, A22, XXREAL_0: 2;

          end;

        end;

      end;

      hence thesis by VALUED_0:def 13;

    end;

    theorem :: INTEGR23:12

    

     Th14: for s be non empty increasing FinSequence of REAL , a be Real st (s . ( len s)) < a holds (s ^ <*a*>) is non empty increasing FinSequence of REAL

    proof

      let s be non empty increasing FinSequence of REAL , a be Real;

      assume

       A1: (s . ( len s)) < a;

      reconsider a0 = a as Element of REAL by XREAL_0:def 1;

      reconsider t = <*a0*> as non empty increasing FinSequence of REAL ;

      (s . ( len s)) < (t . 1) by A1, FINSEQ_1: 40;

      hence thesis by Th13;

    end;

    theorem :: INTEGR23:13

    

     Th15: for T be FinSequence of REAL , n,m be Nat st (n + 1) < m <= ( len T) holds ex TM1 be FinSequence of REAL st ( len TM1) = (m - (n + 1)) & ( rng TM1) c= ( rng T) & for i be Nat st i in ( dom TM1) holds (TM1 . i) = (T . (i + n))

    proof

      let T be FinSequence of REAL , n,m be Nat;

      assume

       A1: (n + 1) < m <= ( len T);

      deffunc F( Nat) = (T . ($1 + n));

      (m - (n + 1)) in NAT by A1, INT_1: 5;

      then

      reconsider m1 = (m - (n + 1)) as Nat;

      consider p be FinSequence such that

       A2: ( len p) = m1 & for k be Nat st k in ( dom p) holds (p . k) = F(k) from FINSEQ_1:sch 2;

      

       A3: ( rng p) c= ( rng T)

      proof

        let x be object;

        assume x in ( rng p);

        then

        consider i be object such that

         A4: i in ( dom p) & x = (p . i) by FUNCT_1:def 3;

        reconsider i as Nat by A4;

        

         A6: (p . i) = (T . (i + n)) by A2, A4;

        

         A7: 1 <= i <= m1 by A2, FINSEQ_3: 25, A4;

        

         A8: (i + n) <= (m1 + n) by A7, XREAL_1: 6;

        (m - 1) <= (m - 0 ) by XREAL_1: 10;

        then (m - 1) <= ( len T) by A1, XXREAL_0: 2;

        then

         A9: (i + n) <= ( len T) by A8, XXREAL_0: 2;

        (1 + 0 ) <= (i + n) by A7, XREAL_1: 7;

        then (i + n) in ( dom T) by FINSEQ_3: 25, A9;

        hence thesis by A4, A6, FUNCT_1: 3;

      end;

      then

      reconsider p as FinSequence of REAL by FINSEQ_1:def 4, XBOOLE_1: 1;

      take p;

      thus ( len p) = (m - (n + 1)) by A2;

      thus ( rng p) c= ( rng T) by A3;

      let i be Nat;

      assume i in ( dom p);

      hence thesis by A2;

    end;

    theorem :: INTEGR23:14

    

     Th16: for T be non empty increasing FinSequence of REAL , n,m be Nat st (n + 1) < m <= ( len T) holds ex TM1 be non empty increasing FinSequence of REAL st ( len TM1) = (m - (n + 1)) & ( rng TM1) c= ( rng T) & for i be Nat st i in ( dom TM1) holds (TM1 . i) = (T . (i + n))

    proof

      let T be non empty increasing FinSequence of REAL , n,m be Nat;

      assume

       A1: (n + 1) < m <= ( len T);

      then

      consider p be FinSequence of REAL such that

       A2: ( len p) = (m - (n + 1)) & ( rng p) c= ( rng T) & for i be Nat st i in ( dom p) holds (p . i) = (T . (i + n)) by Th15;

      (m - (n + 1)) in NAT by A1, INT_1: 5;

      then

      reconsider m1 = (m - (n + 1)) as Nat;

      ( len p) <> 0 by A1, A2;

      then

      reconsider p as non empty FinSequence of REAL ;

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

      proof

        let e1,e2 be ExtReal;

        assume

         A3: e1 in ( dom p) & e2 in ( dom p) & e1 < e2;

        then

        reconsider ie1 = e1, ie2 = e2 as Nat;

        

         A5: (p . e1) = (T . (ie1 + n)) by A2, A3;

        

         A6: (p . e2) = (T . (ie2 + n)) by A2, A3;

        

         A7: 1 <= ie1 <= m1 by A2, A3, FINSEQ_3: 25;

        

         A8: 1 <= ie2 <= m1 by A2, A3, FINSEQ_3: 25;

        

         A9: (ie1 + n) <= (m1 + n) by A7, XREAL_1: 6;

        (m - 1) <= (m - 0 ) by XREAL_1: 10;

        then

         A10: (m - 1) <= ( len T) by A1, XXREAL_0: 2;

        then

         A11: (ie1 + n) <= ( len T) by A9, XXREAL_0: 2;

        (1 + 0 ) <= (ie1 + n) by A7, XREAL_1: 7;

        then

         A12: (ie1 + n) in ( dom T) by A11, FINSEQ_3: 25;

        

         A13: (1 + 0 ) <= (ie2 + n) by A8, XREAL_1: 7;

        (ie2 + n) <= (m1 + n) by A8, XREAL_1: 6;

        then (ie2 + n) <= ( len T) by A10, XXREAL_0: 2;

        then

         A14: (ie2 + n) in ( dom T) by FINSEQ_3: 25, A13;

        (ie1 + n) < (ie2 + n) by A3, XREAL_1: 8;

        hence thesis by A5, A6, A12, A14, VALUED_0:def 13;

      end;

      then

      reconsider p as non empty increasing FinSequence of REAL by VALUED_0:def 13;

      take p;

      thus thesis by A2;

    end;

    theorem :: INTEGR23:15

    

     Th17: for p be FinSequence of REAL , n,m be Nat st (n + 1) < m <= ( len p) holds ex pM1 be FinSequence of REAL st ( len pM1) = ((m - (n + 1)) - 1) & ( rng pM1) c= ( rng p) & for i be Nat st i in ( dom pM1) holds (pM1 . i) = (p . ((i + n) + 1))

    proof

      let p be FinSequence of REAL , n,m be Nat;

      assume

       A1: (n + 1) < m <= ( len p);

      set n1 = (n + 1);

      

       A2: (n1 + 1) <= m by A1, NAT_1: 13;

      per cases ;

        suppose

         A3: (n1 + 1) = m;

        set pM1 = ( <*> REAL );

        take pM1;

        thus ( len pM1) = ((m - (n + 1)) - 1) by A3;

        thus ( rng pM1) c= ( rng p);

        thus for i be Nat st i in ( dom pM1) holds (pM1 . i) = (p . ((i + n) + 1));

      end;

        suppose (n1 + 1) <> m;

        then (n1 + 1) < m by A2, XXREAL_0: 1;

        then

        consider TM1 be FinSequence of REAL such that

         A4: ( len TM1) = (m - (n1 + 1)) & ( rng TM1) c= ( rng p) & for i be Nat st i in ( dom TM1) holds (TM1 . i) = (p . (i + n1)) by A1, Th15;

        take TM1;

        thus ( len TM1) = ((m - (n + 1)) - 1) by A4;

        thus ( rng TM1) c= ( rng p) by A4;

        let i be Nat;

        assume i in ( dom TM1);

        

        hence (TM1 . i) = (p . (i + n1)) by A4

        .= (p . ((i + n) + 1));

      end;

    end;

    begin

    theorem :: INTEGR23:16

    

     Th18: for A be non empty closed_interval Subset of REAL , T be Division of A, rho be real-valued Function, B be non empty closed_interval Subset of REAL , S0 be non empty increasing FinSequence of REAL , ST be FinSequence of REAL st B c= A & ( lower_bound B) = ( lower_bound A) & ex S be Division of B st S = S0 & ( len ST) = ( len S) & for j be Nat st j in ( dom S) holds ex p be FinSequence of REAL st (ST . j) = ( Sum p) & ( len p) = ( len T) & for i be Nat st i in ( dom T) holds (p . i) = |.( vol ((( divset (T,i)) /\ ( divset (S,j))),rho)).| holds ex H be Division of B, F be var_volume of rho, H st ( Sum ST) = ( Sum F)

    proof

      let A be non empty closed_interval Subset of REAL , T be Division of A, rho be real-valued Function;

      defpred P[ Nat] means for B be non empty closed_interval Subset of REAL , S0 be non empty increasing FinSequence of REAL , ST be FinSequence of REAL st B c= A & ( lower_bound B) = ( lower_bound A) & ( len S0) = $1 & ex S be Division of B st S = S0 & ( len ST) = ( len S) & for j be Nat st j in ( dom S) holds ex p be FinSequence of REAL st (ST . j) = ( Sum p) & ( len p) = ( len T) & for i be Nat st i in ( dom T) holds (p . i) = |.( vol ((( divset (T,i)) /\ ( divset (S,j))),rho)).| holds ex H be Division of B, F be var_volume of rho, H st ( Sum ST) = ( Sum F);

      

       A1: P[ 0 ];

      

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

      proof

        let k be Nat;

        assume

         A3: P[k];

        let B be non empty closed_interval Subset of REAL , S0 be non empty increasing FinSequence of REAL , ST be FinSequence of REAL ;

        assume

         A4: B c= A & ( lower_bound B) = ( lower_bound A) & ( len S0) = (k + 1) & ex S be Division of B st S = S0 & ( len ST) = ( len S) & for j be Nat st j in ( dom S) holds ex p be FinSequence of REAL st (ST . j) = ( Sum p) & ( len p) = ( len T) & for i be Nat st i in ( dom T) holds (p . i) = |.( vol ((( divset (T,i)) /\ ( divset (S,j))),rho)).|;

        then

        consider S be Division of B such that

         A5: S = S0 & ( len ST) = ( len S) & for j be Nat st j in ( dom S) holds ex p be FinSequence of REAL st (ST . j) = ( Sum p) & ( len p) = ( len T) & for i be Nat st i in ( dom T) holds (p . i) = |.( vol ((( divset (T,i)) /\ ( divset (S,j))),rho)).|;

        

         Z: ( dom ST) = ( dom S) by A5, FINSEQ_3: 29;

        per cases ;

          suppose

           A6: k = 0 ;

          set IDX = { i where i be Nat : i in ( dom T) & (T . i) < ( upper_bound B) };

          IDX c= ( dom T)

          proof

            let x be object;

            assume x in IDX;

            then ex i be Nat st x = i & i in ( dom T) & (T . i) < ( upper_bound B);

            hence thesis;

          end;

          then

          reconsider IDX as finite Subset of NAT by XBOOLE_1: 1;

          

           a: 1 <= ( len T) by NAT_1: 14;

          then

           A7: 1 in ( dom T) by FINSEQ_3: 25;

          ST = <*(ST . 1)*> by A4, A6, FINSEQ_1: 40;

          then

           A8: ( Sum ST) = (ST . 1) by RVSUM_1: 73;

          

           A10: 1 in ( dom S) by A4, A5, A6, FINSEQ_3: 25;

          

           A11: (S . 1) = ( upper_bound B) by A4, A5, A6, INTEGRA1:def 2;

          per cases ;

            suppose

             A12: IDX = {} ;

            set F = the var_volume of rho, S;

            take S, F;

            F = <*(F . 1)*> by A4, A5, A6, FINSEQ_1: 40, INTEGR22:def 2;

            then

             A13: ( Sum F) = (F . 1) by RVSUM_1: 73;

             not 1 in IDX by A12;

            then

             A14: ( upper_bound B) <= (T . 1) by A7;

            

             A15: (F . 1) = |.( vol (( divset (S,1)),rho)).| by A4, A5, A6, FINSEQ_3: 25, INTEGR22:def 2;

            consider p be FinSequence of REAL such that

             A16: (ST . 1) = ( Sum p) & ( len p) = ( len T) & for i be Nat st i in ( dom T) holds (p . i) = |.( vol ((( divset (T,i)) /\ ( divset (S,1))),rho)).| by A4, A5, A6, FINSEQ_3: 25;

            

             Z: ( dom p) = ( dom T) by A16, FINSEQ_3: 29;

            

             A18: (p . 1) = |.( vol ((( divset (T,1)) /\ ( divset (S,1))),rho)).| by FINSEQ_3: 25, a, A16;

            

             A19: ( divset (S,1)) c= B by A4, A5, A6, FINSEQ_3: 25, INTEGRA1: 8;

            

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

            

             A22: ( lower_bound ( divset (T,1))) = ( lower_bound A) & ( upper_bound ( divset (T,1))) = (T . 1) by INTEGRA1:def 4, A7;

             [.( lower_bound B), ( upper_bound B).] c= [.( lower_bound ( divset (T,1))), ( upper_bound ( divset (T,1))).] by A4, A14, A22, XXREAL_1: 34;

            then [.( lower_bound B), ( upper_bound B).] c= ( divset (T,1)) by INTEGRA1: 4;

            then ( divset (S,1)) c= ( divset (T,1)) by A19, A20;

            then

             A23: (p . 1) = |.( vol (( divset (S,1)),rho)).| by A18, XBOOLE_1: 28;

            for i be Nat st i in ( dom p) & i <> 1 holds (p . i) = 0

            proof

              let i be Nat;

              assume

               A24: i in ( dom p) & i <> 1;

              then

               A26: 1 <= i <= ( len p) by FINSEQ_3: 25;

              then 1 < i by A24, XXREAL_0: 1;

              then (1 + 1) <= i by NAT_1: 13;

              then

               A27: (2 - 1) <= (i - 1) by XREAL_1: 9;

              then

              reconsider i1 = (i - 1) as Nat by INT_1: 3, ORDINAL1:def 12;

              (i - 1) <= (( len p) - 0 ) by A26, XREAL_1: 13;

              then i1 in ( dom T) by A16, A27, FINSEQ_3: 25;

              then

               A28: (T . 1) <= (T . (i - 1)) by A7, A27, VALUED_0:def 15;

              

               A29: ( lower_bound ( divset (T,i))) = (T . (i - 1)) & ( upper_bound ( divset (T,i))) = (T . i) by Z, A24, INTEGRA1:def 4;

              ( dom p) = ( dom T) by FINSEQ_3: 29, A16;

              then

               A30: (p . i) = |.( vol ((( divset (T,i)) /\ ( divset (S,1))),rho)).| by A16, A24;

              (( divset (T,i)) /\ ( divset (S,1))) c= (( divset (T,i)) /\ B) by A10, INTEGRA1: 8, XBOOLE_1: 26;

              then

               A31: (( divset (T,i)) /\ ( divset (S,1))) c= ( [.( lower_bound B), ( upper_bound B).] /\ [.( lower_bound ( divset (T,i))), ( upper_bound ( divset (T,i))).]) by A20, INTEGRA1: 4;

              ( [.( lower_bound B), ( upper_bound B).] /\ [.( lower_bound ( divset (T,i))), ( upper_bound ( divset (T,i))).]) c= [.( upper_bound B), ( upper_bound B).] by A14, A28, A29, Th10, XXREAL_0: 2;

              then (( divset (T,i)) /\ ( divset (S,1))) c= [.( upper_bound B), ( upper_bound B).] by A31;

              hence thesis by A30, COMPLEX1: 44, Th11;

            end;

            hence ( Sum ST) = ( Sum F) by A8, A13, A15, A16, a, FINSEQ_3: 25, A23, Th8;

          end;

            suppose

             A32: IDX <> {} ;

            

             A33: ( sup IDX) in IDX by A32, XXREAL_2:def 6;

            then

            reconsider n = ( sup IDX) as Nat;

            

             A34: ex i be Nat st n = i & i in ( dom T) & (T . i) < ( upper_bound B) by A33;

            

             A35: 1 <= n <= ( len T) by A34, FINSEQ_3: 25;

            n <> ( len T)

            proof

              assume n = ( len T);

              then ( upper_bound A) < ( upper_bound B) by A34, INTEGRA1:def 2;

              hence contradiction by A4, XXREAL_2: 59;

            end;

            then n < ( len T) by A35, XXREAL_0: 1;

            then

             A37: 1 <= (n + 1) <= ( len T) by NAT_1: 11, NAT_1: 13;

            then

             A38: (n + 1) in ( dom T) by FINSEQ_3: 25;

            

             A39: ( upper_bound B) <= (T . (n + 1))

            proof

              assume (T . (n + 1)) < ( upper_bound B);

              then (n + 1) in IDX by A38;

              hence contradiction by NAT_1: 16, XXREAL_2: 4;

            end;

            set H = ((T | n) ^ <*( upper_bound B)*>);

            ( upper_bound B) is Element of REAL by XREAL_0:def 1;

            then

             A40: <*( upper_bound B)*> is FinSequence of REAL by FINSEQ_1: 74;

            

             A41: ( len (T | n)) = n by A35, FINSEQ_1: 59;

            ( len <*( upper_bound B)*>) = 1 by FINSEQ_1: 39;

            then

             A42: ( len H) = (n + 1) by A41, FINSEQ_1: 22;

            reconsider H as non empty FinSequence of REAL by A40, FINSEQ_1: 75;

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

            proof

              let e1,e2 be ExtReal;

              assume

               A43: e1 in ( dom H) & e2 in ( dom H) & e1 < e2;

              then

              reconsider i = e1, j = e2 as Nat;

              

               A45: 1 <= i <= (n + 1) & 1 <= j <= (n + 1) by A42, A43, FINSEQ_3: 25;

              per cases ;

                suppose

                 A46: j = (n + 1);

                then

                 A47: (H . e2) = ( upper_bound B) by A41, FINSEQ_1: 42;

                

                 A48: i <= n by A43, A46, NAT_1: 13;

                then

                 A49: i in ( dom (T | n)) by A41, A45, FINSEQ_3: 25;

                

                then

                 A50: (H . e1) = ((T | n) . i) by FINSEQ_1:def 7

                .= (T . i) by A49, FUNCT_1: 47;

                i <= ( len T) by A37, A43, A46, XXREAL_0: 2;

                then i in ( dom T) by A45, FINSEQ_3: 25;

                then (T . i) <= (T . n) by A34, A48, VALUED_0:def 15;

                hence (H . e1) < (H . e2) by A34, A47, A50, XXREAL_0: 2;

              end;

                suppose j <> (n + 1);

                then j < (n + 1) by A45, XXREAL_0: 1;

                then

                 A52: j <= n by NAT_1: 13;

                then

                 A53: j in ( dom (T | n)) by A41, A45, FINSEQ_3: 25;

                

                then

                 A54: (H . e2) = ((T | n) . j) by FINSEQ_1:def 7

                .= (T . j) by A53, FUNCT_1: 47;

                

                 A55: i <= n by A43, A52, XXREAL_0: 2;

                then

                 A56: i in ( dom (T | n)) by A41, A45, FINSEQ_3: 25;

                

                then

                 A57: (H . e1) = ((T | n) . i) by FINSEQ_1:def 7

                .= (T . i) by A56, FUNCT_1: 47;

                i <= ( len T) by A35, A55, XXREAL_0: 2;

                then

                 A58: i in ( dom T) by A45, FINSEQ_3: 25;

                j <= ( len T) by A35, A52, XXREAL_0: 2;

                then j in ( dom T) by A45, FINSEQ_3: 25;

                hence (H . e1) < (H . e2) by A43, A54, A57, A58, VALUED_0:def 13;

              end;

            end;

            then

            reconsider H as non empty increasing FinSequence of REAL by VALUED_0:def 13;

            

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

            

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

            

             A61: (H . ( len H)) = ( upper_bound B) by A41, A42, FINSEQ_1: 42;

            

             A62: ( rng H) = (( rng (T | n)) \/ ( rng <*( upper_bound B)*>)) by FINSEQ_1: 31;

            

             A63: ( rng <*( upper_bound B)*>) = {( upper_bound B)} by FINSEQ_1: 39;

            

             A64: ( rng (T | n)) c= ( rng T) by RELAT_1: 70;

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

            then

             A65: ( rng (T | n)) c= A by A64;

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

            then ( upper_bound B) in B by A59;

            then {( upper_bound B)} c= A by A4, ZFMISC_1: 31;

            then

             A66: ( rng H) c= A by A62, A63, A65, XBOOLE_1: 8;

            for z be object st z in ( rng H) holds z in B

            proof

              let z be object;

              assume

               A67: z in ( rng H);

              then

              reconsider x = z as Real;

              x in A by A66, A67;

              then

               A68: ex r be Real st x = r & ( lower_bound A) <= r & r <= ( upper_bound A) by A60;

              consider i be object such that

               A69: i in ( dom H) & x = (H . i) by A67, FUNCT_1:def 3;

              reconsider i as Nat by A69;

              

               A70: 1 <= i <= ( len H) by A69, FINSEQ_3: 25;

              1 <= ( len H) <= ( len H) by A70, XXREAL_0: 2;

              then ( len H) in ( dom H) by FINSEQ_3: 25;

              then x <= ( upper_bound B) by A61, A69, A70, VALUED_0:def 15;

              hence z in B by A4, A59, A68;

            end;

            then

             A71: ( rng H) c= B;

            reconsider H as Division of B by A61, A71, INTEGRA1:def 2;

            set F = the var_volume of rho, H;

            take H, F;

            

             A72: ( len F) = ( len H) by INTEGR22:def 2;

            ST = <*(ST . 1)*> by A4, A6, FINSEQ_1: 40;

            then

             A73: ( Sum ST) = (ST . 1) by RVSUM_1: 73;

            consider p be FinSequence of REAL such that

             A74: (ST . 1) = ( Sum p) & ( len p) = ( len T) & for i be Nat st i in ( dom T) holds (p . i) = |.( vol ((( divset (T,i)) /\ ( divset (S,1))),rho)).| by A4, A5, A6, FINSEQ_3: 25;

            for i be Nat st i in ( dom p) holds (i <= ( len F) implies (p . i) = (F . i)) & (( len F) < i implies (p . i) = 0 )

            proof

              let i be Nat;

              assume

               A75: i in ( dom p);

              ( dom p) = ( dom T) by A74, FINSEQ_3: 29;

              then

               A76: (p . i) = |.( vol ((( divset (T,i)) /\ ( divset (S,1))),rho)).| by A74, A75;

              

               A77: 1 <= i <= ( len T) by A74, A75, FINSEQ_3: 25;

              

               A78: ( lower_bound ( divset (S,1))) = ( lower_bound B) & ( upper_bound ( divset (S,1))) = (S . 1) by A10, INTEGRA1:def 4;

              

               A79: ( divset (S,1)) = [.( lower_bound B), ( upper_bound B).] by A11, A78, INTEGRA1: 4;

              thus i <= ( len F) implies (p . i) = (F . i)

              proof

                assume i <= ( len F);

                then

                 A80: 1 <= i <= ( len H) by A75, FINSEQ_3: 25, INTEGR22:def 2;

                then

                 A81: i in ( dom H) by FINSEQ_3: 25;

                (( divset (T,i)) /\ ( divset (S,1))) = ( divset (H,i))

                proof

                  per cases ;

                    suppose i <> (n + 1);

                    then i < (n + 1) by A42, A80, XXREAL_0: 1;

                    then

                     A82: i <= n by NAT_1: 13;

                    then

                     A83: i in ( dom (T | n)) by A41, A80, FINSEQ_3: 25;

                    

                    then

                     A84: (H . i) = ((T | n) . i) by FINSEQ_1:def 7

                    .= (T . i) by A83, FUNCT_1: 47;

                    

                     A85: i in ( dom T) by A83, RELAT_1: 57;

                    then (T . i) <= (T . n) by A34, A82, VALUED_0:def 15;

                    then

                     A86: (T . i) <= ( upper_bound B) by A34, XXREAL_0: 2;

                    thus (( divset (T,i)) /\ ( divset (S,1))) = ( divset (H,i))

                    proof

                      per cases ;

                        suppose

                         A87: i = 1;

                        then

                         A88: ( lower_bound ( divset (T,i))) = ( lower_bound A) & ( upper_bound ( divset (T,i))) = (T . i) by A85, INTEGRA1:def 4;

                        

                         A89: ( lower_bound ( divset (H,i))) = ( lower_bound B) & ( upper_bound ( divset (H,i))) = (H . i) by A81, A87, INTEGRA1:def 4;

                        

                         A90: ( divset (T,i)) = [.( lower_bound B), (T . i).] by A4, A88, INTEGRA1: 4;

                        ( divset (H,i)) = [.( lower_bound B), (T . i).] by A84, A89, INTEGRA1: 4

                        .= ( divset (T,i)) by A4, A88, INTEGRA1: 4;

                        hence (( divset (T,i)) /\ ( divset (S,1))) = ( divset (H,i)) by A79, A86, A90, XBOOLE_1: 28, XXREAL_1: 34;

                      end;

                        suppose

                         A91: i <> 1;

                        then

                         A92: ( lower_bound ( divset (T,i))) = (T . (i - 1)) & ( upper_bound ( divset (T,i))) = (T . i) by A85, INTEGRA1:def 4;

                        

                         A93: ( lower_bound ( divset (H,i))) = (H . (i - 1)) & ( upper_bound ( divset (H,i))) = (H . i) by A81, A91, INTEGRA1:def 4;

                        1 < i by A77, A91, XXREAL_0: 1;

                        then

                         A94: (1 - 1) < (i - 1) by XREAL_1: 14;

                        then

                        reconsider i1 = (i - 1) as Nat by INT_1: 3, ORDINAL1:def 12;

                        

                         A95: 1 <= i1 by A94, NAT_1: 14;

                        i1 <= ((n + 1) - 1) by A42, A80, XREAL_1: 13;

                        then

                         A96: (i - 1) in ( dom (T | n)) by A41, A95, FINSEQ_3: 25;

                        

                        then (H . (i - 1)) = ((T | n) . (i - 1)) by FINSEQ_1:def 7

                        .= (T . (i - 1)) by A96, FUNCT_1: 47;

                        then

                         A98: ( divset (H,i)) = [.(T . (i - 1)), (T . i).] by A84, A93, INTEGRA1: 4;

                        

                         A99: ( divset (T,i)) = [.(T . (i - 1)), (T . i).] by A92, INTEGRA1: 4;

                        (i - 1) in ( dom T) by A96, RELAT_1: 57;

                        then (T . (i - 1)) in A by INTEGRA1: 6;

                        then ex r be Real st r = (T . (i - 1)) & ( lower_bound A) <= r & r <= ( upper_bound A) by A60;

                        hence (( divset (T,i)) /\ ( divset (S,1))) = ( divset (H,i)) by A4, A79, A86, A98, A99, XBOOLE_1: 28, XXREAL_1: 34;

                      end;

                    end;

                  end;

                    suppose

                     A100: i = (n + 1);

                    

                     A101: 1 < i by A35, A100, NAT_1: 16;

                    

                     A102: ( lower_bound ( divset (T,i))) = (T . (i - 1)) & ( upper_bound ( divset (T,i))) = (T . i) by A38, A100, A101, INTEGRA1:def 4;

                    

                     A103: ( lower_bound ( divset (H,i))) = (H . (i - 1)) & ( upper_bound ( divset (H,i))) = (H . i) by A81, A101, INTEGRA1:def 4;

                    reconsider i1 = (i - 1) as Nat by A100;

                    

                     A104: (i - 1) in ( dom (T | n)) by A35, A41, A100, FINSEQ_3: 25;

                    

                    then

                     A105: (H . (i - 1)) = ((T | n) . (i - 1)) by FINSEQ_1:def 7

                    .= (T . (i - 1)) by A104, FUNCT_1: 47;

                    (T . (i - 1)) in A by A34, A100, INTEGRA1: 6;

                    then

                     A106: ex r be Real st r = (T . (i - 1)) & ( lower_bound A) <= r & r <= ( upper_bound A) by A60;

                    

                    thus (( divset (T,i)) /\ ( divset (S,1))) = ( [.(T . (i - 1)), (T . i).] /\ [.( lower_bound B), ( upper_bound B).]) by A79, A102, INTEGRA1: 4

                    .= [.(T . (i - 1)), ( upper_bound B).] by A4, A39, A100, A106, XXREAL_1: 143

                    .= [.(H . (i - 1)), (H . i).] by A41, A100, A105, FINSEQ_1: 42

                    .= ( divset (H,i)) by A103, INTEGRA1: 4;

                  end;

                end;

                hence thesis by A76, A81, INTEGR22:def 2;

              end;

              thus ( len F) < i implies (p . i) = 0

              proof

                assume

                 A107: ( len F) < i;

                then

                 A108: ( len H) < i by INTEGR22:def 2;

                

                 A109: 1 <= (n + 1) by NAT_1: 11;

                i in ( dom T) by A75, A74, FINSEQ_3: 29;

                then ( lower_bound ( divset (T,i))) = (T . (i - 1)) & ( upper_bound ( divset (T,i))) = (T . i) by A42, A72, A107, A109, INTEGRA1:def 4;

                then

                 A110: ( divset (T,i)) = [.(T . (i - 1)), (T . i).] by INTEGRA1: 4;

                ((n + 1) + 1) <= i by A42, A108, NAT_1: 13;

                then

                 A111: (((n + 1) + 1) - 1) <= (i - 1) by XREAL_1: 9;

                1 <= (n + 1) by NAT_1: 11;

                then

                 A112: 1 <= (i - 1) by A111, XXREAL_0: 2;

                reconsider i1 = (i - 1) as Nat by A111, INT_1: 3, ORDINAL1:def 12;

                (i - 1) <= (i - 0 ) by XREAL_1: 13;

                then (i - 1) <= ( len T) by A77, XXREAL_0: 2;

                then i1 in ( dom T) by A112, FINSEQ_3: 25;

                then (T . (n + 1)) <= (T . i1) by A38, A111, VALUED_0:def 15;

                then (( divset (T,i)) /\ ( divset (S,1))) c= [.( upper_bound B), ( upper_bound B).] by A39, A79, A110, Th10, XXREAL_0: 2;

                hence (p . i) = 0 by A76, COMPLEX1: 44, Th11;

              end;

            end;

            hence ( Sum ST) = ( Sum F) by A37, A42, A72, A73, A74, Th9;

          end;

        end;

          suppose

           A114: k <> 0 ;

          set S01 = (S0 | k);

          

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

          

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

          

           A117: k = ( len S01) by A4, FINSEQ_1: 59, NAT_1: 11;

          ( dom S0) = ( Seg (k + 1)) by A4, FINSEQ_1:def 3;

          then

           A118: ( Seg k) c= ( dom S0) by FINSEQ_1: 5, NAT_1: 11;

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

          proof

            let e1,e2 be ExtReal;

            assume

             A119: e1 in ( dom S01) & e2 in ( dom S01) & e1 < e2;

            then

             A120: e1 in ( Seg k) & e2 in ( Seg k) by A117, FINSEQ_1:def 3;

            then (S01 . e1) = (S0 . e1) & (S01 . e2) = (S0 . e2) by FUNCT_1: 49;

            hence thesis by A118, A119, A120, VALUED_0:def 13;

          end;

          then

          reconsider S01 as non empty increasing FinSequence of REAL by A114, VALUED_0:def 13;

          

           A121: k in ( dom S0) by A114, A118, FINSEQ_1: 3;

          then

          consider B1,B2 be non empty closed_interval Subset of REAL such that

           A122: B1 = [.( lower_bound B), (S0 . k).] & B2 = [.(S0 . k), ( upper_bound B).] & B = (B1 \/ B2) by A5, INTEGRA1: 32;

          

           A123: B1 c= B by A122, XBOOLE_1: 7;

          then

           A124: B1 c= A by A4;

          

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

          then

           A126: ( upper_bound B1) = (S . k) by A5, A122, INTEGRA1: 5;

          

           A127: ( lower_bound B1) = ( lower_bound A) by A4, A122, A125, INTEGRA1: 5;

          

           A128: ( rng S0) c= B by A5, INTEGRA1:def 2;

          

           A129: ( rng S01) c= ( rng S0) by RELAT_1: 70;

          for y be object st y in ( rng S01) holds y in B1

          proof

            let y be object;

            assume

             A130: y in ( rng S01);

            then y in B by A128, A129;

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

            then

            consider y1 be Real such that

             A131: y = y1 & ( lower_bound B) <= y1 & y1 <= ( upper_bound B);

            consider x be object such that

             A132: x in ( dom S01) & y1 = (S01 . x) by A130, A131, FUNCT_1:def 3;

            reconsider x as Nat by A132;

            

             A133: x in ( Seg k) by A117, A132, FINSEQ_1:def 3;

            then

             A134: x <= k by FINSEQ_1: 1;

            now

              assume x <> k;

              then x < k by A134, XXREAL_0: 1;

              hence (S0 . x) <= (S0 . k) by A118, A121, A133, VALUED_0:def 13;

            end;

            then y1 <= (S0 . k) by A132, A133, FUNCT_1: 49;

            hence y in B1 by A122, A131;

          end;

          then

           A135: ( rng S01) c= B1;

          

           A136: (S01 . k) = (S0 . k) by A114, FINSEQ_1: 3, FUNCT_1: 49;

          

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

          then (S01 . ( len S01)) = ( upper_bound B1) by A117, A122, A136, INTEGRA1: 5;

          then

          reconsider S1 = S01 as Division of B1 by A135, INTEGRA1:def 2;

          reconsider ST1 = (ST | k) as FinSequence of REAL ;

          

           A138: ( len S1) = k by A4, FINSEQ_1: 59, NAT_1: 11;

          

           A139: ( len ST1) = ( len S1) by A4, A138, FINSEQ_1: 59, NAT_1: 11;

          for j be Nat st j in ( dom S1) holds ex p be FinSequence of REAL st (ST1 . j) = ( Sum p) & ( len p) = ( len T) & for i be Nat st i in ( dom T) holds (p . i) = |.( vol ((( divset (T,i)) /\ ( divset (S1,j))),rho)).|

          proof

            let j be Nat;

            assume

             A140: j in ( dom S1);

            then

             A141: j in ( Seg k) & j in ( dom S0) by RELAT_1: 57;

            then

            consider p be FinSequence of REAL such that

             A142: (ST . j) = ( Sum p) & ( len p) = ( len T) & for i be Nat st i in ( dom T) holds (p . i) = |.( vol ((( divset (T,i)) /\ ( divset (S,j))),rho)).| by A5;

            

             A143: for i be Nat st i in ( dom T) holds (p . i) = |.( vol ((( divset (T,i)) /\ ( divset (S1,j))),rho)).|

            proof

              let i be Nat;

              assume

               A144: i in ( dom T);

              

               A145: ( divset (S,j)) = [.( lower_bound ( divset (S,j))), ( upper_bound ( divset (S,j))).] & ( divset (S1,j)) = [.( lower_bound ( divset (S1,j))), ( upper_bound ( divset (S1,j))).] by INTEGRA1: 4;

              ( divset (S,j)) = ( divset (S1,j))

              proof

                per cases ;

                  suppose j = 1;

                  then

                   A146: ( lower_bound ( divset (S,j))) = ( lower_bound B) & ( upper_bound ( divset (S,j))) = (S . j) & ( lower_bound ( divset (S1,j))) = ( lower_bound B1) & ( upper_bound ( divset (S1,j))) = (S1 . j) by A5, A140, A141, INTEGRA1:def 4;

                  ( lower_bound B) = ( lower_bound B1) by A122, A137, INTEGRA1: 5;

                  hence ( divset (S,j)) = ( divset (S1,j)) by A5, A140, A145, A146, FUNCT_1: 47;

                end;

                  suppose

                   A147: j <> 1;

                  then

                   A148: ( lower_bound ( divset (S,j))) = (S . (j - 1)) & ( upper_bound ( divset (S,j))) = (S . j) & ( lower_bound ( divset (S1,j))) = (S1 . (j - 1)) & ( upper_bound ( divset (S1,j))) = (S1 . j) by A5, A140, A141, INTEGRA1:def 4;

                  

                   A149: 1 <= j by A141, FINSEQ_1: 1;

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

                  then

                  reconsider j1 = (j - 1) as Nat;

                  1 < j by A147, A149, XXREAL_0: 1;

                  then (S . j1) = (S1 . j1) by A5, A141, FINSEQ_3: 12, FUNCT_1: 49;

                  hence ( divset (S,j)) = ( divset (S1,j)) by A5, A140, A145, A148, FUNCT_1: 47;

                end;

              end;

              hence (p . i) = |.( vol ((( divset (T,i)) /\ ( divset (S1,j))),rho)).| by A142, A144;

            end;

            take p;

            thus thesis by A141, A142, A143, FUNCT_1: 49;

          end;

          then

          consider H1 be Division of B1, F1 be var_volume of rho, H1 such that

           A150: ( Sum ST1) = ( Sum F1) by A3, A124, A127, A138, A139;

          

           A151: 1 <= (k + 1) <= ( len ST) by A4, NAT_1: 11;

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

          then

           A152: ST = (ST1 ^ <*(ST . (k + 1))*>) by A151, FINSEQ_4: 15;

          ( dom ST) = ( Seg (k + 1)) by A4, FINSEQ_1:def 3;

          then

          consider p be FinSequence of REAL such that

           A153: (ST . (k + 1)) = ( Sum p) & ( len p) = ( len T) & for i be Nat st i in ( dom T) holds (p . i) = |.( vol ((( divset (T,i)) /\ ( divset (S,(k + 1)))),rho)).| by Z, A5, FINSEQ_1: 4;

          set JDX = { i where i be Nat : i in ( dom T) & ( upper_bound B) <= (T . i) };

          JDX c= ( dom T)

          proof

            let x be object;

            assume x in JDX;

            then ex i be Nat st x = i & i in ( dom T) & ( upper_bound B) <= (T . i);

            hence thesis;

          end;

          then

          reconsider JDX as finite Subset of NAT by XBOOLE_1: 1;

          

           H: ( dom p) = ( dom T) by FINSEQ_3: 29, A153;

          

           A154: ( upper_bound B) <= ( upper_bound A) by A4, XXREAL_2: 59;

          

           A155: (T . ( len T)) = ( upper_bound A) by INTEGRA1:def 2;

          

           A156: 1 <= ( len T) by NAT_1: 14;

          then

           A157: 1 in ( dom T) by FINSEQ_3: 25;

          reconsider m = ( min* JDX) as Nat;

          

           A159: (S . ( len S)) = ( upper_bound B) by INTEGRA1:def 2;

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

          then ( len T) in JDX by A154, A155;

          then m in JDX by NAT_1:def 1;

          then

          consider i be Nat such that

           A160: m = i & i in ( dom T) & ( upper_bound B) <= (T . i);

          

           A161: 1 <= k by A114, NAT_1: 14;

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

          then k in ( Seg (k + 1)) by A161;

          then

           A162: k in ( dom S) by A4, A5, FINSEQ_1:def 3;

          then (S . k) in B by INTEGRA1: 6;

          then

           A163: ex r be Real st r = (S . k) & ( lower_bound B) <= r & r <= ( upper_bound B) by A115;

          

           A164: for i be Nat st m <= i & i in ( dom T) holds ( upper_bound B) <= (T . i)

          proof

            let i be Nat;

            assume m <= i & i in ( dom T);

            then (T . m) <= (T . i) by A160, VALUED_0:def 15;

            hence thesis by A160, XXREAL_0: 2;

          end;

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

          then

           A167: (k + 1) in ( dom S) by A4, A5, FINSEQ_1:def 3;

          (S . k) < (S . (k + 1)) by A162, A167, NAT_1: 16, VALUED_0:def 13;

          then

           A168: (S . k) < ( upper_bound B) by A4, A5, INTEGRA1:def 2;

          

           A169: ( divset (S,(k + 1))) = [.( lower_bound ( divset (S,(k + 1)))), ( upper_bound ( divset (S,(k + 1)))).] by INTEGRA1: 4;

          (k + 1) <> 1 by A114;

          then

           A170: ( lower_bound ( divset (S,(k + 1)))) = (S . ((k + 1) - 1)) & ( upper_bound ( divset (S,(k + 1)))) = (S . (k + 1)) by A167, INTEGRA1:def 4;

          

           A171: (S . (k + 1)) = ( upper_bound B) by A4, A5, INTEGRA1:def 2;

          per cases ;

            suppose

             A172: m = 1;

            set H = (H1 ^ <*( upper_bound B)*>);

            

             A173: ( upper_bound B) <= (T . 1) by A156, A164, A172, FINSEQ_3: 25;

            ( upper_bound B) is Element of REAL by XREAL_0:def 1;

            then

             A174: <*( upper_bound B)*> is FinSequence of REAL by FINSEQ_1: 74;

            

             A175: ( len <*( upper_bound B)*>) = 1 by FINSEQ_1: 39;

            then

             A176: ( len H) = (( len H1) + 1) by FINSEQ_1: 22;

            reconsider H as non empty FinSequence of REAL by A174, FINSEQ_1: 75;

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

            proof

              let e1,e2 be ExtReal;

              assume

               A177: e1 in ( dom H) & e2 in ( dom H) & e1 < e2;

              then

               A178: e1 in ( Seg ( len H)) & e2 in ( Seg ( len H)) by FINSEQ_1:def 3;

              reconsider i = e1, j = e2 as Nat by A177;

              

               A179: 1 <= i & i <= (( len H1) + 1) & 1 <= j & j <= (( len H1) + 1) by A176, A178, FINSEQ_1: 1;

              per cases ;

                suppose

                 A180: j = (( len H1) + 1);

                then

                 A181: (H . e2) = ( upper_bound B) by FINSEQ_1: 42;

                i <= ( len H1) by A177, A180, NAT_1: 13;

                then

                 A182: i in ( dom H1) by A179, FINSEQ_3: 25;

                then

                 A183: (H . e1) = (H1 . i) by FINSEQ_1:def 7;

                (H1 . i) in [.( lower_bound B), (S0 . k).] by A122, A182, INTEGRA1: 6;

                then ex r be Real st r = (H1 . i) & ( lower_bound B) <= r & r <= (S0 . k);

                hence (H . e1) < (H . e2) by A5, A168, A181, A183, XXREAL_0: 2;

              end;

                suppose j <> (( len H1) + 1);

                then j < (( len H1) + 1) by A179, XXREAL_0: 1;

                then

                 A184: j <= ( len H1) by NAT_1: 13;

                then

                 A185: j in ( dom H1) by A179, FINSEQ_3: 25;

                then

                 A186: (H . e2) = (H1 . j) by FINSEQ_1:def 7;

                i <= ( len H1) by A177, A184, XXREAL_0: 2;

                then

                 A187: i in ( dom H1) by A179, FINSEQ_3: 25;

                then (H . e1) = (H1 . i) by FINSEQ_1:def 7;

                hence (H . e1) < (H . e2) by A177, A185, A186, A187, VALUED_0:def 13;

              end;

            end;

            then

            reconsider H as non empty increasing FinSequence of REAL by VALUED_0:def 13;

            

             A188: (H . ( len H)) = ( upper_bound B) by A176, FINSEQ_1: 42;

            ( rng H1) c= B1 by INTEGRA1:def 2;

            then

             A189: ( rng H1) c= B by A123;

            

             A190: ( rng H) = (( rng H1) \/ ( rng <*( upper_bound B)*>)) by FINSEQ_1: 31;

            

             A191: ( rng <*( upper_bound B)*>) = {( upper_bound B)} by FINSEQ_1: 39;

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

            then ( upper_bound B) in B by A115;

            then ( rng <*( upper_bound B)*>) c= B by A191, ZFMISC_1: 31;

            then

            reconsider H as Division of B by A188, A189, A190, INTEGRA1:def 2, XBOOLE_1: 8;

            set F = (F1 ^ <* |.( vol ( [.(S . k), ( upper_bound B).],rho)).|*>);

             |.( vol ( [.(S . k), ( upper_bound B).],rho)).| is Element of REAL by XREAL_0:def 1;

            then

             A192: <* |.( vol ( [.(S . k), ( upper_bound B).],rho)).|*> is FinSequence of REAL by FINSEQ_1: 74;

            reconsider F as FinSequence of REAL by A192, FINSEQ_1: 75;

            

             A193: ( len F) = (( len F1) + ( len <* |.( vol ( [.(S . k), ( upper_bound B).],rho)).|*>)) by FINSEQ_1: 22

            .= (( len H1) + ( len <* |.( vol ( [.(S . k), ( upper_bound B).],rho)).|*>)) by INTEGR22:def 2

            .= (( len H1) + 1) by FINSEQ_1: 40

            .= ( len H) by A175, FINSEQ_1: 22;

            1 <= ( len H1) by NAT_1: 14;

            then

             A194: 1 in ( dom H1) by FINSEQ_3: 25;

            

             A195: ( len F1) = ( len H1) by INTEGR22:def 2;

            then

             A196: ( dom F1) = ( dom H1) by FINSEQ_3: 29;

            for j be Nat st j in ( dom H) holds (F . j) = |.( vol (( divset (H,j)),rho)).|

            proof

              let j be Nat;

              

               A197: ( divset (H,j)) = [.( lower_bound ( divset (H,j))), ( upper_bound ( divset (H,j))).] & ( divset (H1,j)) = [.( lower_bound ( divset (H1,j))), ( upper_bound ( divset (H1,j))).] by INTEGRA1: 4;

              assume

               A198: j in ( dom H);

              then

               A199: 1 <= j <= ( len H) by FINSEQ_3: 25;

              per cases ;

                suppose

                 A200: j = 1;

                then

                 A201: ( lower_bound ( divset (H,j))) = ( lower_bound B) & ( upper_bound ( divset (H,j))) = (H . j) by A198, INTEGRA1:def 4;

                

                 A203: ( lower_bound ( divset (H1,j))) = ( lower_bound B1) & ( upper_bound ( divset (H1,j))) = (H1 . j) by A194, A200, INTEGRA1:def 4;

                

                 A204: ( lower_bound B) = ( lower_bound B1) by A122, A137, INTEGRA1: 5;

                

                thus (F . j) = (F1 . j) by A196, A194, A200, FINSEQ_1:def 7

                .= |.( vol (( divset (H1,j)),rho)).| by A200, A194, INTEGR22:def 2

                .= |.( vol (( divset (H,j)),rho)).| by A197, A201, A200, A194, A203, A204, FINSEQ_1:def 7;

              end;

                suppose

                 A205: j <> 1;

                per cases ;

                  suppose

                   A206: j = ( len H);

                  then

                   A207: j = (( len H1) + 1) by A175, FINSEQ_1: 22;

                  

                   A208: (F . j) = |.( vol ( [.(S . k), ( upper_bound B).],rho)).| by A176, A195, A206, FINSEQ_1: 42;

                  

                   A209: ( lower_bound ( divset (H,j))) = (H . (j - 1)) & ( upper_bound ( divset (H,j))) = (H . j) by A198, A205, INTEGRA1:def 4;

                  (j - 1) in NAT by A198, INT_1: 5, FINSEQ_3: 25;

                  then

                  reconsider j1 = (j - 1) as Nat;

                  1 < j by A199, A205, XXREAL_0: 1;

                  then (1 - 1) < j1 by XREAL_1: 14;

                  then

                   A210: 1 <= j1 by NAT_1: 14;

                  (j - 1) in ( dom H1) by A207, A210, FINSEQ_3: 25;

                  

                  then (H . (j - 1)) = (H1 . ( len H1)) by A207, FINSEQ_1:def 7

                  .= (S . k) by A126, INTEGRA1:def 2;

                  hence (F . j) = |.( vol (( divset (H,j)),rho)).| by A197, A206, A208, A209, INTEGRA1:def 2;

                end;

                  suppose j <> ( len H);

                  then j < (( len H1) + 1) by A176, A199, XXREAL_0: 1;

                  then

                   L: j <= ( len H1) by NAT_1: 13;

                  then

                   A211: j in ( Seg ( len H1)) by A199;

                  

                   A212: j in ( dom H1) by A199, L, FINSEQ_3: 25;

                  then

                   A213: (H . j) = (H1 . j) by FINSEQ_1:def 7;

                  (j - 1) in NAT by A198, FINSEQ_3: 25, INT_1: 5;

                  then

                  reconsider j1 = (j - 1) as Nat;

                  1 < j by A199, A205, XXREAL_0: 1;

                  then (j - 1) in ( Seg ( len H1)) by A211, FINSEQ_3: 12;

                  then (j - 1) in ( dom H1) by FINSEQ_1:def 3;

                  then

                   A214: (H . j1) = (H1 . j1) by FINSEQ_1:def 7;

                  

                   A215: ( lower_bound ( divset (H,j))) = (H . (j - 1)) & ( upper_bound ( divset (H,j))) = (H . j) by A198, A205, INTEGRA1:def 4;

                  

                  thus (F . j) = (F1 . j) by A196, A212, FINSEQ_1:def 7

                  .= |.( vol (( divset (H1,j)),rho)).| by A212, INTEGR22:def 2

                  .= |.( vol (( divset (H,j)),rho)).| by A205, A212, A213, A214, A215, INTEGRA1:def 4;

                end;

              end;

            end;

            then

            reconsider F as var_volume of rho, H by A193, INTEGR22:def 2;

            take H, F;

            

             A217: (p . 1) = |.( vol ((( divset (T,1)) /\ ( divset (S,(k + 1)))),rho)).| by A156, FINSEQ_3: 25, A153;

            

             A218: ( divset (S,(k + 1))) c= B by A167, INTEGRA1: 8;

            

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

            

             A221: ( lower_bound ( divset (T,1))) = ( lower_bound A) & ( upper_bound ( divset (T,1))) = (T . 1) by INTEGRA1:def 4, A157;

             [.( lower_bound B), ( upper_bound B).] c= [.( lower_bound ( divset (T,1))), ( upper_bound ( divset (T,1))).] by A4, A173, A221, XXREAL_1: 34;

            then [.( lower_bound B), ( upper_bound B).] c= ( divset (T,1)) by INTEGRA1: 4;

            then ( divset (S,(k + 1))) c= ( divset (T,1)) by A218, A219;

            then

             A222: (p . 1) = |.( vol (( divset (S,(k + 1))),rho)).| by A217, XBOOLE_1: 28;

            for i be Nat st i in ( dom p) & i <> 1 holds (p . i) = 0

            proof

              let i be Nat;

              assume

               A223: i in ( dom p) & i <> 1;

              then

               A225: 1 <= i <= ( len p) by FINSEQ_3: 25;

              then 1 < i by A223, XXREAL_0: 1;

              then (1 + 1) <= i by NAT_1: 13;

              then

               A226: (2 - 1) <= (i - 1) by XREAL_1: 9;

              then

              reconsider i1 = (i - 1) as Nat by INT_1: 3, ORDINAL1:def 12;

              (i - 1) <= (( len p) - 0 ) by A225, XREAL_1: 13;

              then i1 in ( dom T) by A226, FINSEQ_3: 25, A153;

              then

               A227: (T . 1) <= (T . (i - 1)) by A157, A226, VALUED_0:def 15;

              

               A228: ( lower_bound ( divset (T,i))) = (T . (i - 1)) & ( upper_bound ( divset (T,i))) = (T . i) by INTEGRA1:def 4, A223, H;

              

               A229: (p . i) = |.( vol ((( divset (T,i)) /\ ( divset (S,(k + 1)))),rho)).| by A153, A223, H;

              (( divset (T,i)) /\ ( divset (S,(k + 1)))) c= (( divset (T,i)) /\ B) by A167, INTEGRA1: 8, XBOOLE_1: 26;

              then

               A230: (( divset (T,i)) /\ ( divset (S,(k + 1)))) c= ( [.( lower_bound B), ( upper_bound B).] /\ [.( lower_bound ( divset (T,i))), ( upper_bound ( divset (T,i))).]) by A219, INTEGRA1: 4;

              ( [.( lower_bound B), ( upper_bound B).] /\ [.( lower_bound ( divset (T,i))), ( upper_bound ( divset (T,i))).]) c= [.( upper_bound B), ( upper_bound B).] by A173, A227, A228, Th10, XXREAL_0: 2;

              then (( divset (T,i)) /\ ( divset (S,(k + 1)))) c= [.( upper_bound B), ( upper_bound B).] by A230;

              hence thesis by A229, COMPLEX1: 44, Th11;

            end;

            

            then

             A231: ( Sum p) = |.( vol (( divset (S,(k + 1))),rho)).| by A153, A156, A222, Th8, FINSEQ_3: 25

            .= |.( vol ( [.(S . k), ( upper_bound B).],rho)).| by A4, A5, A159, A170, INTEGRA1: 4;

            

            thus ( Sum ST) = (( Sum F1) + ( Sum p)) by A150, A152, A153, RVSUM_1: 74

            .= ( Sum F) by A231, RVSUM_1: 74;

          end;

            suppose

             A232: m <> 1;

            

             S: m in ( Seg ( len T)) by A160, FINSEQ_1:def 3;

            

             A233: 1 <= m <= ( len T) by A160, FINSEQ_3: 25;

            then 1 < m by A232, XXREAL_0: 1;

            then

             a234: (m - 1) in ( Seg ( len T)) by FINSEQ_3: 12, S;

            then

             A234: (m - 1) in ( dom T) by FINSEQ_1:def 3;

            then

             A235: 1 <= (m - 1) <= ( len T) by FINSEQ_3: 25;

            reconsider m1 = (m - 1) as Nat by a234;

            

             LL: m1 in ( dom T) by a234, FINSEQ_1:def 3;

            set IDX = { i where i be Nat : i in ( dom T) & (T . i) <= (S . k) };

            IDX c= ( dom T)

            proof

              let x be object;

              assume x in IDX;

              then ex i be Nat st x = i & i in ( dom T) & (T . i) <= (S . k);

              hence thesis;

            end;

            then

            reconsider IDX as finite Subset of NAT by XBOOLE_1: 1;

            per cases ;

              suppose

               A237: IDX = {} ;

              

               A238: for i be Nat st i in ( dom T) holds (S . k) < (T . i)

              proof

                assume not for i be Nat st i in ( dom T) holds (S . k) < (T . i);

                then

                consider i be Nat such that

                 A239: i in ( dom T) & not (S . k) < (T . i);

                i in IDX by A239;

                hence contradiction by A237;

              end;

              reconsider TM1 = (T | m1) as non empty increasing FinSequence of REAL by Th12, LL;

              

               A240: ( len TM1) = m1 by A235, FINSEQ_1: 59;

              then

               a240: ( dom TM1) = ( Seg m1) by FINSEQ_1:def 3;

              then

               A242: (TM1 . ( len TM1)) = (T . m1) by FUNCT_1: 49, A240, FINSEQ_3: 25, A235;

              

               A243: (T . m1) < ( upper_bound B)

              proof

                assume not (T . m1) < ( upper_bound B);

                then

                 A245: m1 in JDX by A234;

                (m - 1) < (m - 0 ) by XREAL_1: 15;

                hence contradiction by A245, NAT_1:def 1;

              end;

              then

              reconsider TM1B = (TM1 ^ <*( upper_bound B)*>) as non empty increasing FinSequence of REAL by A242, Th14;

              

               A246: (H1 . ( len H1)) = (S . k) by A126, INTEGRA1:def 2;

              1 in ( Seg ( len TM1)) by A235, A240;

              then

               A248: (TM1 . 1) = (T . 1) by A240, FUNCT_1: 49;

              1 in ( dom TM1) by A235, A240, FINSEQ_3: 25;

              then

               A249: (TM1B . 1) = (T . 1) by A248, FINSEQ_1:def 7;

              reconsider H = (H1 ^ TM1B) as non empty increasing FinSequence of REAL by A157, A238, A246, A249, Th13;

              

               A250: ( rng TM1B) = (( rng TM1) \/ ( rng <*( upper_bound B)*>)) by FINSEQ_1: 31;

              

               A251: ( rng <*( upper_bound B)*>) = {( upper_bound B)} by FINSEQ_1: 39;

              

               A256: ( rng TM1) c= B

              proof

                let z be object;

                assume

                 A252: z in ( rng TM1);

                then

                reconsider x = z as Real;

                x in ( rng T) by A252, RELAT_1: 70, TARSKI:def 3;

                then x in A by INTEGRA1:def 2, TARSKI:def 3;

                then

                 A253: ex r be Real st x = r & ( lower_bound A) <= r & r <= ( upper_bound A) by A116;

                consider i be object such that

                 A254: i in ( dom TM1) & x = (TM1 . i) by A252, FUNCT_1:def 3;

                reconsider i as Nat by A254;

                

                 A255: 1 <= i <= ( len TM1) by FINSEQ_3: 25, A254;

                1 <= ( len TM1) by A255, XXREAL_0: 2;

                then ( len TM1) in ( dom TM1) by FINSEQ_3: 25;

                then (TM1 . i) <= (TM1 . ( len TM1)) by A254, A255, VALUED_0:def 15;

                then x <= ( upper_bound B) by A242, A243, A254, XXREAL_0: 2;

                hence z in B by A4, A115, A253;

              end;

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

              then ( upper_bound B) in B by A115;

              then {( upper_bound B)} c= B by ZFMISC_1: 31;

              then

               A257: ( rng TM1B) c= B by A250, A251, A256, XBOOLE_1: 8;

              ( rng H1) c= B1 by INTEGRA1:def 2;

              then ( rng H1) c= B by A123;

              then (( rng H1) \/ ( rng TM1B)) c= B by A257, XBOOLE_1: 8;

              then

               A258: ( rng H) c= B by FINSEQ_1: 31;

              

               A259: ( len TM1B) = (( len TM1) + ( len <*( upper_bound B)*>)) by FINSEQ_1: 22

              .= (( len TM1) + 1) by FINSEQ_1: 40;

              (( len TM1) + 1) in ( Seg (( len TM1) + 1)) by FINSEQ_1: 4;

              then

               A260: (( len TM1) + 1) in ( dom TM1B) by A259, FINSEQ_1:def 3;

              

               A261: ( len H) = (( len H1) + (( len TM1) + 1)) by A259, FINSEQ_1: 22;

              

               X: 1 in ( Seg 1);

              then

               A262: 1 in ( dom <*( upper_bound B)*>) by FINSEQ_1: 38;

              (H . ( len H)) = (TM1B . (( len TM1) + 1)) by A260, A261, FINSEQ_1:def 7

              .= ( <*( upper_bound B)*> . 1) by A262, FINSEQ_1:def 7

              .= ( upper_bound B) by FINSEQ_1: 40;

              then

              reconsider H as Division of B by A258, INTEGRA1:def 2;

              set q = ((p | m1) ^ <* |.( vol ( [.(T . m1), ( upper_bound B).],rho)).|*>);

              ( rng q) c= REAL ;

              then

              reconsider q as FinSequence of REAL by FINSEQ_1:def 4;

              

               A263: ( len (p | m1)) = m1 by A153, A235, FINSEQ_1: 59;

              

               A264: ( len q) = (( len (p | m1)) + ( len <* |.( vol ( [.(T . m1), ( upper_bound B).],rho)).|*>)) by FINSEQ_1: 22

              .= (m1 + 1) by A263, FINSEQ_1: 40

              .= m;

              

               A265: 1 in ( dom <* |.( vol ( [.(T . m1), ( upper_bound B).],rho)).|*>) by FINSEQ_1: 38, X;

              

               A266: (q . m) = (q . (m1 + 1))

              .= ( <* |.( vol ( [.(T . m1), ( upper_bound B).],rho)).|*> . 1) by A263, A265, FINSEQ_1:def 7

              .= |.( vol ( [.(T . m1), ( upper_bound B).],rho)).| by FINSEQ_1: 40;

              

               A267: for i be Nat st 1 <= i & i <= m1 holds (q . i) = |.( vol ((( divset (T,i)) /\ ( divset (S,(k + 1)))),rho)).|

              proof

                let i be Nat;

                assume

                 A268: 1 <= i <= m1;

                then

                 A269: i in ( Seg m1);

                then

                 A270: i in ( dom (p | m1)) by A263, FINSEQ_1:def 3;

                

                 C: i <= ( len T) by A235, A268, XXREAL_0: 2;

                

                thus (q . i) = ((p | m1) . i) by A270, FINSEQ_1:def 7

                .= (p . i) by A269, FUNCT_1: 49

                .= |.( vol ((( divset (T,i)) /\ ( divset (S,(k + 1)))),rho)).| by A153, C, FINSEQ_3: 25, A268;

              end;

              reconsider F = (F1 ^ q) as FinSequence of REAL ;

              

               A272: ( Sum F) = (( Sum F1) + ( Sum q)) by RVSUM_1: 75;

              

               A273: ( len F) = (( len F1) + ( len q)) by FINSEQ_1: 22;

              

               A274: ( len H) = ((( len H1) + m1) + 1) by A240, A261;

              

               A275: 1 <= ( len H1) by NAT_1: 14;

              then

               A276: 1 in ( dom H1) by FINSEQ_3: 25;

              

               A277: ( len F1) = ( len H1) by INTEGR22:def 2;

              then

               A278: ( dom F1) = ( dom H1) by FINSEQ_3: 29;

              (m - 1) <= (m - 0 ) by XREAL_1: 15;

              then 1 <= m by A235, XXREAL_0: 2;

              then

               A279: m in ( dom q) by A264, FINSEQ_3: 25;

              for j be Nat st j in ( dom H) holds (F . j) = |.( vol (( divset (H,j)),rho)).|

              proof

                let j be Nat;

                

                 A280: ( divset (H,j)) = [.( lower_bound ( divset (H,j))), ( upper_bound ( divset (H,j))).] & ( divset (H1,j)) = [.( lower_bound ( divset (H1,j))), ( upper_bound ( divset (H1,j))).] by INTEGRA1: 4;

                assume

                 A281: j in ( dom H);

                then

                 A282: 1 <= j <= ( len H) by FINSEQ_3: 25;

                per cases ;

                  suppose

                   A283: j = 1;

                  then

                   A284: ( lower_bound ( divset (H,j))) = ( lower_bound B) & ( upper_bound ( divset (H,j))) = (H . j) by A281, INTEGRA1:def 4;

                  

                   A285: j in ( dom H1) by A275, A283, FINSEQ_3: 25;

                  then

                   A286: ( lower_bound ( divset (H1,j))) = ( lower_bound B1) & ( upper_bound ( divset (H1,j))) = (H1 . j) by A283, INTEGRA1:def 4;

                  

                   A287: ( lower_bound B) = ( lower_bound B1) by A122, A137, INTEGRA1: 5;

                  

                  thus (F . j) = (F1 . j) by A278, A276, A283, FINSEQ_1:def 7

                  .= |.( vol (( divset (H1,j)),rho)).| by A285, INTEGR22:def 2

                  .= |.( vol (( divset (H,j)),rho)).| by A280, A284, A285, A286, A287, FINSEQ_1:def 7;

                end;

                  suppose

                   A288: j <> 1;

                  per cases ;

                    suppose

                     A289: j = ( len H);

                    

                     A290: (F . j) = |.( vol ( [.(T . m1), ( upper_bound B).],rho)).| by A240, A261, A266, A277, A279, A289, FINSEQ_1:def 7;

                    

                     A291: ( lower_bound ( divset (H,j))) = (H . (j - 1)) & ( upper_bound ( divset (H,j))) = (H . j) by A281, A288, INTEGRA1:def 4;

                    (j - 1) in NAT by A281, INT_1: 5, FINSEQ_3: 25;

                    then

                    reconsider j1 = (j - 1) as Nat;

                    (m - 1) < (m - 0 ) by XREAL_1: 15;

                    then m1 in ( Seg m) by A235;

                    then

                     A292: m1 in ( dom TM1B) by A240, A259, FINSEQ_1:def 3;

                    

                     A293: m1 in ( dom TM1) by A240, A235, FINSEQ_3: 25;

                    (H . j1) = (TM1B . m1) by A274, A289, A292, FINSEQ_1:def 7

                    .= (TM1 . m1) by A293, FINSEQ_1:def 7

                    .= (T . m1) by a240, A240, FUNCT_1: 49, A235, FINSEQ_3: 25;

                    hence (F . j) = |.( vol (( divset (H,j)),rho)).| by A280, A289, A290, A291, INTEGRA1:def 2;

                  end;

                    suppose j <> ( len H);

                    then

                     A294: j < (( len H1) + m) by A240, A261, A282, XXREAL_0: 1;

                    per cases ;

                      suppose j > ( len H1);

                      then

                       A295: (j - ( len H1)) > 0 by XREAL_1: 50;

                      then (j - ( len H1)) in NAT by INT_1: 3;

                      then

                      reconsider j1 = (j - ( len H1)) as Nat;

                      

                       A296: j1 < ((( len H1) + m) - ( len H1)) by A294, XREAL_1: 14;

                      then (j1 + 1) <= m by NAT_1: 13;

                      then

                       A297: ((j1 + 1) - 1) <= (m - 1) by XREAL_1: 13;

                      

                       A298: 1 <= j1 by A295, NAT_1: 14;

                      then

                       A299: j1 in ( Seg m) by A296;

                      

                       A300: j1 in ( dom q) by A296, A264, FINSEQ_3: 25, A298;

                      

                       A301: j1 in ( Seg m1) by A297, A298;

                      then

                       A302: j1 in ( dom TM1) by A240, FINSEQ_1:def 3;

                      

                       A303: (F . j) = (F . (( len H1) + j1))

                      .= (q . j1) by A277, A300, FINSEQ_1:def 7

                      .= |.( vol ((( divset (T,j1)) /\ ( divset (S,(k + 1)))),rho)).| by A267, A297, A298;

                      

                       A304: j1 in ( dom TM1B) by A240, A259, A299, FINSEQ_1:def 3;

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

                      then

                       A305: m1 in ( dom TM1) by A240, FINSEQ_1:def 3;

                      

                       A306: (H . j) = (H . (( len H1) + j1))

                      .= (TM1B . j1) by A304, FINSEQ_1:def 7

                      .= (TM1 . j1) by A302, FINSEQ_1:def 7

                      .= (T . j1) by A301, FUNCT_1: 49;

                      

                       A307: j1 in ( dom T) by A302, RELAT_1: 57;

                      m1 in ( dom T) by A305, RELAT_1: 57;

                      then (T . j1) <= (T . m1) by A297, A307, VALUED_0:def 15;

                      then

                       A308: (T . j1) <= ( upper_bound B) by A243, XXREAL_0: 2;

                      per cases ;

                        suppose

                         A309: j1 <> 1;

                        then

                         A310: ( lower_bound ( divset (T,j1))) = (T . (j1 - 1)) & ( upper_bound ( divset (T,j1))) = (T . j1) by A307, INTEGRA1:def 4;

                        1 < j1 by A298, A309, XXREAL_0: 1;

                        then (1 + 1) <= j1 by NAT_1: 13;

                        then

                         A311: ((1 + 1) - 1) <= (j1 - 1) by XREAL_1: 9;

                        then (j1 - 1) in NAT by INT_1: 3;

                        then

                        reconsider j11 = (j1 - 1) as Nat;

                        

                         A312: j11 <= (m1 - 0 ) by A297, XREAL_1: 13;

                        j11 <= ( len T) by A235, A312, XXREAL_0: 2;

                        then

                         A313: ( lower_bound ( divset (S,(k + 1)))) <= ( lower_bound ( divset (T,j1))) by A170, A238, A310, A311, FINSEQ_3: 25;

                        

                         A314: ( upper_bound ( divset (T,j1))) <= ( upper_bound ( divset (S,(k + 1)))) by A4, A5, A159, A170, A307, A308, A309, INTEGRA1:def 4;

                        

                         A315: ( divset (T,j1)) = [.( lower_bound ( divset (T,j1))), ( upper_bound ( divset (T,j1))).] by INTEGRA1: 4;

                        

                         A316: (( divset (T,j1)) /\ ( divset (S,(k + 1)))) = ( divset (T,j1)) by A169, A313, A314, A315, XBOOLE_1: 28, XXREAL_1: 34;

                        (m - 1) < (m - 0 ) by XREAL_1: 15;

                        then 1 <= j11 <= m by A311, A312, XXREAL_0: 2;

                        then

                         A317: j11 in ( dom TM1B) by A240, A259, FINSEQ_3: 25;

                        

                         A318: j11 in ( Seg m1) by A311, A312;

                        then

                         A319: j11 in ( dom TM1) by A240, FINSEQ_1:def 3;

                        

                         A320: (H . (j - 1)) = (H . (( len H1) + j11))

                        .= (TM1B . j11) by A317, FINSEQ_1:def 7

                        .= (TM1 . j11) by A319, FINSEQ_1:def 7

                        .= (T . j11) by A318, FUNCT_1: 49;

                        

                         A321: ( upper_bound ( divset (H,j))) = (T . j1) by A281, A288, A306, INTEGRA1:def 4

                        .= ( upper_bound ( divset (T,j1))) by A307, A309, INTEGRA1:def 4;

                        ( lower_bound ( divset (H,j))) = (T . (j1 - 1)) by A281, A288, A320, INTEGRA1:def 4

                        .= ( lower_bound ( divset (T,j1))) by A307, A309, INTEGRA1:def 4;

                        hence (F . j) = |.( vol (( divset (H,j)),rho)).| by A303, A315, A316, A321, INTEGRA1: 4;

                      end;

                        suppose

                         A322: j1 = 1;

                        then

                         A323: ( lower_bound ( divset (T,j1))) = ( lower_bound A) & ( upper_bound ( divset (T,j1))) = (T . j1) by A307, INTEGRA1:def 4;

                        

                         A324: ( divset (T,j1)) = [.( lower_bound ( divset (T,j1))), ( upper_bound ( divset (T,j1))).] by INTEGRA1: 4;

                        

                         A325: ( upper_bound ( divset (H,j))) = (T . j1) by A281, A288, A306, INTEGRA1:def 4

                        .= ( upper_bound ( divset (T,j1))) by A307, A322, INTEGRA1:def 4;

                        

                         A326: ( len H1) in ( dom H1) by A275, FINSEQ_3: 25;

                        

                         A327: ( lower_bound ( divset (H,j))) = (H . ((( len H1) + j1) - 1)) by A281, A288, INTEGRA1:def 4

                        .= (S . k) by A246, A322, A326, FINSEQ_1:def 7;

                        (( divset (T,j1)) /\ ( divset (S,(k + 1)))) = [.(S . k), ( upper_bound ( divset (T,j1))).] by A4, A163, A169, A170, A171, A308, A323, A324, XXREAL_1: 143

                        .= ( divset (H,j)) by A325, A327, INTEGRA1: 4;

                        hence (F . j) = |.( vol (( divset (H,j)),rho)).| by A303;

                      end;

                    end;

                      suppose

                       B: j <= ( len H1);

                      then

                       A328: j in ( Seg ( len H1)) by A282;

                      

                       A329: j in ( dom H1) by A282, B, FINSEQ_3: 25;

                      then

                       A330: (H . j) = (H1 . j) by FINSEQ_1:def 7;

                      (j - 1) in NAT by A281, INT_1: 5, FINSEQ_3: 25;

                      then

                      reconsider j1 = (j - 1) as Nat;

                      1 < j by A282, A288, XXREAL_0: 1;

                      then (j - 1) in ( Seg ( len H1)) by A328, FINSEQ_3: 12;

                      then (j - 1) in ( dom H1) by FINSEQ_1:def 3;

                      then

                       A331: (H . j1) = (H1 . j1) by FINSEQ_1:def 7;

                      

                       A332: ( lower_bound ( divset (H,j))) = (H . (j - 1)) & ( upper_bound ( divset (H,j))) = (H . j) by A281, A288, INTEGRA1:def 4;

                      

                      thus (F . j) = (F1 . j) by A278, A329, FINSEQ_1:def 7

                      .= |.( vol (( divset (H1,j)),rho)).| by A329, INTEGR22:def 2

                      .= |.( vol (( divset (H,j)),rho)).| by A288, A329, A330, A331, A332, INTEGRA1:def 4;

                    end;

                  end;

                end;

              end;

              then

              reconsider F as var_volume of rho, H by A240, A261, A264, A273, A277, INTEGR22:def 2;

              take H, F;

              

               Z: ( dom p) = ( dom T) by FINSEQ_3: 29, A153;

              

               A333: for i be Nat st i in ( dom p) holds (i <= ( len q) implies (p . i) = (q . i)) & (( len q) < i implies (p . i) = 0 )

              proof

                let i be Nat;

                assume

                 A334: i in ( dom p);

                then

                 A335: 1 <= i <= ( len p) by FINSEQ_3: 25;

                ( dom p) = ( dom T) by A153, FINSEQ_3: 29;

                then

                 A336: (p . i) = |.( vol ((( divset (T,i)) /\ ( divset (S,(k + 1)))),rho)).| by A153, A334;

                thus i <= ( len q) implies (p . i) = (q . i)

                proof

                  assume

                   A337: i <= ( len q);

                  

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

                  per cases ;

                    suppose i <> m;

                    then i < m by A264, A337, XXREAL_0: 1;

                    then (i + 1) <= m by NAT_1: 13;

                    then ((i + 1) - 1) <= (m - 1) by XREAL_1: 13;

                    hence thesis by A267, A335, A336;

                  end;

                    suppose

                     A339: i = m;

                    (m - 1) < (m - 0 ) by XREAL_1: 15;

                    then

                     A341: ( lower_bound ( divset (T,m))) = (T . (m - 1)) & ( upper_bound ( divset (T,m))) = (T . m) by A235, A160, INTEGRA1:def 4;

                    

                     A342: ( lower_bound ( divset (S,(k + 1)))) < ( lower_bound ( divset (T,m))) by A170, A234, A238, A341;

                    (( divset (T,i)) /\ ( divset (S,(k + 1)))) = ( [.( lower_bound ( divset (T,i))), ( upper_bound ( divset (T,i))).] /\ [.( lower_bound ( divset (S,(k + 1)))), ( upper_bound ( divset (S,(k + 1)))).]) by A338, INTEGRA1: 4

                    .= [.(T . m1), ( upper_bound B).] by A4, A5, A159, A160, A170, A339, A341, A342, XXREAL_1: 143;

                    hence thesis by A153, A266, A334, A339, Z;

                  end;

                end;

                

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

                thus ( len q) < i implies (p . i) = 0

                proof

                  assume

                   A344: ( len q) < i;

                  (m - 1) < (m - 0 ) by XREAL_1: 15;

                  then

                   A345: 1 < m by A235, XXREAL_0: 2;

                  then

                   A346: ( lower_bound ( divset (T,i))) = (T . (i - 1)) & ( upper_bound ( divset (T,i))) = (T . i) by A264, A344, INTEGRA1:def 4, A334, Z;

                  (m + 1) <= i by A264, A344, NAT_1: 13;

                  then

                   A347: ((m + 1) - 1) <= (i - 1) by XREAL_1: 13;

                  then

                   A348: 1 < (i - 1) by A345, XXREAL_0: 2;

                  (i - 1) in NAT by A347, INT_1: 3;

                  then

                  reconsider i1 = (i - 1) as Nat;

                  (( len T) - 1) < (( len T) - 0 ) by XREAL_1: 15;

                  then i1 <= ( len T) by A153, A335, XREAL_1: 15;

                  then

                   A350: i1 in ( dom T) by A348, FINSEQ_3: 25;

                  (( divset (T,i)) /\ ( divset (S,(k + 1)))) c= [.( upper_bound ( divset (S,(k + 1)))), ( upper_bound ( divset (S,(k + 1)))).] by A4, A5, A159, A164, A169, A170, A343, A346, A347, A350, Th10;

                  hence thesis by A336, COMPLEX1: 44, Th11;

                end;

              end;

              

              thus ( Sum ST) = (( Sum F1) + ( Sum p)) by A150, A152, A153, RVSUM_1: 74

              .= ( Sum F) by A272, A264, A153, A160, FINSEQ_3: 25, A333, Th9;

            end;

              suppose IDX <> {} ;

              then

               A351: ( sup IDX) in IDX by XXREAL_2:def 6;

              then

              reconsider n = ( sup IDX) as Nat;

              consider i be Nat such that

               A352: n = i & i in ( dom T) & (T . i) <= (S . k) by A351;

              

               A353: 1 <= n <= ( len T) by FINSEQ_3: 25, A352;

              n <> ( len T)

              proof

                assume n = ( len T);

                then

                 A354: ( upper_bound A) <= (S . k) by A352, INTEGRA1:def 2;

                ( upper_bound A) < ( upper_bound B) by A168, A354, XXREAL_0: 2;

                hence contradiction by A4, XXREAL_2: 59;

              end;

              then n < ( len T) by A353, XXREAL_0: 1;

              then

               Z: 1 <= (n + 1) <= ( len T) by NAT_1: 11, NAT_1: 13;

              then

               A355: (n + 1) in ( dom T) by FINSEQ_3: 25;

              

               A356: (S . k) < (T . (n + 1))

              proof

                assume (T . (n + 1)) <= (S . k);

                then (n + 1) in IDX by A355;

                hence contradiction by NAT_1: 16, XXREAL_2: 4;

              end;

              

               A357: for i be Nat st i in ( dom T) & n < i holds (S . k) < (T . i)

              proof

                let i be Nat;

                assume

                 A358: i in ( dom T) & n < i;

                then

                 A359: (n + 1) <= i by NAT_1: 13;

                (n + 1) in ( dom T) by Z, FINSEQ_3: 25;

                then (T . (n + 1)) <= (T . i) by A358, A359, VALUED_0:def 15;

                hence (S . k) < (T . i) by A356, XXREAL_0: 2;

              end;

              

               A361: n < m

              proof

                assume m <= n;

                then (T . m) <= (T . n) by A160, A352, VALUED_0:def 15;

                then ( upper_bound B) <= (T . n) by A160, XXREAL_0: 2;

                hence contradiction by A168, A352, XXREAL_0: 2;

              end;

              

               A364: for i be Nat st i <= n & i in ( dom T) holds (T . i) <= (S . k)

              proof

                let i be Nat;

                assume

                 A365: i <= n & i in ( dom T);

                assume

                 A366: not (T . i) <= (S . k);

                (T . i) <= (T . n) by A352, A365, VALUED_0:def 15;

                hence contradiction by A352, A366, XXREAL_0: 2;

              end;

              

               A368: for i be Nat st n < i & i < m & i in ( dom T) holds (S . k) < (T . i) & (T . i) < (S . (k + 1))

              proof

                let i be Nat;

                assume

                 A369: n < i & i < m & i in ( dom T);

                hence (S . k) < (T . i) by A357;

                assume not (T . i) < (S . (k + 1));

                then i in JDX by A4, A5, A159, A369;

                hence contradiction by A369, NAT_1:def 1;

              end;

              

               A370: (n + 1) <= m by A361, NAT_1: 13;

              per cases ;

                suppose

                 A371: (n + 1) = m;

                set H = (H1 ^ <*( upper_bound B)*>);

                (H1 . ( len H1)) = (S . k) by A126, INTEGRA1:def 2;

                then

                reconsider H as non empty increasing FinSequence of REAL by A168, Th14;

                

                 A372: ( len <*( upper_bound B)*>) = 1 by FINSEQ_1: 39;

                then

                 A373: ( len H) = (( len H1) + 1) by FINSEQ_1: 22;

                

                 A374: (H . ( len H)) = ( upper_bound B) by A373, FINSEQ_1: 42;

                ( rng H1) c= B1 by INTEGRA1:def 2;

                then

                 A375: ( rng H1) c= B by A123;

                

                 A376: ( rng H) = (( rng H1) \/ ( rng <*( upper_bound B)*>)) by FINSEQ_1: 31;

                

                 A377: ( rng <*( upper_bound B)*>) = {( upper_bound B)} by FINSEQ_1: 39;

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

                then ( upper_bound B) in B by A115;

                then ( rng <*( upper_bound B)*>) c= B by A377, ZFMISC_1: 31;

                then

                reconsider H as Division of B by A374, A375, A376, INTEGRA1:def 2, XBOOLE_1: 8;

                set F = (F1 ^ <* |.( vol ( [.(S . k), ( upper_bound B).],rho)).|*>);

                 |.( vol ( [.(S . k), ( upper_bound B).],rho)).| is Element of REAL by XREAL_0:def 1;

                then

                 A378: <* |.( vol ( [.(S . k), ( upper_bound B).],rho)).|*> is FinSequence of REAL by FINSEQ_1: 74;

                reconsider F as FinSequence of REAL by A378, FINSEQ_1: 75;

                

                 A379: ( len F) = (( len F1) + ( len <* |.( vol ( [.(S . k), ( upper_bound B).],rho)).|*>)) by FINSEQ_1: 22

                .= (( len H1) + ( len <* |.( vol ( [.(S . k), ( upper_bound B).],rho)).|*>)) by INTEGR22:def 2

                .= (( len H1) + 1) by FINSEQ_1: 40

                .= ( len H) by A372, FINSEQ_1: 22;

                

                 D: 1 <= ( len H1) by NAT_1: 14;

                then

                 A380: 1 in ( dom H1) by FINSEQ_3: 25;

                

                 A381: ( len F1) = ( len H1) by INTEGR22:def 2;

                then

                 A382: ( dom F1) = ( dom H1) by FINSEQ_3: 29;

                for j be Nat st j in ( dom H) holds (F . j) = |.( vol (( divset (H,j)),rho)).|

                proof

                  let j be Nat;

                  

                   A383: ( divset (H,j)) = [.( lower_bound ( divset (H,j))), ( upper_bound ( divset (H,j))).] & ( divset (H1,j)) = [.( lower_bound ( divset (H1,j))), ( upper_bound ( divset (H1,j))).] by INTEGRA1: 4;

                  assume

                   A384: j in ( dom H);

                  then

                   A385: 1 <= j <= ( len H) by FINSEQ_3: 25;

                  per cases ;

                    suppose

                     A386: j = 1;

                    then

                     A387: ( lower_bound ( divset (H,j))) = ( lower_bound B) & ( upper_bound ( divset (H,j))) = (H . j) by A384, INTEGRA1:def 4;

                    

                     A388: j in ( dom H1) by D, A386, FINSEQ_3: 25;

                    

                     A389: ( lower_bound ( divset (H1,j))) = ( lower_bound B1) & ( upper_bound ( divset (H1,j))) = (H1 . j) by INTEGRA1:def 4, A380, A386;

                    

                     A390: ( lower_bound B) = ( lower_bound B1) by A122, A137, INTEGRA1: 5;

                    

                    thus (F . j) = (F1 . j) by A382, A388, FINSEQ_1:def 7

                    .= |.( vol (( divset (H1,j)),rho)).| by A388, INTEGR22:def 2

                    .= |.( vol (( divset (H,j)),rho)).| by A383, A387, A388, A389, A390, FINSEQ_1:def 7;

                  end;

                    suppose

                     A391: j <> 1;

                    per cases ;

                      suppose

                       A392: j = ( len H);

                      

                       A393: (F . j) = |.( vol ( [.(S . k), ( upper_bound B).],rho)).| by A373, A381, A392, FINSEQ_1: 42;

                      

                       A394: ( lower_bound ( divset (H,j))) = (H . (j - 1)) & ( upper_bound ( divset (H,j))) = (H . j) by A384, A391, INTEGRA1:def 4;

                      (j - 1) in NAT by A384, INT_1: 5, FINSEQ_3: 25;

                      then

                      reconsider j1 = (j - 1) as Nat;

                      1 < j by A385, A391, XXREAL_0: 1;

                      then (1 - 1) < j1 by XREAL_1: 14;

                      then 1 <= j1 by NAT_1: 14;

                      then j1 in ( dom H1) by FINSEQ_3: 25, A373, A392;

                      

                      then (H . (j - 1)) = (H1 . ( len H1)) by A373, A392, FINSEQ_1:def 7

                      .= (S . k) by A126, INTEGRA1:def 2;

                      hence (F . j) = |.( vol (( divset (H,j)),rho)).| by A383, A392, A393, A394, INTEGRA1:def 2;

                    end;

                      suppose j <> ( len H);

                      then j < (( len H1) + 1) by A373, A385, XXREAL_0: 1;

                      then

                       K: j <= ( len H1) by NAT_1: 13;

                      then

                       A396: j in ( Seg ( len H1)) by A385;

                      

                       A397: j in ( dom H1) by FINSEQ_3: 25, K, A385;

                      then

                       A398: (H . j) = (H1 . j) by FINSEQ_1:def 7;

                      (j - 1) in NAT by A384, FINSEQ_3: 25, INT_1: 5;

                      then

                      reconsider j1 = (j - 1) as Nat;

                      1 < j by A385, A391, XXREAL_0: 1;

                      then (j - 1) in ( Seg ( len H1)) by A396, FINSEQ_3: 12;

                      then (j - 1) in ( dom H1) by FINSEQ_1:def 3;

                      then

                       A399: (H . j1) = (H1 . j1) by FINSEQ_1:def 7;

                      

                       A400: ( lower_bound ( divset (H,j))) = (H . (j - 1)) & ( upper_bound ( divset (H,j))) = (H . j) by A384, A391, INTEGRA1:def 4;

                      

                      thus (F . j) = (F1 . j) by A382, A397, FINSEQ_1:def 7

                      .= |.( vol (( divset (H1,j)),rho)).| by A397, INTEGR22:def 2

                      .= |.( vol (( divset (H,j)),rho)).| by A391, A397, A398, A399, A400, INTEGRA1:def 4;

                    end;

                  end;

                end;

                then

                reconsider F as var_volume of rho, H by A379, INTEGR22:def 2;

                take H, F;

                

                 A401: 1 < (1 + n) by A353, NAT_1: 16;

                

                 A403: (p . m) = |.( vol ((( divset (T,m)) /\ ( divset (S,(k + 1)))),rho)).| by A153, A160;

                

                 A405: ( lower_bound ( divset (T,m))) = (T . m1) & ( upper_bound ( divset (T,m))) = (T . m) by A160, A371, A401, INTEGRA1:def 4;

                 [.( lower_bound ( divset (S,(k + 1)))), ( upper_bound ( divset (S,(k + 1)))).] c= [.( lower_bound ( divset (T,m))), ( upper_bound ( divset (T,m))).] by A160, A170, A171, A352, A371, A405, XXREAL_1: 34;

                then ( divset (S,(k + 1))) c= ( divset (T,m)) by A169, INTEGRA1: 4;

                then

                 A406: (p . m) = |.( vol (( divset (S,(k + 1))),rho)).| by A403, XBOOLE_1: 28;

                for i be Nat st i in ( dom p) & i <> m holds (p . i) = 0

                proof

                  let i be Nat;

                  assume

                   A407: i in ( dom p) & i <> m;

                  then

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

                  

                   A409: 1 <= i <= ( len p) by A407, FINSEQ_3: 25;

                  per cases by A407, XXREAL_0: 1;

                    suppose

                     A410: i < m;

                    

                     A412: i in ( dom T) by A153, A408, FINSEQ_1:def 3;

                    

                     A413: ( upper_bound ( divset (T,i))) = (T . i)

                    proof

                      per cases ;

                        suppose i = 1;

                        hence ( upper_bound ( divset (T,i))) = (T . i) by A412, INTEGRA1:def 4;

                      end;

                        suppose i <> 1;

                        hence ( upper_bound ( divset (T,i))) = (T . i) by A412, INTEGRA1:def 4;

                      end;

                    end;

                    

                     A414: ((i + 1) - 1) <= ((n + 1) - 1) by A371, A410, NAT_1: 13;

                    

                     A415: (( divset (T,i)) /\ ( divset (S,(k + 1)))) = ( [.( lower_bound ( divset (T,i))), ( upper_bound ( divset (T,i))).] /\ [.( lower_bound ( divset (S,(k + 1)))), ( upper_bound ( divset (S,(k + 1)))).]) by A169, INTEGRA1: 4;

                    (( divset (T,i)) /\ ( divset (S,(k + 1)))) c= [.( upper_bound ( divset (T,i))), ( upper_bound ( divset (T,i))).] by H, A170, A364, A407, A413, A414, A415, Th10;

                    then ( vol ((( divset (T,i)) /\ ( divset (S,(k + 1)))),rho)) = 0 by Th11;

                    hence thesis by A153, COMPLEX1: 44, A412;

                  end;

                    suppose

                     A416: m < i;

                    then

                     A417: 1 < i by A353, A371, NAT_1: 16, XXREAL_0: 2;

                    

                     a418: i in ( dom T) by A153, A408, FINSEQ_1:def 3;

                    then

                     A419: ( lower_bound ( divset (T,i))) = (T . (i - 1)) & ( upper_bound ( divset (T,i))) = (T . i) by A371, A401, A416, INTEGRA1:def 4;

                    (m + 1) <= i by A416, NAT_1: 13;

                    then

                     A420: ((m + 1) - 1) <= (i - 1) by XREAL_1: 9;

                    (1 + 1) <= i by A417, NAT_1: 13;

                    then

                     A421: (2 - 1) <= (i - 1) by XREAL_1: 9;

                    then

                    reconsider i1 = (i - 1) as Nat by INT_1: 3, ORDINAL1:def 12;

                    (i - 1) <= (( len p) - 0 ) by A409, XREAL_1: 13;

                    then i1 in ( dom T) by A153, FINSEQ_3: 25, A421;

                    then

                     A422: (T . m) <= (T . i1) by A160, A420, VALUED_0:def 15;

                    (( divset (T,i)) /\ ( divset (S,(k + 1)))) = ( [.( lower_bound ( divset (T,i))), ( upper_bound ( divset (T,i))).] /\ [.( lower_bound ( divset (S,(k + 1)))), ( upper_bound ( divset (S,(k + 1)))).]) by A169, INTEGRA1: 4;

                    then (( divset (T,i)) /\ ( divset (S,(k + 1)))) c= [.( upper_bound ( divset (S,(k + 1)))), ( upper_bound ( divset (S,(k + 1)))).] by A160, A170, A171, A419, A422, Th10, XXREAL_0: 2;

                    then ( vol ((( divset (T,i)) /\ ( divset (S,(k + 1)))),rho)) = 0 by Th11;

                    hence thesis by A153, a418, COMPLEX1: 44;

                  end;

                end;

                

                then

                 A423: ( Sum p) = |.( vol (( divset (S,(k + 1))),rho)).| by A160, H, A406, Th8

                .= |.( vol ( [.(S . k), ( upper_bound B).],rho)).| by A4, A5, A159, A170, INTEGRA1: 4;

                

                thus ( Sum ST) = (( Sum F1) + ( Sum p)) by A150, A152, A153, RVSUM_1: 74

                .= ( Sum F) by A423, RVSUM_1: 74;

              end;

                suppose

                 A424: (n + 1) <> m;

                then

                 A425: (n + 1) < m by A370, XXREAL_0: 1;

                (m - (n + 1)) in NAT by A370, INT_1: 5;

                then

                reconsider mn1 = (m - (n + 1)) as Nat;

                (m - n) in NAT by A361, INT_1: 5;

                then

                reconsider mn = (m - n) as Nat;

                

                 A426: ( 0 + 1) <= mn1 by A425, NAT_1: 13, XREAL_1: 50;

                ((m - n) - 1) <= (mn - 0 ) by XREAL_1: 13;

                then

                 A427: 1 <= mn by A426, XXREAL_0: 2;

                consider TM1 be non empty increasing FinSequence of REAL such that

                 A428: ( len TM1) = mn1 & ( rng TM1) c= ( rng T) & for i be Nat st i in ( dom TM1) holds (TM1 . i) = (T . (i + n)) by A233, A425, Th16;

                consider pM1 be FinSequence of REAL such that

                 A429: ( len pM1) = (mn1 - 1) & ( rng pM1) c= ( rng p) & for i be Nat st i in ( dom pM1) holds (pM1 . i) = (p . ((i + n) + 1)) by A153, A233, A425, Th17;

                reconsider m1 = (m - 1) as Nat by a234;

                

                 A430: (TM1 . ( len TM1)) = (T . (mn1 + n)) by FINSEQ_3: 25, A426, A428;

                

                 A431: (T . (mn1 + n)) < ( upper_bound B)

                proof

                  assume

                   A432: not (T . (mn1 + n)) < ( upper_bound B);

                  

                   A433: (mn1 + n) in JDX by A234, A432;

                  (m - 1) < (m - 0 ) by XREAL_1: 15;

                  hence contradiction by A433, NAT_1:def 1;

                end;

                then

                reconsider TM1B = (TM1 ^ <*( upper_bound B)*>) as non empty increasing FinSequence of REAL by A430, Th14;

                

                 A434: (H1 . ( len H1)) = (S . k) by A126, INTEGRA1:def 2;

                

                 KK: 1 in ( dom TM1) by A426, A428, FINSEQ_3: 25;

                

                 A436: (TM1 . 1) = (T . (1 + n)) by A428, A426, FINSEQ_3: 25;

                

                 A437: (TM1B . 1) = (T . (1 + n)) by A436, FINSEQ_1:def 7, KK;

                reconsider H = (H1 ^ TM1B) as non empty increasing FinSequence of REAL by A356, A434, A437, Th13;

                

                 A438: ( rng TM1B) = (( rng TM1) \/ ( rng <*( upper_bound B)*>)) by FINSEQ_1: 31;

                

                 A439: ( rng <*( upper_bound B)*>) = {( upper_bound B)} by FINSEQ_1: 39;

                

                 A444: ( rng TM1) c= B

                proof

                  let z be object;

                  assume

                   A440: z in ( rng TM1);

                  then

                  reconsider x = z as Real;

                  x in A by A428, A440, INTEGRA1:def 2, TARSKI:def 3;

                  then

                   A441: ex r be Real st x = r & ( lower_bound A) <= r & r <= ( upper_bound A) by A116;

                  consider i be object such that

                   A442: i in ( dom TM1) & x = (TM1 . i) by A440, FUNCT_1:def 3;

                  reconsider i as Nat by A442;

                  

                   A443: 1 <= i <= ( len TM1) by A442, FINSEQ_3: 25;

                  1 <= ( len TM1) <= ( len TM1) by A443, XXREAL_0: 2;

                  then ( len TM1) in ( dom TM1) by FINSEQ_3: 25;

                  then (TM1 . i) <= (TM1 . ( len TM1)) by A442, A443, VALUED_0:def 15;

                  then x <= ( upper_bound B) by A430, A431, A442, XXREAL_0: 2;

                  hence z in B by A4, A115, A441;

                end;

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

                then ( upper_bound B) in B by A115;

                then {( upper_bound B)} c= B by ZFMISC_1: 31;

                then

                 A445: ( rng TM1B) c= B by A438, A439, A444, XBOOLE_1: 8;

                ( rng H1) c= B1 by INTEGRA1:def 2;

                then ( rng H1) c= B by A123;

                then (( rng H1) \/ ( rng TM1B)) c= B by A445, XBOOLE_1: 8;

                then

                 A446: ( rng H) c= B by FINSEQ_1: 31;

                

                 A447: ( len TM1B) = (( len TM1) + ( len <*( upper_bound B)*>)) by FINSEQ_1: 22

                .= (( len TM1) + 1) by FINSEQ_1: 40;

                (( len TM1) + 1) in ( Seg (( len TM1) + 1)) by FINSEQ_1: 4;

                then

                 A448: (( len TM1) + 1) in ( dom TM1B) by A447, FINSEQ_1:def 3;

                

                 A449: ( len H) = (( len H1) + (( len TM1) + 1)) by A447, FINSEQ_1: 22;

                

                 G: 1 in ( Seg 1);

                then

                 A450: 1 in ( dom <*( upper_bound B)*>) by FINSEQ_1: 38;

                (H . ( len H)) = (TM1B . (( len TM1) + 1)) by A448, A449, FINSEQ_1:def 7

                .= ( <*( upper_bound B)*> . 1) by A450, FINSEQ_1:def 7

                .= ( upper_bound B) by FINSEQ_1: 40;

                then

                reconsider H as Division of B by A446, INTEGRA1:def 2;

                set q1 = ( <* |.( vol ( [.(S . k), (T . (n + 1)).],rho)).|*> ^ pM1);

                set q = (q1 ^ <* |.( vol ( [.(T . m1), ( upper_bound B).],rho)).|*>);

                ( rng q1) c= REAL ;

                then

                reconsider q1 as FinSequence of REAL by FINSEQ_1:def 4;

                ( rng q) c= REAL ;

                then

                reconsider q as FinSequence of REAL by FINSEQ_1:def 4;

                

                 A451: ( len q1) = (( len <* |.( vol ( [.(S . k), (T . (n + 1)).],rho)).|*>) + ( len pM1)) by FINSEQ_1: 22

                .= (1 + (mn1 - 1)) by A429, FINSEQ_1: 40

                .= mn1;

                

                 A452: ( len q) = (( len q1) + ( len <* |.( vol ( [.(T . m1), ( upper_bound B).],rho)).|*>)) by FINSEQ_1: 22

                .= (mn1 + 1) by A451, FINSEQ_1: 40

                .= mn;

                

                 A453: 1 in ( dom <* |.( vol ( [.(T . m1), ( upper_bound B).],rho)).|*>) by G, FINSEQ_1: 38;

                

                 A454: (q . ( len q)) = (q . (mn1 + 1)) by A452

                .= ( <* |.( vol ( [.(T . m1), ( upper_bound B).],rho)).|*> . 1) by A451, A453, FINSEQ_1:def 7

                .= |.( vol ( [.(T . m1), ( upper_bound B).],rho)).| by FINSEQ_1: 40;

                

                 A455: 1 in ( dom <* |.( vol ( [.(S . k), (T . (n + 1)).],rho)).|*>) by FINSEQ_1: 38, G;

                1 in ( Seg mn1) by A426;

                then 1 in ( dom q1) by A451, FINSEQ_1:def 3;

                

                then

                 A456: (q . 1) = (q1 . 1) by FINSEQ_1:def 7

                .= ( <* |.( vol ( [.(S . k), (T . (n + 1)).],rho)).|*> . 1) by A455, FINSEQ_1:def 7

                .= |.( vol ( [.(S . k), (T . (n + 1)).],rho)).| by FINSEQ_1: 40;

                

                 A457: for i be Nat st 2 <= i & i <= ( len q1) holds (q . i) = |.( vol ((( divset (T,(n + i))) /\ ( divset (S,(k + 1)))),rho)).|

                proof

                  let i be Nat;

                  assume

                   A458: 2 <= i & i <= ( len q1);

                  then

                   A459: 1 <= i by XXREAL_0: 2;

                  then i in ( dom q1) by A458, FINSEQ_3: 25;

                  then

                   A460: (q . i) = (q1 . i) by FINSEQ_1:def 7;

                  

                   A461: (2 - 1) <= (i - 1) by A458, XREAL_1: 9;

                  then

                   A462: 1 <= (i - 1) & (i - 1) <= (mn1 - 1) by A451, A458, XREAL_1: 9;

                  (i - 1) in NAT by A461, INT_1: 3;

                  then

                  reconsider i1 = (i - 1) as Nat;

                  

                   A463: ( len <* |.( vol ( [.(S . k), (T . (n + 1)).],rho)).|*>) = 1 by FINSEQ_1: 40;

                  

                   A465: i1 in ( dom pM1) by FINSEQ_3: 25, A429, A462;

                  

                   A466: (q1 . i) = (q1 . (1 + i1))

                  .= (pM1 . i1) by A463, A465, FINSEQ_1:def 7

                  .= (p . ((i1 + n) + 1)) by FINSEQ_3: 25, A429, A462

                  .= (p . (i + n));

                  i <= (i + n) by NAT_1: 11;

                  then

                   A467: 1 <= (i + n) by A459, XXREAL_0: 2;

                  (i + n) <= (((m - n) - 1) + n) by A451, A458, XREAL_1: 6;

                  then (i + n) <= ( len T) by A235, XXREAL_0: 2;

                  hence thesis by A153, A460, A466, FINSEQ_3: 25, A467;

                end;

                reconsider F = (F1 ^ q) as FinSequence of REAL ;

                

                 A468: ( len F) = (( len F1) + ( len q)) by FINSEQ_1: 22;

                

                 E: 1 <= ( len H1) by NAT_1: 14;

                then

                 A469: 1 in ( dom H1) by FINSEQ_3: 25;

                

                 A470: ( len F1) = ( len H1) by INTEGR22:def 2;

                then

                 A471: ( dom F1) = ( dom H1) by FINSEQ_3: 29;

                mn in ( Seg mn) by A427;

                then

                 A472: mn in ( dom q) by A452, FINSEQ_1:def 3;

                1 <= ( len q) by NAT_1: 14;

                then

                 A473: 1 in ( dom q) by FINSEQ_3: 25;

                1 <= ( len TM1B) by NAT_1: 14;

                then

                 A474: 1 in ( dom TM1B) by FINSEQ_3: 25;

                1 <= ( len TM1) by NAT_1: 14;

                then

                 A475: 1 in ( dom TM1) by FINSEQ_3: 25;

                

                 A476: (H . (( len H1) + 1)) = (TM1B . 1) by A474, FINSEQ_1:def 7

                .= (TM1 . 1) by A475, FINSEQ_1:def 7

                .= (T . (n + 1)) by A428, A426, FINSEQ_3: 25;

                for j be Nat st j in ( dom H) holds (F . j) = |.( vol (( divset (H,j)),rho)).|

                proof

                  let j be Nat;

                  

                   A477: ( divset (H,j)) = [.( lower_bound ( divset (H,j))), ( upper_bound ( divset (H,j))).] & ( divset (H1,j)) = [.( lower_bound ( divset (H1,j))), ( upper_bound ( divset (H1,j))).] by INTEGRA1: 4;

                  assume

                   A478: j in ( dom H);

                  then

                   A479: 1 <= j <= ( len H) by FINSEQ_3: 25;

                  per cases ;

                    suppose

                     A480: j = 1;

                    then

                     A481: ( lower_bound ( divset (H,j))) = ( lower_bound B) & ( upper_bound ( divset (H,j))) = (H . j) by A478, INTEGRA1:def 4;

                    

                     A482: j in ( dom H1) by E, A480, FINSEQ_3: 25;

                    

                     A483: ( lower_bound ( divset (H1,j))) = ( lower_bound B1) & ( upper_bound ( divset (H1,j))) = (H1 . j) by A469, A480, INTEGRA1:def 4;

                    

                     A484: ( lower_bound B) = ( lower_bound B1) by A122, A137, INTEGRA1: 5;

                    

                    thus (F . j) = (F1 . j) by A471, A482, FINSEQ_1:def 7

                    .= |.( vol (( divset (H1,j)),rho)).| by A482, INTEGR22:def 2

                    .= |.( vol (( divset (H,j)),rho)).| by A477, A481, A482, A483, A484, FINSEQ_1:def 7;

                  end;

                    suppose

                     A485: j <> 1;

                    per cases ;

                      suppose

                       A486: j = ( len H);

                      then

                       A487: j = ((( len H1) + mn1) + 1) by A428, A449;

                      

                       A488: (F . j) = |.( vol ( [.(T . m1), ( upper_bound B).],rho)).| by A428, A449, A452, A454, A470, A472, A486, FINSEQ_1:def 7;

                      

                       A489: ( lower_bound ( divset (H,j))) = (H . (j - 1)) & ( upper_bound ( divset (H,j))) = (H . j) by A478, A485, INTEGRA1:def 4;

                      (j - 1) in NAT by A478, INT_1: 5, FINSEQ_3: 25;

                      then

                      reconsider j1 = (j - 1) as Nat;

                      (mn - 1) < (mn - 0 ) by XREAL_1: 15;

                      then mn1 in ( Seg mn) by A426;

                      then

                       A490: mn1 in ( dom TM1B) by A428, A447, FINSEQ_1:def 3;

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

                      then

                       A491: mn1 in ( dom TM1) by A428, FINSEQ_1:def 3;

                      (H . j1) = (TM1B . mn1) by A487, A490, FINSEQ_1:def 7

                      .= (T . m1) by A428, A430, A491, FINSEQ_1:def 7;

                      hence (F . j) = |.( vol (( divset (H,j)),rho)).| by A477, A486, A488, A489, INTEGRA1:def 2;

                    end;

                      suppose j <> ( len H);

                      then

                       A492: j < ((( len H1) + mn1) + 1) by A428, A449, A479, XXREAL_0: 1;

                      per cases ;

                        suppose j > ( len H1);

                        then

                         A493: (j - ( len H1)) > 0 by XREAL_1: 50;

                        then (j - ( len H1)) in NAT by INT_1: 3;

                        then

                        reconsider j1 = (j - ( len H1)) as Nat;

                        

                         A494: j1 < ((( len H1) + mn) - ( len H1)) by A492, XREAL_1: 14;

                        then (j1 + 1) <= mn by NAT_1: 13;

                        then

                         A495: ((j1 + 1) - 1) <= (mn - 1) by XREAL_1: 13;

                        

                         A496: 1 <= j1 by A493, NAT_1: 14;

                        then

                         A497: j1 in ( Seg mn) by A494;

                        then

                         A498: j1 in ( dom q) by A452, FINSEQ_1:def 3;

                        1 <= j1 <= mn1 by A493, A495, NAT_1: 14;

                        then j1 in ( Seg mn1);

                        then

                         A500: j1 in ( dom TM1) by A428, FINSEQ_1:def 3;

                        

                         A501: j1 in ( dom TM1B) by A428, A447, A497, FINSEQ_1:def 3;

                        

                         A502: (H . j) = (H . (( len H1) + j1))

                        .= (TM1B . j1) by A501, FINSEQ_1:def 7

                        .= (TM1 . j1) by A500, FINSEQ_1:def 7

                        .= (T . (j1 + n)) by A428, A500;

                        

                         A503: (j1 + n) <= (mn1 + n) by A495, XREAL_1: 6;

                        

                         A504: 1 <= (j1 + n) by A493, NAT_1: 14;

                        (j1 + n) <= ( len T) by A235, A503, XXREAL_0: 2;

                        then

                         A505: (j1 + n) in ( dom T) by A504, FINSEQ_3: 25;

                        then (T . (j1 + n)) <= (T . (mn1 + n)) by A234, A503, VALUED_0:def 15;

                        then

                         A506: (T . (j1 + n)) <= ( upper_bound ( divset (S,(k + 1)))) by A4, A5, A159, A170, A431, XXREAL_0: 2;

                        per cases ;

                          suppose

                           A507: j1 = 1;

                           0 < ( len H1);

                          then (1 + 0 ) < (1 + ( len H1)) by XREAL_1: 8;

                          then

                           A508: ( lower_bound ( divset (H,j))) = (H . (j - 1)) & ( upper_bound ( divset (H,j))) = (H . j) by A478, A507, INTEGRA1:def 4;

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

                          then

                           A509: ( len H1) in ( dom H1) by FINSEQ_1:def 3;

                          

                           A510: (F . j) = (F . (( len H1) + 1)) by A507

                          .= |.( vol ( [.(S . k), (T . (n + 1)).],rho)).| by A456, A470, A473, FINSEQ_1:def 7;

                          (H . ( len H1)) = (S . k) by A434, A509, FINSEQ_1:def 7;

                          hence (F . j) = |.( vol (( divset (H,j)),rho)).| by A476, A507, A508, A510, INTEGRA1: 4;

                        end;

                          suppose j1 <> 1;

                          then

                           A511: 1 < j1 by A496, XXREAL_0: 1;

                          then

                           A512: (1 + 1) <= j1 by NAT_1: 13;

                          

                           A513: (F . j) = (F . (( len H1) + j1))

                          .= (q . j1) by A470, A498, FINSEQ_1:def 7

                          .= |.( vol ((( divset (T,(j1 + n))) /\ ( divset (S,(k + 1)))),rho)).| by A451, A457, A495, A512;

                          

                           A514: (j1 + n) <> 1 by A511, NAT_1: 11;

                          then 1 < (j1 + n) by A504, XXREAL_0: 1;

                          then (1 + 1) <= (j1 + n) by NAT_1: 13;

                          then

                           A515: ((1 + 1) - 1) <= ((j1 + n) - 1) by XREAL_1: 9;

                          then ((j1 + n) - 1) in NAT by INT_1: 3;

                          then

                          reconsider j11 = ((j1 + n) - 1) as Nat;

                          (2 + (n - 1)) <= (j1 + (n - 1)) by A512, XREAL_1: 6;

                          then (n + 1) <= j11;

                          then

                           A516: n < j11 by NAT_1: 16, XXREAL_0: 2;

                          

                           A517: (j1 + (n - 1)) <= (((m - n) - 1) + (n - 1)) by A495, XREAL_1: 6;

                          (m1 - 1) <= (m1 - 0 ) by XREAL_1: 13;

                          then

                           A518: j11 <= m1 by A517, XXREAL_0: 2;

                          j11 <= ( len T) by A235, A518, XXREAL_0: 2;

                          then j11 in ( dom T) by FINSEQ_3: 25, A515;

                          then

                           A519: (S . k) < (T . j11) by A357, A516;

                          

                           A520: ( lower_bound ( divset (S,(k + 1)))) <= ( lower_bound ( divset (T,(j1 + n)))) by A170, A505, A514, A519, INTEGRA1:def 4;

                          

                           A521: ( upper_bound ( divset (T,(j1 + n)))) <= ( upper_bound ( divset (S,(k + 1)))) by A505, A506, A514, INTEGRA1:def 4;

                          

                           A522: ( divset (T,(j1 + n))) = [.( lower_bound ( divset (T,(j1 + n)))), ( upper_bound ( divset (T,(j1 + n)))).] by INTEGRA1: 4;

                          

                           A523: (( divset (T,(j1 + n))) /\ ( divset (S,(k + 1)))) = ( divset (T,(j1 + n))) by A169, A520, A521, A522, XBOOLE_1: 28, XXREAL_1: 34;

                          (j1 - 1) <= (j1 - 0 ) by XREAL_1: 13;

                          then

                           A524: (j11 - n) <= mn1 by A495, XXREAL_0: 2;

                          

                           A525: (2 - 1) <= (j1 - 1) by A512, XREAL_1: 9;

                          then (j11 - n) in NAT by INT_1: 3;

                          then

                          reconsider j11n = (j11 - n) as Nat;

                          j11n in ( Seg mn1) by A524, A525;

                          then

                           A527: (j11 - n) in ( dom TM1) by A428, FINSEQ_1:def 3;

                          (mn - 1) <= (mn - 0 ) by XREAL_1: 13;

                          then 1 <= (j11 - n) & (j11 - n) <= mn by A524, A525, XXREAL_0: 2;

                          then j11n in ( Seg mn);

                          then

                           A528: (j11 - n) in ( dom TM1B) by A428, A447, FINSEQ_1:def 3;

                          

                           A529: (H . (j - 1)) = (H . (( len H1) + (j11 - n)))

                          .= (TM1B . (j11 - n)) by A528, FINSEQ_1:def 7

                          .= (TM1 . (j11 - n)) by A527, FINSEQ_1:def 7

                          .= (T . ((j1 - 1) + n)) by A428, A527;

                          

                           A530: ( upper_bound ( divset (H,j))) = (T . (j1 + n)) by A478, A485, A502, INTEGRA1:def 4

                          .= ( upper_bound ( divset (T,(j1 + n)))) by A505, A514, INTEGRA1:def 4;

                          ( lower_bound ( divset (H,j))) = (T . ((j1 + n) - 1)) by A478, A485, A529, INTEGRA1:def 4

                          .= ( lower_bound ( divset (T,(j1 + n)))) by A505, A514, INTEGRA1:def 4;

                          hence (F . j) = |.( vol (( divset (H,j)),rho)).| by A513, A522, A523, A530, INTEGRA1: 4;

                        end;

                      end;

                        suppose j <= ( len H1);

                        then

                         A531: j in ( Seg ( len H1)) by A479;

                        then

                         A532: j in ( dom H1) by FINSEQ_1:def 3;

                        then

                         A533: (H . j) = (H1 . j) by FINSEQ_1:def 7;

                        (j - 1) in NAT by A478, INT_1: 5, FINSEQ_3: 25;

                        then

                        reconsider j1 = (j - 1) as Nat;

                        1 < j by A479, A485, XXREAL_0: 1;

                        then (j - 1) in ( Seg ( len H1)) by A531, FINSEQ_3: 12;

                        then (j - 1) in ( dom H1) by FINSEQ_1:def 3;

                        then

                         A534: (H . j1) = (H1 . j1) by FINSEQ_1:def 7;

                        

                         A535: ( lower_bound ( divset (H,j))) = (H . (j - 1)) & ( upper_bound ( divset (H,j))) = (H . j) by A478, A485, INTEGRA1:def 4;

                        

                        thus (F . j) = (F1 . j) by A471, A532, FINSEQ_1:def 7

                        .= |.( vol (( divset (H1,j)),rho)).| by A532, INTEGR22:def 2

                        .= |.( vol (( divset (H,j)),rho)).| by A485, A532, A533, A534, A535, INTEGRA1:def 4;

                      end;

                    end;

                  end;

                end;

                then

                reconsider F as var_volume of rho, H by A428, A449, A452, A468, A470, INTEGR22:def 2;

                take H, F;

                

                 A536: for i be Nat st i in ( dom p) holds (i <= n implies (p . i) = 0 ) & (i <= ( len q) implies (p . (n + i)) = (q . i)) & ((( len q) + n) < i implies (p . i) = 0 )

                proof

                  let i be Nat;

                  assume

                   A537: i in ( dom p);

                  then

                   A538: 1 <= i & i <= ( len p) by FINSEQ_3: 25;

                  

                   F: ( dom p) = ( dom T) by A153, FINSEQ_3: 29;

                  then

                   A539: (p . i) = |.( vol ((( divset (T,i)) /\ ( divset (S,(k + 1)))),rho)).| by A153, A537;

                  thus i <= n implies (p . i) = 0

                  proof

                    assume

                     A540: i <= n;

                    per cases ;

                      suppose i = 1;

                      then

                       A542: ( lower_bound ( divset (T,i))) = ( lower_bound A) & ( upper_bound ( divset (T,i))) = (T . i) by INTEGRA1:def 4, F, A537;

                      (( divset (T,i)) /\ ( divset (S,(k + 1)))) = ( [.( lower_bound ( divset (T,i))), ( upper_bound ( divset (T,i))).] /\ [.( lower_bound ( divset (S,(k + 1)))), ( upper_bound ( divset (S,(k + 1)))).]) by A169, INTEGRA1: 4;

                      then (( divset (T,i)) /\ ( divset (S,(k + 1)))) c= [.( upper_bound ( divset (T,i))), ( upper_bound ( divset (T,i))).] by A170, A364, A537, A540, F, A542, Th10;

                      hence thesis by A539, COMPLEX1: 44, Th11;

                    end;

                      suppose

                       A543: i <> 1;

                      then 1 < i by A538, XXREAL_0: 1;

                      then (1 + 1) <= i by NAT_1: 13;

                      then ((1 + 1) - 1) <= (i - 1) by XREAL_1: 13;

                      then (i - 1) in NAT by INT_1: 3;

                      then

                      reconsider i1 = (i - 1) as Nat;

                      

                       A544: ( lower_bound ( divset (T,i))) = (T . (i - 1)) & ( upper_bound ( divset (T,i))) = (T . i) by A543, INTEGRA1:def 4, A537, F;

                      (( divset (T,i)) /\ ( divset (S,(k + 1)))) = ( [.( lower_bound ( divset (T,i))), ( upper_bound ( divset (T,i))).] /\ [.( lower_bound ( divset (S,(k + 1)))), ( upper_bound ( divset (S,(k + 1)))).]) by A169, INTEGRA1: 4;

                      then (( divset (T,i)) /\ ( divset (S,(k + 1)))) c= [.( upper_bound ( divset (T,i))), ( upper_bound ( divset (T,i))).] by A170, A364, A537, A540, A544, F, Th10;

                      hence thesis by A539, COMPLEX1: 44, Th11;

                    end;

                  end;

                  thus i <= ( len q) implies (p . (n + i)) = (q . i)

                  proof

                    assume

                     A545: i <= ( len q);

                    per cases ;

                      suppose

                       A546: i = 1;

                      

                       A547: ( divset (T,(n + 1))) = [.( lower_bound ( divset (T,(n + 1)))), ( upper_bound ( divset (T,(n + 1)))).] by INTEGRA1: 4;

                      n <> 0 by FINSEQ_3: 25, A352;

                      then

                       A548: (n + 1) <> 1;

                      

                       A549: ( lower_bound ( divset (T,(n + 1)))) = (T . ((n + 1) - 1)) & ( upper_bound ( divset (T,(n + 1)))) = (T . (n + 1)) by A548, A355, INTEGRA1:def 4;

                      n < (n + 1) & (n + 1) < m by A370, A424, NAT_1: 16, XXREAL_0: 1;

                      then

                       A550: (T . (n + 1)) < (S . (k + 1)) by A355, A368;

                      (( divset (T,(n + 1))) /\ ( divset (S,(k + 1)))) = [.(S . k), (T . (n + 1)).] by A169, A170, A352, A547, A549, A550, XXREAL_1: 143;

                      hence (p . (n + i)) = (q . i) by A153, Z, A456, A546, FINSEQ_3: 25;

                    end;

                      suppose i <> 1;

                      then 1 < i by A538, XXREAL_0: 1;

                      then

                       A551: (1 + 1) <= i by NAT_1: 13;

                      per cases ;

                        suppose i <> mn;

                        then i < mn by A452, A545, XXREAL_0: 1;

                        then (i + 1) <= mn by NAT_1: 13;

                        then ((i + 1) - 1) <= (mn - 1) by XREAL_1: 9;

                        then

                         A552: (q . i) = |.( vol ((( divset (T,(n + i))) /\ ( divset (S,(k + 1)))),rho)).| by A451, A457, A551;

                        (i + n) <= ((m - n) + n) by A452, A545, XREAL_1: 7;

                        then

                         A553: (i + n) <= ( len T) by A233, XXREAL_0: 2;

                        (1 + 0 ) <= (i + n) by A538, XREAL_1: 7;

                        then (n + i) in ( Seg ( len T)) by A553;

                        then (n + i) in ( dom T) by FINSEQ_1:def 3;

                        hence (p . (n + i)) = (q . i) by A153, A552;

                      end;

                        suppose

                         A554: i = mn;

                        1 <= (n + 1) by NAT_1: 11;

                        then

                         A556: ( lower_bound ( divset (T,m))) = (T . (m - 1)) & ( upper_bound ( divset (T,m))) = (T . m) by A425, A160, INTEGRA1:def 4;

                        

                         A557: (m - 1) < (m - 0 ) by XREAL_1: 15;

                        ((n + 1) - 1) < (m - 1) by A425, XREAL_1: 14;

                        then

                         A558: (S . k) < (T . m1) < (S . (k + 1)) by A234, A368, A557;

                        (( divset (T,m)) /\ ( divset (S,(k + 1)))) = ( [.( lower_bound ( divset (T,m))), ( upper_bound ( divset (T,m))).] /\ [.( lower_bound ( divset (S,(k + 1)))), ( upper_bound ( divset (S,(k + 1)))).]) by A169, INTEGRA1: 4

                        .= [.(T . m1), ( upper_bound B).] by A4, A5, A159, A160, A170, A556, A558, XXREAL_1: 143;

                        hence (p . (n + i)) = (q . i) by A153, A160, A452, A454, A554;

                      end;

                    end;

                  end;

                  thus (( len q) + n) < i implies (p . i) = 0

                  proof

                    assume

                     A559: (( len q) + n) < i;

                    (m - 1) < (m - 0 ) by XREAL_1: 15;

                    then

                     A560: 1 < m by A235, XXREAL_0: 2;

                    

                     A561: ( lower_bound ( divset (T,i))) = (T . (i - 1)) & ( upper_bound ( divset (T,i))) = (T . i) by A452, A559, A560, INTEGRA1:def 4, A537, F;

                    (m + 1) <= i by A452, A559, NAT_1: 13;

                    then

                     A562: ((m + 1) - 1) <= (i - 1) by XREAL_1: 13;

                    then

                     A563: 1 < (i - 1) by A560, XXREAL_0: 2;

                    (i - 1) in NAT by A562, INT_1: 3;

                    then

                    reconsider i1 = (i - 1) as Nat;

                    (( len T) - 1) < (( len T) - 0 ) by XREAL_1: 15;

                    then

                     A565: i1 in ( dom T) by A563, FINSEQ_3: 25, A153, A538, XREAL_1: 13;

                    (( divset (T,i)) /\ ( divset (S,(k + 1)))) = ( [.( lower_bound ( divset (T,i))), ( upper_bound ( divset (T,i))).] /\ [.( lower_bound ( divset (S,(k + 1)))), ( upper_bound ( divset (S,(k + 1)))).]) by A169, INTEGRA1: 4;

                    then (( divset (T,i)) /\ ( divset (S,(k + 1)))) c= [.( upper_bound ( divset (S,(k + 1)))), ( upper_bound ( divset (S,(k + 1)))).] by A4, A5, A159, A164, A170, A561, A562, A565, Th10;

                    hence thesis by A539, COMPLEX1: 44, Th11;

                  end;

                end;

                (( len p) - (( len q) + n)) in NAT by A153, A233, A452, INT_1: 5;

                then

                reconsider L = (( len p) - (( len q) + n)) as Nat;

                set s = (((n |-> 0 qua Real) ^ q) ^ (L |-> 0 qua Real));

                reconsider nn = n, nL = L as Element of NAT by ORDINAL1:def 12;

                reconsider z0 = 0 qua Real as Element of REAL by XREAL_0:def 1;

                

                 A566: ( len (n |-> 0 qua Real)) = ( len (nn |-> z0))

                .= n by FINSEQ_2: 133;

                

                 A567: ( len (L |-> 0 qua Real)) = ( len (nL |-> z0))

                .= L by FINSEQ_2: 133;

                

                 A568: ( len s) = (( len ((n |-> 0 qua Real) ^ q)) + ( len (L |-> 0 qua Real))) by FINSEQ_1: 22

                .= ((n + ( len q)) + L) by A566, A567, FINSEQ_1: 22

                .= ( len p);

                for j be Nat st 1 <= j & j <= ( len p) holds (p . j) = (s . j)

                proof

                  let j be Nat;

                  assume

                   A569: 1 <= j <= ( len p);

                  then

                   A570: j in ( dom p) by FINSEQ_3: 25;

                  set sw = ((n |-> 0 qua Real) ^ q);

                  

                   A571: ( len sw) = (n + ( len q)) by A566, FINSEQ_1: 22;

                  per cases ;

                    suppose

                     A572: j <= n;

                    then

                     A573: (p . j) = 0 by A536, A570;

                    j <= (n + ( len q)) by A572, NAT_1: 12;

                    then j in ( Seg ( len sw)) by A569, A571;

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

                    then

                     A574: (s . j) = (sw . j) by FINSEQ_1:def 7;

                    j in ( Seg ( len (n |-> 0 qua Real))) by A566, A569, A572;

                    then j in ( dom (n |-> 0 qua Real)) by FINSEQ_1:def 3;

                    then

                     A575: (sw . j) = ((n |-> 0 qua Real) . j) by FINSEQ_1:def 7;

                    j in ( Seg n) by A569, A572;

                    hence (p . j) = (s . j) by A573, A574, A575, FINSEQ_2: 57;

                  end;

                    suppose

                     A576: n < j;

                    per cases ;

                      suppose

                       A577: j <= (( len q) + n);

                      (j - n) in NAT by A576, INT_1: 5;

                      then

                      reconsider jn = (j - n) as Nat;

                      

                       A578: ( 0 + 1) <= jn by A576, NAT_1: 13, XREAL_1: 50;

                      

                       A579: (j - n) <= ((( len q) + n) - n) by A577, XREAL_1: 9;

                      then

                       A580: jn in ( dom q) by A578, FINSEQ_3: 25;

                      ( len q) <= (( len q) + n) by NAT_1: 11;

                      then ( len q) <= ( len p) by A153, A233, A452, XXREAL_0: 2;

                      then jn <= ( len p) by A579, XXREAL_0: 2;

                      then jn in ( dom p) by FINSEQ_3: 25, A578;

                      then

                       A581: (p . (n + jn)) = (q . jn) by A536, A579;

                      

                       A582: j in ( dom sw) by A569, A571, A577, FINSEQ_3: 25;

                      (s . j) = (sw . (n + jn)) by A582, FINSEQ_1:def 7

                      .= (q . jn) by A566, A580, FINSEQ_1:def 7;

                      hence (p . j) = (s . j) by A581;

                    end;

                      suppose

                       A583: (( len q) + n) < j;

                      (j - (( len q) + n)) in NAT by A583, INT_1: 5;

                      then

                      reconsider j1 = (j - (( len q) + n)) as Nat;

                      

                       A584: ( 0 + 1) <= j1 by A583, NAT_1: 13, XREAL_1: 50;

                      (j - (( len q) + n)) <= (( len p) - (( len q) + n)) by A569, XREAL_1: 9;

                      then

                       A585: j1 in ( Seg L) by A584;

                      then

                       A586: j1 in ( dom (L |-> 0 qua Real)) by A567, FINSEQ_1:def 3;

                      (s . j) = (s . (( len sw) + j1)) by A571

                      .= ((L |-> 0 qua Real) . j1) by A586, FINSEQ_1:def 7

                      .= 0 by A585, FINSEQ_2: 57;

                      hence (p . j) = (s . j) by A536, A570, A583;

                    end;

                  end;

                end;

                then

                 A587: p = s by A568;

                

                 A588: ( Sum p) = (( Sum ((n |-> 0 qua Real) ^ q)) + ( Sum (L |-> 0 qua Real))) by A587, RVSUM_1: 75

                .= ((( Sum (n |-> 0 qua Real)) + ( Sum q)) + ( Sum (L |-> 0 qua Real))) by RVSUM_1: 75

                .= (( 0 + ( Sum q)) + ( Sum (L |-> 0 qua Real))) by RVSUM_1: 81

                .= ( 0 + ( Sum q)) by RVSUM_1: 81;

                

                thus ( Sum ST) = (( Sum F1) + ( Sum p)) by A150, A152, A153, RVSUM_1: 74

                .= ( Sum F) by A588, RVSUM_1: 75;

              end;

            end;

          end;

        end;

      end;

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

      hence thesis;

    end;

    

     Lm2: for A be non empty closed_interval Subset of REAL , rho be Function of A, REAL , T,S be Division of A, ST be FinSequence of REAL st rho is bounded_variation & ( len ST) = ( len S) & for j be Nat st j in ( dom S) holds ex p be FinSequence of REAL st (ST . j) = ( Sum p) & ( len p) = ( len T) & for i be Nat st i in ( dom T) holds (p . i) = |.( vol ((( divset (T,i)) /\ ( divset (S,j))),rho)).| holds ex H be Division of A, F be var_volume of rho, H st ( Sum ST) = ( Sum F)

    proof

      let A be non empty closed_interval Subset of REAL , rho be Function of A, REAL , T,S be Division of A, ST be FinSequence of REAL ;

      assume

       A1: rho is bounded_variation & ( len ST) = ( len S) & for j be Nat st j in ( dom S) holds ex p be FinSequence of REAL st (ST . j) = ( Sum p) & ( len p) = ( len T) & for i be Nat st i in ( dom T) holds (p . i) = |.( vol ((( divset (T,i)) /\ ( divset (S,j))),rho)).|;

      A c= A & ( lower_bound A) = ( lower_bound A);

      hence thesis by A1, Th18;

    end;

    theorem :: INTEGR23:17

    

     Th19: for A be non empty closed_interval Subset of REAL , rho be Function of A, REAL , T,S be Division of A st rho is bounded_variation holds ex ST be FinSequence of REAL st ( len ST) = ( len S) & ( Sum ST) <= ( total_vd rho) & for j be Nat st j in ( dom S) holds ex p be FinSequence of REAL st (ST . j) = ( Sum p) & ( len p) = ( len T) & for i be Nat st i in ( dom T) holds (p . i) = |.( vol ((( divset (T,i)) /\ ( divset (S,j))),rho)).|

    proof

      let A be non empty closed_interval Subset of REAL , rho be Function of A, REAL , T,S be Division of A;

      assume

       A1: rho is bounded_variation;

      defpred P[ Nat, object] means ex p be FinSequence of REAL st $2 = ( Sum p) & ( len p) = ( len T) & for i be Nat st i in ( dom T) holds (p . i) = |.( vol ((( divset (T,i)) /\ ( divset (S,$1))),rho)).|;

      

       A2: for j be Nat st j in ( Seg ( len S)) holds ex x be Element of REAL st P[j, x]

      proof

        let j be Nat;

        assume j in ( Seg ( len S));

        defpred Q[ Nat, object] means $2 = |.( vol ((( divset (T,$1)) /\ ( divset (S,j))),rho)).|;

        

         A3: for i be Nat st i in ( Seg ( len T)) holds ex y be Element of REAL st Q[i, y]

        proof

          let i be Nat;

          assume i in ( Seg ( len T));

           |.( vol ((( divset (T,i)) /\ ( divset (S,j))),rho)).| in REAL by XREAL_0:def 1;

          hence thesis;

        end;

        consider p be FinSequence of REAL such that

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

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

        

         Z2: ( dom T) = ( Seg ( len T)) by FINSEQ_1:def 3;

        ( len p) = ( len T) by A4, FINSEQ_1:def 3;

        then P[j, x] by A4, Z2;

        hence ex x be Element of REAL st P[j, x];

      end;

      consider ST be FinSequence of REAL such that

       A5: ( dom ST) = ( Seg ( len S)) & for j be Nat st j in ( Seg ( len S)) holds P[j, (ST . j)] from FINSEQ_1:sch 5( A2);

      take ST;

      thus

       A6: ( len ST) = ( len S) by A5, FINSEQ_1:def 3;

      

       a6: ( dom ST) = ( dom S) by A5, FINSEQ_1:def 3;

      then

      consider H be Division of A, F be var_volume of rho, H such that

       A7: ( Sum ST) = ( Sum F) by A1, A5, A6, Lm2;

      thus thesis by A1, A5, A7, INTEGR22: 5, a6;

    end;

    theorem :: INTEGR23:18

    

     Th20: for A be non empty closed_interval Subset of REAL , rho be Function of A, REAL , u be PartFunc of REAL , REAL st rho is bounded_variation & ( dom u) = A & (u | A) is uniformly_continuous holds for T be DivSequence of A, S be middle_volume_Sequence of rho, u, T st ( delta T) is convergent & ( lim ( delta T)) = 0 holds ( middle_sum S) is convergent

    proof

      let A be non empty closed_interval Subset of REAL , rho be Function of A, REAL , u be PartFunc of REAL , REAL ;

      assume that

       A1: rho is bounded_variation & ( dom u) = A and

       A2: (u | A) is uniformly_continuous;

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

      proof

        let T be DivSequence of A, S be middle_volume_Sequence of rho, u, T;

        assume

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

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

        

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

        proof

          let k be Element of NAT ;

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

          

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

          

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

          proof

            let i be Nat;

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

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

            then

            consider c be Real such that

             A8: c in ( rng (u | ( divset ((T . k),i)))) & ((S . k) . i) = (c * ( vol (( divset ((T . k),i)),rho))) by A1, INTEGR22:def 5;

            consider x be object such that

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

            reconsider x as Element of REAL by A9;

            take x;

            thus thesis by A8, A9;

          end;

          consider p be FinSequence of REAL such that

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

          take p;

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

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

        end;

        consider Fn be sequence of ( REAL * ) such that

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

        consider Fm be sequence of ( REAL * ) such that

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

        set TVD = ( total_vd rho);

        

         A13: 0 <= TVD by A1, INTEGR22: 6;

        now

          let p be Real;

          set pp2 = (p / 2);

          set pv = (pp2 / (TVD + 1));

          assume

           B13: p > 0 ;

          then

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

          then

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

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

          then (pv * TVD) < pp2 by A13, XCMPLX_1: 87;

          then

           A16: (pv * TVD) < p by A14, XXREAL_0: 2;

          set p2v = (pv / 2);

          consider sk be Real such that

           A17: 0 < sk & for x1,x2 be Real st x1 in ( dom (u | A)) & x2 in ( dom (u | A)) & |.(x1 - x2).| < sk holds |.(((u | A) . x1) - ((u | A) . x2)).| < p2v by A2, A15, FCONT_2:def 1, XREAL_1: 215;

          consider m be Nat such that

           A18: for i be Nat st m <= i holds |.((( delta T) . i) - 0 ).| < sk by A4, A17, SEQ_2:def 7;

          take m;

          let n be Nat;

          

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

          assume n >= m;

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

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

          then

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

          

           A21: (( middle_sum S) . n) = ( Sum (S . n)) & (( middle_sum S) . m) = ( Sum (S . m)) by INTEGR22:def 7;

          consider p1 be FinSequence of REAL such that

           A22: p1 = (Fn . n) & ( len p1) = ( len (T . n)) & for i be Nat st i in ( dom (T . n)) holds (p1 . i) in ( dom (u | ( divset ((T . n),i)))) & ex z be Real st z = ((u | ( divset ((T . n),i))) . (p1 . i)) & ((S . n) . i) = (z * ( vol (( divset ((T . n),i)),rho))) by A11, A19;

          consider p2 be FinSequence of REAL such that

           A23: p2 = (Fm . m) & ( len p2) = ( len (T . m)) & for i be Nat st i in ( dom (T . m)) holds (p2 . i) in ( dom (u | ( divset ((T . m),i)))) & ex z be Real st z = ((u | ( divset ((T . m),i))) . (p2 . i)) & ((S . m) . i) = (z * ( vol (( divset ((T . m),i)),rho))) by A12, A19;

          defpred H1[ object, object, object] means ex i,j be Nat, z be Real st $1 = i & $2 = j & z = ((u | ( divset ((T . n),i))) . (p1 . i)) & $3 = (( vol ((( divset ((T . n),i)) /\ ( divset ((T . m),j))),rho)) * z);

          

           A24: 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 REAL & H1[x, y, w]

          proof

            let x,y be object;

            assume

             A25: 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 A25, FINSEQ_1:def 3;

            then

            consider z be Real such that

             A26: z = ((u | ( divset ((T . n),i))) . (p1 . i)) & ((S . n) . i) = (z * ( vol (( divset ((T . n),i)),rho))) by A22;

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

            hence thesis by A26;

          end;

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

           A27: 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( A24);

          

           A28: for i,j be Nat st i in ( Seg ( len (T . n))) & j in ( Seg ( len (T . m))) holds ex z be Real st z = ((u | ( divset ((T . n),i))) . (p1 . i)) & (Snm . (i,j)) = (( vol ((( divset ((T . n),i)) /\ ( divset ((T . m),j))),rho)) * 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 Real st i = i1 & j = j1 & z = ((u | ( divset ((T . n),i1))) . (p1 . i1)) & (Snm . (i,j)) = (( vol ((( divset ((T . n),i1)) /\ ( divset ((T . m),j1))),rho)) * z) by A27;

            hence thesis;

          end;

          defpred P1[ Nat, object] means ex r be FinSequence of REAL 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));

          

           A29: 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

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

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

            consider r be FinSequence such that

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

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

            

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

            for j be Nat st j in ( dom r) holds (r . j) in REAL

            proof

              let j be Nat;

              assume

               A34: j in ( dom r);

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

              then (Snm . (k,j)) in REAL by FUNCT_2: 5;

              hence thesis by A32, A34;

            end;

            then

            reconsider r as FinSequence of REAL by FINSEQ_2: 12;

            take x = ( Sum r);

            thus thesis by A32, A33;

          end;

          consider Xp be FinSequence such that

           A35: ( 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( A29);

          for i be Nat st i in ( dom Xp) holds (Xp . i) in REAL

          proof

            let i be Nat;

            assume i in ( dom Xp);

            then ex r be FinSequence of REAL 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 A35;

            hence thesis by XREAL_0:def 1;

          end;

          then

          reconsider Xp as FinSequence of REAL by FINSEQ_2: 12;

          

           A36: ( len Xp) = ( len (T . n)) by A35, FINSEQ_1:def 3;

          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

             A38: k in ( Seg ( len Xp)) & k in ( Seg ( len (T . n))) by A36;

            then

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

            then

            consider z be Real such that

             A40: z = ((u | ( divset ((T . n),k))) . (p1 . k)) & ((S . n) . k) = (z * ( vol (( divset ((T . n),k)),rho))) by A22;

            consider r be FinSequence of REAL such that

             A41: ( 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, A38;

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

            

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

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

              hence thesis;

            end;

            consider vtntm be FinSequence of REAL such that

             A43: ( 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( A42);

            

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

            

             A45: ( len vtntm) = ( len r) & ( len (T . m)) = ( len r) by A41, A43, FINSEQ_1:def 3;

            then

             A46: ( Sum vtntm) = ( vol (( divset ((T . n),k)),rho)) by A39, A43, INTEGR22: 1, 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

               A47: j in ( dom r);

              then

               A48: ex w be Real st w = ((u | ( divset ((T . n),k))) . (p1 . k)) & (Snm . (k,j)) = (( vol ((( divset ((T . n),k)) /\ ( divset ((T . m),j))),rho)) * w) by A28, A38, A41;

              take (vtntm . j);

              (r . j) = (( vol ((( divset ((T . n),k)) /\ ( divset ((T . m),j))),rho)) * z) by A40, A41, A47, A48;

              hence thesis by A44, A47;

            end;

            hence thesis by A40, A41, A45, A46, Th1;

          end;

          then

           A49: Xp = (S . n) by A1, A36, INTEGR22:def 5;

          defpred P2[ Nat, object] means ex s be FinSequence of REAL 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));

          

           A50: 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

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

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

            consider s be FinSequence such that

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

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

            

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

            for i be Nat st i in ( dom s) holds (s . i) in REAL

            proof

              let i be Nat;

              assume

               A55: i in ( dom s);

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

              then (Snm . (i,k)) in REAL by FUNCT_2: 5;

              hence thesis by A53, A55;

            end;

            then

            reconsider s as FinSequence of REAL by FINSEQ_2: 12;

            take x = ( Sum s);

            thus thesis by A53, A54;

          end;

          consider Xq be FinSequence such that

           A56: ( 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( A50);

          for j be Nat st j in ( dom Xq) holds (Xq . j) in REAL

          proof

            let j be Nat;

            assume j in ( dom Xq);

            then ex s be FinSequence of REAL 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 A56;

            hence thesis by XREAL_0:def 1;

          end;

          then

          reconsider Xq as FinSequence of REAL by FINSEQ_2: 12;

          defpred H2[ object, object, object] means ex i,j be Nat, z be Real st $1 = i & $2 = j & z = ((u | ( divset ((T . m),j))) . (p2 . j)) & $3 = (( vol ((( divset ((T . n),i)) /\ ( divset ((T . m),j))),rho)) * z);

          

           A57: 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 REAL & H2[x, y, w]

          proof

            let x,y be object;

            assume

             A58: 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 A58, FINSEQ_1:def 3;

            then

            consider z be Real such that

             A59: z = ((u | ( divset ((T . m),j))) . (p2 . j)) & ((S . m) . j) = (z * ( vol (( divset ((T . m),j)),rho))) by A23;

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

            hence thesis by A59;

          end;

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

           A60: 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( A57);

          

           A61: for i,j be Nat st i in ( Seg ( len (T . n))) & j in ( Seg ( len (T . m))) holds ex z be Real st z = ((u | ( divset ((T . m),j))) . (p2 . j)) & (Smn . (i,j)) = (( vol ((( divset ((T . n),i)) /\ ( divset ((T . m),j))),rho)) * 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 Real st i = i1 & j = j1 & z = ((u | ( divset ((T . m),j1))) . (p2 . j1)) & (Smn . (i,j)) = (( vol ((( divset ((T . n),i1)) /\ ( divset ((T . m),j1))),rho)) * z) by A60;

            hence thesis;

          end;

          defpred P3[ Nat, object] means ex s be FinSequence of REAL 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));

          

           A62: 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

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

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

            consider s be FinSequence such that

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

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

            

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

            for i be Nat st i in ( dom s) holds (s . i) in REAL

            proof

              let i be Nat;

              assume

               A67: i in ( dom s);

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

              then (Smn . (i,k)) in REAL by FUNCT_2: 5;

              hence thesis by A65, A67;

            end;

            then

            reconsider s as FinSequence of REAL by FINSEQ_2: 12;

            take x = ( Sum s);

            thus thesis by A65, A66;

          end;

          consider Zq be FinSequence such that

           A68: ( 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( A62);

          for j be Nat st j in ( dom Zq) holds (Zq . j) in REAL

          proof

            let j be Nat;

            assume j in ( dom Zq);

            then ex s be FinSequence of REAL 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 A68;

            hence thesis by XREAL_0:def 1;

          end;

          then

          reconsider Zq as FinSequence of REAL by FINSEQ_2: 12;

          

           A69: ( len Zq) = ( len (T . m)) by A68, FINSEQ_1:def 3;

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

          proof

            let k be Nat;

            assume

             A71: 1 <= k <= ( len Zq);

            then

            consider s be FinSequence of REAL such that

             A72: ( 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 A68, FINSEQ_3: 25;

            

             A73: k in ( Seg ( len (T . m))) by A69, A71;

            

             A74: k in ( dom (T . m)) by A69, A71, FINSEQ_3: 25;

            then

            consider z be Real such that

             A75: z = ((u | ( divset ((T . m),k))) . (p2 . k)) & ((S . m) . k) = (z * ( vol (( divset ((T . m),k)),rho))) by A23;

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

            

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

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

              hence thesis;

            end;

            consider vtntm be FinSequence of REAL such that

             A77: ( 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( A76);

            

             A78: ( dom vtntm) = ( dom s) & ( len vtntm) = ( len s) by A77, FINSEQ_1:def 3;

            

             A79: for j be Nat st j in ( dom vtntm) holds (vtntm . j) = ( vol ((( divset ((T . m),k)) /\ ( divset ((T . n),j))),rho)) by A77;

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

            then

             A80: ( Sum vtntm) = ( vol (( divset ((T . m),k)),rho)) by A74, A78, A79, INTEGR22: 1, 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

               A81: j in ( dom s);

              then

               A82: ex w be Real st w = ((u | ( divset ((T . m),k))) . (p2 . k)) & (Smn . (j,k)) = (( vol ((( divset ((T . n),j)) /\ ( divset ((T . m),k))),rho)) * w) by A61, A72, A73;

              take (vtntm . j);

              (s . j) = (( vol ((( divset ((T . n),j)) /\ ( divset ((T . m),k))),rho)) * z) by A72, A75, A81, A82;

              hence thesis by A77, A78, A81;

            end;

            hence thesis by A72, A75, A78, A80, Th1;

          end;

          then Zq = (S . m) by A1, A69, INTEGR22:def 5;

          then

           A83: (( Sum (S . n)) - ( Sum (S . m))) = (( Sum Xq) - ( Sum Zq)) by A35, A49, A56, INTEGR22: 2;

          set XZq = (Xq - Zq);

          

           A84: ( dom XZq) = (( dom Xq) /\ ( dom Zq)) by VALUED_1: 12;

          reconsider XZq = (Xq - Zq) as FinSequence of REAL ;

          ( len Xq) = ( len Zq) by A56, A68, FINSEQ_3: 29;

          then

           A86: Xq is Element of (( len Xq) -tuples_on REAL ) & Zq is Element of (( len Xq) -tuples_on REAL ) by FINSEQ_2: 92;

          

           A87: for i,j be Nat, Snmij,Smnij be Real st i in ( Seg ( len (T . n))) & j in ( Seg ( len (T . m))) & Snmij = (Snm . (i,j)) & Smnij = (Smn . (i,j)) holds |.(Snmij - Smnij).| <= ( |.( vol ((( divset ((T . n),i)) /\ ( divset ((T . m),j))),rho)).| * pv)

          proof

            let i,j be Nat, Snmij,Smnij be Real;

            assume

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

            then

            consider z1 be Real such that

             A89: z1 = ((u | ( divset ((T . n),i))) . (p1 . i)) & (Snm . (i,j)) = (( vol ((( divset ((T . n),i)) /\ ( divset ((T . m),j))),rho)) * z1) by A28;

            consider z2 be Real such that

             A90: z2 = ((u | ( divset ((T . m),j))) . (p2 . j)) & (Smn . (i,j)) = (( vol ((( divset ((T . n),i)) /\ ( divset ((T . m),j))),rho)) * z2) by A61, A88;

            

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

            then

             A92: (p1 . i) in ( dom (u | ( divset ((T . n),i)))) & (p2 . j) in ( dom (u | ( divset ((T . m),j)))) by A22, A23;

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

            then

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

            

             A94: z1 = (u . (p1 . i)) & z2 = (u . (p2 . j)) by A89, A90, A92, FUNCT_1: 47;

            per cases ;

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

              then ( vol ((( divset ((T . n),i)) /\ ( divset ((T . m),j))),rho)) = 0 qua Real by INTEGR22:def 1;

              hence |.(Snmij - Smnij).| <= ( |.( vol ((( divset ((T . n),i)) /\ ( divset ((T . m),j))),rho)).| * pv) by A88, A89, A90, COMPLEX1: 44;

            end;

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

              then

              consider t be object such that

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

              reconsider t as Real by A97;

              

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

              

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

              then |.((p1 . i) - t).| < sk & |.(t - (p2 . j)).| < sk by A20, A91, A93, INTEGR20: 12;

              then

               A100: |.((u . (p1 . i)) - (u . t)).| < p2v & |.((u . t) - (u . (p2 . j))).| < p2v by A1, A17, A93, A98, A99;

              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) = ((( vol (DMN,rho)) * ((u . (p1 . i)) - (u . t))) + (( vol (DMN,rho)) * ((u . t) - (u . (p2 . j))))) by A88, A89, A90, A94;

              then

               A101: |.(Snmij - Smnij).| <= ( |.(( vol (DMN,rho)) * ((u . (p1 . i)) - (u . t))).| + |.(( vol (DMN,rho)) * ((u . t) - (u . (p2 . j)))).|) by COMPLEX1: 56;

              

               A102: |.(( vol (DMN,rho)) * ((u . (p1 . i)) - (u . t))).| = ( |.( vol (DMN,rho)).| * |.((u . (p1 . i)) - (u . t)).|) & |.(( vol (DMN,rho)) * ((u . t) - (u . (p2 . j)))).| = ( |.( vol (DMN,rho)).| * |.((u . t) - (u . (p2 . j))).|) by COMPLEX1: 65;

               0 <= |.( vol (DMN,rho)).| by COMPLEX1: 46;

              then |.(( vol (DMN,rho)) * ((u . (p1 . i)) - (u . t))).| <= ( |.( vol (DMN,rho)).| * p2v) & |.(( vol (DMN,rho)) * ((u . t) - (u . (p2 . j)))).| <= ( |.( vol (DMN,rho)).| * p2v) by A100, A102, XREAL_1: 64;

              then ( |.(( vol (DMN,rho)) * ((u . (p1 . i)) - (u . t))).| + |.(( vol (DMN,rho)) * ((u . t) - (u . (p2 . j)))).|) <= (( |.( vol (DMN,rho)).| * p2v) + ( |.( vol (DMN,rho)).| * p2v)) by XREAL_1: 7;

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

            end;

          end;

          consider vtntm be FinSequence of REAL such that

           A103: ( len vtntm) = ( len (T . m)) & ( Sum vtntm) <= ( total_vd rho) & for j be Nat st j in ( dom (T . m)) holds ex p be FinSequence of REAL st (vtntm . j) = ( Sum p) & ( len p) = ( len (T . n)) & for i be Nat st i in ( dom (T . n)) holds (p . i) = |.( vol ((( divset ((T . n),i)) /\ ( divset ((T . m),j))),rho)).| by A1, Th19;

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

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

          then ( dom PVD) = ( Seg ( len (T . m))) by A103, FINSEQ_1:def 3;

          then

           A104: ( len PVD) = ( len (T . m)) by FINSEQ_1:def 3;

          

           A105: for j be Nat st j in ( Seg ( len (T . m))) holds ex pvtntm be FinSequence of REAL st (PVD . j) = ( Sum pvtntm) & ( len pvtntm) = ( len (T . n)) & for i be Nat st i in ( Seg ( len (T . n))) holds (pvtntm . i) = (pv * |.( vol ((( divset ((T . n),i)) /\ ( divset ((T . m),j))),rho)).|)

          proof

            let j be Nat;

            assume j in ( Seg ( len (T . m)));

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

            then

            consider v be FinSequence of REAL such that

             A107: (vtntm . j) = ( Sum v) & ( len v) = ( len (T . n)) & for i be Nat st i in ( dom (T . n)) holds (v . i) = |.( vol ((( divset ((T . n),i)) /\ ( divset ((T . m),j))),rho)).| by A103;

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

            take pvtntm;

            

            thus (PVD . j) = (pv * (vtntm . j)) by VALUED_1: 6

            .= ( Sum pvtntm) by A107, RVSUM_1: 87;

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

            then ( dom pvtntm) = ( Seg ( len (T . n))) by A107, FINSEQ_1:def 3;

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

            let i be Nat;

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

            then

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

            

            thus (pvtntm . i) = (pv * (v . i)) by VALUED_1: 6

            .= (pv * |.( vol ((( divset ((T . n),i)) /\ ( divset ((T . m),j))),rho)).|) by A107, a108;

          end;

          

           A109: ( Sum PVD) = (pv * ( Sum vtntm)) by RVSUM_1: 87;

          

           A110: (pv * ( Sum vtntm)) <= (pv * ( total_vd rho)) by A13, B13, A103, XREAL_1: 64;

          

           A111: ( len XZq) = ( len (T . m)) by A56, A68, A84, FINSEQ_1:def 3;

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

          proof

            let j be Nat;

            assume

             A112: j in ( dom XZq);

            then

             A113: (XZq . j) = ((Xq . j) - (Zq . j)) by VALUED_1: 13;

            consider Xsq be FinSequence of REAL such that

             A114: ( 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 A56, A68, A84, A112;

            consider Zsq be FinSequence of REAL such that

             A115: ( 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 A56, A68, A84, A112;

            set XZsq = (Xsq - Zsq);

            

             A116: ( dom XZsq) = (( dom Xsq) /\ ( dom Zsq)) by VALUED_1: 12;

            reconsider XZsq as FinSequence of REAL ;

            

             A117: ( len XZsq) = ( len (T . n)) by A114, A115, A116, FINSEQ_1:def 3;

            consider pvtntm be FinSequence of REAL such that

             A118: (PVD . j) = ( Sum pvtntm) & ( len pvtntm) = ( len (T . n)) & for i be Nat st i in ( Seg ( len (T . n))) holds (pvtntm . i) = (pv * |.( vol ((( divset ((T . n),i)) /\ ( divset ((T . m),j))),rho)).|) by A105, A56, A68, A84, A112;

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

            proof

              let i be Nat;

              assume

               A119: i in ( dom XZsq);

              then

               A120: (XZsq . i) = ((Xsq . i) - (Zsq . i)) by VALUED_1: 13;

              

               A121: (pvtntm . i) = (pv * |.( vol ((( divset ((T . n),i)) /\ ( divset ((T . m),j))),rho)).|) by A118, A114, A115, A116, A119;

              (Xsq . i) = (Snm . (i,j)) & (Zsq . i) = (Smn . (i,j)) by A114, A115, A116, A119;

              hence |.(XZsq . i).| <= (pvtntm . i) by A56, A68, A84, A87, A112, A114, A115, A116, A119, A120, A121;

            end;

            then

             A122: |.( Sum XZsq).| <= (PVD . j) by A117, A118, Th3;

            ( len Xsq) = ( len Zsq) by A114, A115, FINSEQ_3: 29;

            then Xsq is Element of (( len Xsq) -tuples_on REAL ) & Zsq is Element of (( len Xsq) -tuples_on REAL ) by FINSEQ_2: 92;

            hence thesis by A113, A114, A115, A122, RVSUM_1: 90;

          end;

          then |.( Sum XZq).| <= ( Sum PVD) by A104, A111, Th3;

          then

           A124: |.( Sum XZq).| <= (TVD * pv) by A109, A110, XXREAL_0: 2;

          ( Sum XZq) = ((( middle_sum S) . n) - (( middle_sum S) . m)) by A21, A83, A86, RVSUM_1: 90;

          hence |.((( middle_sum S) . n) - (( middle_sum S) . m)).| < p by A16, A124, XXREAL_0: 2;

        end;

        hence ( middle_sum S) is convergent by SEQ_4: 41;

      end;

    end;

    theorem :: INTEGR23:19

    

     Th21: for A be non empty closed_interval Subset of REAL , rho be Function of A, REAL , u be PartFunc of REAL , REAL , T0,T,T1 be DivSequence of A, S0 be middle_volume_Sequence of rho, u, T0, S be middle_volume_Sequence of rho, u, 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 rho, u, T1 st for i be Nat holds (S1 . (2 * i)) = (S0 . i) & (S1 . ((2 * i) + 1)) = (S . i)

    proof

      let A be non empty closed_interval Subset of REAL , rho be Function of A, REAL , u be PartFunc of REAL , REAL , T0,T,T1 be DivSequence of A, S0 be middle_volume_Sequence of rho, u, T0, S be middle_volume_Sequence of rho, u, T;

      assume

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

      reconsider SS0 = S0, SS = S as sequence of ( REAL * );

      deffunc F( Nat) = ( In ((SS0 . $1),( REAL * )));

      deffunc G( Nat) = ( In ((SS . $1),( REAL * )));

      consider S1 be sequence of ( REAL * ) such that

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

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

      proof

        let i be Element of NAT ;

        consider k be Nat such that

         A4: i = (2 * k) or i = ((2 * k) + 1) by INTEGR20: 14;

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

        per cases by A4;

          suppose

           A5: i = (2 * k);

          

          then (S1 . i) = ( In ((SS0 . k),( REAL * ))) by A3

          .= (S0 . k) by FUNCT_2: 5, SUBSET_1:def 8;

          hence (S1 . i) is middle_volume of rho, u, (T1 . i) by A2, A5;

        end;

          suppose

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

          

          then (S1 . i) = ( In ((SS . k),( REAL * ))) by A3

          .= (S . k) by FUNCT_2: 5, SUBSET_1:def 8;

          hence (S1 . i) is middle_volume of rho, u, (T1 . i) by A2, A6;

        end;

      end;

      then

      reconsider S1 as middle_volume_Sequence of rho, u, T1 by INTEGR22:def 6;

      take S1;

      let i be Nat;

      

       A7: i is Element of NAT by ORDINAL1:def 12;

      

       A8: (S1 . (2 * i)) = ( In ((SS0 . i),( REAL * ))) by A3

      .= (S0 . i) by A7, FUNCT_2: 5, SUBSET_1:def 8;

      (S1 . ((2 * i) + 1)) = ( In ((SS . i),( REAL * ))) by A3

      .= (S . i) by A7, FUNCT_2: 5, SUBSET_1:def 8;

      hence thesis by A8;

    end;

    theorem :: INTEGR23:20

    

     Th22: for Sq0,Sq,Sq1 be Real_Sequence 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 Sq0,Sq,Sq1 be Real_Sequence;

      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, SEQ_2:def 7;

        consider k be Nat such that

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

        ((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 by SEQ_2:def 6;

      hence ( lim Sq0) = ( lim Sq1) by A3, SEQ_2: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, SEQ_2:def 7;

        consider k be Nat such that

         A9: m = (2 * k) or m = ((2 * k) + 1) by INTEGR20: 14;

        ((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 by SEQ_2:def 6;

      hence ( lim Sq) = ( lim Sq1) by SEQ_2:def 7, A7;

    end;

    theorem :: INTEGR23:21

    for A be non empty closed_interval Subset of REAL , rho be Function of A, REAL , u be continuous PartFunc of REAL , REAL st rho is bounded_variation & ( dom u) = A holds u is_RiemannStieltjes_integrable_with rho

    proof

      let A be non empty closed_interval Subset of REAL , rho be Function of A, REAL , u be continuous PartFunc of REAL , REAL ;

      assume

       A1: rho is bounded_variation & ( dom u) = A;

      

       A2: (u | A) is uniformly_continuous by A1, FCONT_2: 11;

      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 rho, u, T0;

      set I = ( lim ( middle_sum S0));

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

      proof

        let T be DivSequence of A, S be middle_volume_Sequence of rho, u, T;

        assume

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

        hence ( middle_sum S) is convergent by A1, A2, Th20;

        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 INTEGR20: 15;

        consider S1 be middle_volume_Sequence of rho, u, T1 such that

         A6: for i be Nat holds (S1 . (2 * i)) = (S0 . i) & (S1 . ((2 * i) + 1)) = (S . i) by A5, Th21;

        ( delta T1) is convergent & ( lim ( delta T1)) = 0 by A3, A4, A5, INTEGR20: 16;

        then

         A7: ( middle_sum S1) is convergent by A1, A2, Th20;

        

         A8: for i be Nat holds (( middle_sum S1) . (2 * i)) = (( middle_sum S0) . i) & (( middle_sum S1) . ((2 * i) + 1)) = (( middle_sum S) . i)

        proof

          let i be Nat;

          reconsider S1 as middle_volume_Sequence of rho, u, T1;

          (S1 . (2 * i)) = (S0 . i) & (T1 . (2 * i)) = (T0 . i) & (S1 . ((2 * i) + 1)) = (S . i) & (T1 . ((2 * i) + 1)) = (T . i) by A5, A6;

          then (( middle_sum S1) . (2 * i)) = ( Sum (S0 . i)) & (( middle_sum S1) . ((2 * i) + 1)) = ( Sum (S . i)) by INTEGR22:def 7;

          hence thesis by INTEGR22:def 7;

        end;

        ( lim ( middle_sum S)) = ( lim ( middle_sum S1)) by A7, A8, Th22;

        hence ( lim ( middle_sum S)) = ( lim ( middle_sum S0)) by A7, A8, Th22;

      end;

      hence u is_RiemannStieltjes_integrable_with rho by INTEGR22:def 8;

    end;