integra1.miz



    begin

    reserve a,a1,b,b1,x,y for Real,

F,G,H for FinSequence of REAL ,

i,j,k,n,m for Element of NAT ,

I for Subset of REAL ,

X for non empty set,

x1,R,s for set;

    reserve A for non empty closed_interval Subset of REAL ;

    registration

      cluster closed_interval -> compact for Subset of REAL ;

      coherence

      proof

        let IT be Subset of REAL ;

        assume IT is closed_interval;

        then ex a,b be Real st IT = [.a, b.] by MEASURE5:def 3;

        hence thesis by RCOMP_1: 6;

      end;

    end

    ::$Canceled

    theorem :: INTEGRA1:3

    

     Th1: A is bounded_below bounded_above

    proof

      A is real-bounded by RCOMP_1: 10;

      hence thesis;

    end;

    registration

      cluster non empty closed_interval -> real-bounded for Subset of REAL ;

      coherence by Th1;

    end

    reserve A,B for non empty closed_interval Subset of REAL ;

    theorem :: INTEGRA1:4

    

     Th2: A = [.( lower_bound A), ( upper_bound A).]

    proof

      consider a,b be Real such that

       A1: a <= b and

       A2: A = [.a, b.] by MEASURE5: 14;

      

       A3: for y be Real st 0 < y holds ex x be Real st x in A & (b - y) < x

      proof

        let y be Real;

        assume

         A4: 0 < y;

        take b;

        b < (b + y) by A4, XREAL_1: 29;

        then (b - y) < ((b + y) - y) by XREAL_1: 9;

        hence thesis by A1, A2, XXREAL_1: 1;

      end;

      

       A5: for x be Real st x in A holds x <= b

      proof

        let x be Real;

        assume

         A6: x in A;

        A = { y : a <= y & y <= b } by A2, RCOMP_1:def 1;

        then ex y st x = y & a <= y & y <= b by A6;

        hence thesis;

      end;

      

       A7: for x be Real st x in A holds a <= x

      proof

        let x be Real;

        assume

         A8: x in A;

        A = { y : a <= y & y <= b } by A2, RCOMP_1:def 1;

        then ex y st x = y & a <= y & y <= b by A8;

        hence thesis;

      end;

      for y be Real st 0 < y holds ex x be Real st x in A & x < (a + y)

      proof

        let y be Real;

        assume

         A9: 0 < y;

        take a;

        thus thesis by A1, A2, A9, XREAL_1: 29, XXREAL_1: 1;

      end;

      then a = ( lower_bound A) by A7, SEQ_4:def 2;

      hence thesis by A2, A5, A3, SEQ_4:def 1;

    end;

    theorem :: INTEGRA1:5

    

     Th3: for a1,a2,b1,b2 be Real holds A = [.a1, b1.] & A = [.a2, b2.] implies a1 = a2 & b1 = b2

    proof

      let a1,a2,b1,b2 be Real;

      assume that

       A1: A = [.a1, b1.] and

       A2: A = [.a2, b2.];

      a1 <= b1 by A1, XXREAL_1: 29;

      hence thesis by A1, A2, XXREAL_1: 66;

    end;

    begin

    definition

      ::$Canceled

      let A be non empty compact Subset of REAL ;

      :: INTEGRA1:def2

      mode Division of A -> non empty increasing FinSequence of REAL means

      : Def1: ( rng it ) c= A & (it . ( len it )) = ( upper_bound A);

      existence

      proof

        reconsider a = ( upper_bound A) as Element of REAL by XREAL_0:def 1;

        reconsider p = (( Seg 1) --> a) as Function of ( Seg 1), REAL by FUNCOP_1: 45;

        

         A1: ( dom p) = ( Seg 1) by FUNCOP_1: 13;

        ( rng p) c= REAL ;

        then

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

        

         A2: 1 in ( Seg 1) by FINSEQ_1: 2, TARSKI:def 1;

        for n,m be Nat st n in ( dom p) & m in ( dom p) & n < m holds (p . n) < (p . m)

        proof

          let n,m be Nat;

          assume that

           A3: n in ( dom p) and

           A4: m in ( dom p);

          n = 1 by A1, A3, FINSEQ_1: 2, TARSKI:def 1;

          hence thesis by A1, A4, FINSEQ_1: 2, TARSKI:def 1;

        end;

        then

         A5: p is non empty increasing FinSequence of REAL by SEQM_3:def 1;

        ( upper_bound A) in A by RCOMP_1: 14;

        then for n be Nat st n in ( Seg 1) holds (p . n) in A by FUNCOP_1: 7;

        then p is FinSequence of A by A1, FINSEQ_2: 12;

        then

         A6: ( rng p) c= A by FINSEQ_1:def 4;

        ( len p) = 1 by A1, FINSEQ_1:def 3;

        then (p . ( len p)) = ( upper_bound A) by A2, FUNCOP_1: 7;

        hence thesis by A6, A5;

      end;

    end

    definition

      let A be non empty compact Subset of REAL ;

      :: INTEGRA1:def3

      func divs A -> set means

      : Def2: x1 in it iff x1 is Division of A;

      existence

      proof

        defpred P[ set] means $1 is Division of A;

        consider R such that

         A1: x1 in R iff x1 in ( bool [: NAT , REAL :]) & P[x1] from XFAMILY:sch 1;

        take R;

        let x1;

        thus x1 in R implies x1 is Division of A by A1;

        assume x1 is Division of A;

        then

        reconsider p = x1 as Division of A;

        p c= [: NAT , REAL :];

        hence thesis by A1;

      end;

      uniqueness

      proof

        let D1,D2 be set such that

         A2: x1 in D1 iff x1 is Division of A and

         A3: x1 in D2 iff x1 is Division of A;

        now

          let x1 be object;

          thus x1 in D1 implies x1 in D2

          proof

            assume x1 in D1;

            then x1 is Division of A by A2;

            hence thesis by A3;

          end;

          assume x1 in D2;

          then x1 is Division of A by A3;

          hence x1 in D1 by A2;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    registration

      let A be non empty compact Subset of REAL ;

      cluster ( divs A) -> non empty;

      coherence

      proof

         the Division of A in ( divs A) by Def2;

        hence thesis;

      end;

    end

    registration

      let A be non empty compact Subset of REAL ;

      cluster -> Function-like Relation-like for Element of ( divs A);

      coherence by Def2;

    end

    registration

      let A be non empty compact Subset of REAL ;

      cluster -> real-valued FinSequence-like for Element of ( divs A);

      coherence by Def2;

    end

    reserve r for Real;

    reserve D,D1,D2 for Division of A;

    reserve f,g for Function of A, REAL ;

    theorem :: INTEGRA1:6

    

     Th4: i in ( dom D) implies (D . i) in A

    proof

      assume i in ( dom D);

      then

       A1: (D . i) in ( rng D) by FUNCT_1:def 3;

      ( rng D) c= A by Def1;

      hence thesis by A1;

    end;

    theorem :: INTEGRA1:7

    

     Th5: i in ( dom D) & i <> 1 implies (i - 1) in ( dom D) & (D . (i - 1)) in A & (i - 1) in NAT

    proof

      assume that

       A1: i in ( dom D) and

       A2: i <> 1;

      consider j be Nat such that

       A3: ( dom D) = ( Seg j) by FINSEQ_1:def 2;

      i <> 0 by A1, A3, FINSEQ_1: 1;

      then

       A4: i is non trivial by A2, NAT_2:def 1;

      then

      consider l be Nat such that

       A5: i = (2 + l) by NAT_1: 10, NAT_2: 29;

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

      i >= 2 by A4, NAT_2: 29;

      then

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

      i <= j by A1, A3, FINSEQ_1: 1;

      then

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

      

       A8: ( rng D) c= A by Def1;

      

       A9: (l + 1) = (i - (2 - 1)) by A5;

      then (i - 1) in ( dom D) by A3, A6, A7, FINSEQ_1: 1;

      then (D . (i - 1)) in ( rng D) by FUNCT_1:def 3;

      hence thesis by A3, A6, A7, A9, A8, FINSEQ_1: 1;

    end;

    definition

      let A be non empty closed_interval Subset of REAL ;

      let D be Division of A;

      let i be Nat;

      assume

       A1: i in ( dom D);

      :: INTEGRA1:def4

      func divset (D,i) -> non empty closed_interval Subset of REAL means

      : Def3: ( lower_bound it ) = ( lower_bound A) & ( upper_bound it ) = (D . i) if i = 1

      otherwise ( lower_bound it ) = (D . (i - 1)) & ( upper_bound it ) = (D . i);

      existence

      proof

        hereby

          assume i = 1;

          thus ex IT be non empty closed_interval Subset of REAL st ( lower_bound IT) = ( lower_bound A) & ( upper_bound IT) = (D . i)

          proof

            consider I such that

             A2: I = [.( lower_bound A), (D . i).];

            (D . i) in A by A1, Th4;

            then ( lower_bound A) <= (D . i) by SEQ_4:def 2;

            then

             A3: I is non empty closed_interval Subset of REAL by A2, MEASURE5: 14;

            then

             A4: I = [.( lower_bound I), ( upper_bound I).] by Th2;

            then

             A5: ( upper_bound I) = (D . i) by A2, A3, Th3;

            ( lower_bound I) = ( lower_bound A) by A2, A3, A4, Th3;

            hence thesis by A3, A5;

          end;

        end;

        assume that

         A6: i <> 1;

        thus ex IT be non empty closed_interval Subset of REAL st ( lower_bound IT) = (D . (i - 1)) & ( upper_bound IT) = (D . i)

        proof

          reconsider j = (i - 1) as Element of NAT by A1, A6, Th5;

          

           A7: (i + ( - 1)) < (i + (1 + ( - 1))) by XREAL_1: 6;

          consider a1, b1 such that

           A8: a1 = (D . (i - 1)) and

           A9: b1 = (D . i);

          consider I such that

           A10: I = [.a1, b1.];

          (i - 1) in ( dom D) by A1, A6, Th5;

          then (D . j) < (D . i) by A1, A7, SEQM_3:def 1;

          then

           A11: I is non empty closed_interval Subset of REAL by A8, A9, A10, MEASURE5: 14;

          then

           A12: I = [.( lower_bound I), ( upper_bound I).] by Th2;

          then

           A13: ( upper_bound I) = (D . i) by A9, A10, A11, Th3;

          ( lower_bound I) = (D . (i - 1)) by A8, A10, A11, A12, Th3;

          hence thesis by A11, A13;

        end;

      end;

      uniqueness

      proof

        let A1,A2 be non empty closed_interval Subset of REAL ;

        hereby

          consider b such that

           A14: b = (D . i);

          assume that i = 1 and

           A15: ( lower_bound A1) = ( lower_bound A) and

           A16: ( upper_bound A1) = (D . i) and

           A17: ( lower_bound A2) = ( lower_bound A) and

           A18: ( upper_bound A2) = (D . i);

          A1 = [.( lower_bound A), b.] by A15, A16, A14, Th2;

          hence A1 = A2 by A17, A18, A14, Th2;

        end;

        assume that i <> 1 and

         A19: ( lower_bound A1) = (D . (i - 1)) and

         A20: ( upper_bound A1) = (D . i) and

         A21: ( lower_bound A2) = (D . (i - 1)) and

         A22: ( upper_bound A2) = (D . i);

        consider a, b such that

         A23: a = (D . (i - 1)) and

         A24: b = (D . i);

        A1 = [.a, b.] by A19, A20, A23, A24, Th2;

        hence thesis by A21, A22, A23, A24, Th2;

      end;

      correctness ;

    end

    theorem :: INTEGRA1:8

    

     Th6: i in ( dom D) implies ( divset (D,i)) c= A

    proof

      assume

       A1: i in ( dom D);

      now

        per cases ;

          suppose

           A2: i = 1;

          ( lower_bound A) in A by RCOMP_1: 14;

          then

           A3: ( lower_bound A) in [.( lower_bound A), ( upper_bound A).] by Th2;

          

           A4: ( lower_bound ( divset (D,i))) = ( lower_bound A) by A1, A2, Def3;

          consider b such that

           A5: b = (D . i);

          ( upper_bound ( divset (D,i))) = b by A1, A2, A5, Def3;

          then

           A6: ( divset (D,i)) = [.( lower_bound A), b.] by A4, Th2;

          b in A by A1, A5, Th4;

          then b in [.( lower_bound A), ( upper_bound A).] by Th2;

          then [.( lower_bound A), b.] c= [.( lower_bound A), ( upper_bound A).] by A3, XXREAL_2:def 12;

          hence thesis by A6, Th2;

        end;

          suppose

           A7: i <> 1;

          set b = (D . i);

          b in A by A1, Th4;

          then

           A8: b in [.( lower_bound A), ( upper_bound A).] by Th2;

          set a = (D . (i - 1));

          (D . (i - 1)) in A by A1, A7, Th5;

          then a in [.( lower_bound A), ( upper_bound A).] by Th2;

          then

           A9: [.a, b.] c= [.( lower_bound A), ( upper_bound A).] by A8, XXREAL_2:def 12;

          

           A10: ( upper_bound ( divset (D,i))) = b by A1, A7, Def3;

          ( lower_bound ( divset (D,i))) = a by A1, A7, Def3;

          then ( divset (D,i)) = [.a, b.] by A10, Th2;

          hence thesis by A9, Th2;

        end;

      end;

      hence thesis;

    end;

    definition

      let A be Subset of REAL ;

      :: INTEGRA1:def5

      func vol (A) -> Real equals (( upper_bound A) - ( lower_bound A));

      correctness ;

    end

    theorem :: INTEGRA1:9

    for A be real-bounded non empty Subset of REAL holds 0 <= ( vol A) by SEQ_4: 11, XREAL_1: 48;

    begin

    definition

      let A be non empty closed_interval Subset of REAL ;

      let f be PartFunc of A, REAL ;

      let D be Division of A;

      :: INTEGRA1:def6

      func upper_volume (f,D) -> FinSequence of REAL means

      : Def5: ( len it ) = ( len D) & for i be Nat st i in ( dom D) holds (it . i) = (( upper_bound ( rng (f | ( divset (D,i))))) * ( vol ( divset (D,i))));

      existence

      proof

        deffunc F( Nat) = ( In ((( upper_bound ( rng (f | ( divset (D,$1))))) * ( vol ( divset (D,$1)))), REAL ));

        consider IT be FinSequence of REAL such that

         A1: ( len IT) = ( len D) & for i be Nat st i in ( dom IT) holds (IT . i) = F(i) from FINSEQ_2:sch 1;

        take IT;

        thus ( len IT) = ( len D) by A1;

        let i be Nat;

        

         A2: F(i) = (( upper_bound ( rng (f | ( divset (D,i))))) * ( vol ( divset (D,i))));

        assume i in ( dom D);

        then i in ( dom IT) by A1, FINSEQ_3: 29;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        let s1,s2 be FinSequence of REAL such that

         A3: ( len s1) = ( len D) and

         A4: for i be Nat st i in ( dom D) holds (s1 . i) = (( upper_bound ( rng (f | ( divset (D,i))))) * ( vol ( divset (D,i)))) and

         A5: ( len s2) = ( len D) and

         A6: for i be Nat st i in ( dom D) holds (s2 . i) = (( upper_bound ( rng (f | ( divset (D,i))))) * ( vol ( divset (D,i))));

        

         A7: ( dom s1) = ( dom D) by A3, FINSEQ_3: 29;

        for i be Nat st i in ( dom s1) holds (s1 . i) = (s2 . i)

        proof

          let i be Nat;

          assume

           A8: i in ( dom s1);

          then (s1 . i) = (( upper_bound ( rng (f | ( divset (D,i))))) * ( vol ( divset (D,i)))) by A4, A7;

          hence thesis by A6, A7, A8;

        end;

        hence thesis by A3, A5, FINSEQ_2: 9;

      end;

      :: INTEGRA1:def7

      func lower_volume (f,D) -> FinSequence of REAL means

      : Def6: ( len it ) = ( len D) & for i be Nat st i in ( dom D) holds (it . i) = (( lower_bound ( rng (f | ( divset (D,i))))) * ( vol ( divset (D,i))));

      existence

      proof

        deffunc F( Nat) = ( In ((( lower_bound ( rng (f | ( divset (D,$1))))) * ( vol ( divset (D,$1)))), REAL ));

        consider IT be FinSequence of REAL such that

         A9: ( len IT) = ( len D) & for i be Nat st i in ( dom IT) holds (IT . i) = F(i) from FINSEQ_2:sch 1;

        take IT;

        thus ( len IT) = ( len D) by A9;

        let i be Nat;

        

         A10: ( In ((( lower_bound ( rng (f | ( divset (D,i))))) * ( vol ( divset (D,i)))), REAL )) = (( lower_bound ( rng (f | ( divset (D,i))))) * ( vol ( divset (D,i))));

        assume i in ( dom D);

        then i in ( dom IT) by A9, FINSEQ_3: 29;

        hence thesis by A9, A10;

      end;

      uniqueness

      proof

        let s1,s2 be FinSequence of REAL such that

         A11: ( len s1) = ( len D) and

         A12: for i be Nat st i in ( dom D) holds (s1 . i) = (( lower_bound ( rng (f | ( divset (D,i))))) * ( vol ( divset (D,i)))) and

         A13: ( len s2) = ( len D) and

         A14: for i be Nat st i in ( dom D) holds (s2 . i) = (( lower_bound ( rng (f | ( divset (D,i))))) * ( vol ( divset (D,i))));

        

         A15: ( dom s1) = ( dom D) by A11, FINSEQ_3: 29;

        for i be Nat st i in ( dom s1) holds (s1 . i) = (s2 . i)

        proof

          let i be Nat;

          assume

           A16: i in ( dom s1);

          then (s1 . i) = (( lower_bound ( rng (f | ( divset (D,i))))) * ( vol ( divset (D,i)))) by A12, A15;

          hence thesis by A14, A15, A16;

        end;

        hence thesis by A11, A13, FINSEQ_2: 9;

      end;

    end

    definition

      let A be non empty closed_interval Subset of REAL ;

      let f be PartFunc of A, REAL ;

      let D be Division of A;

      :: INTEGRA1:def8

      func upper_sum (f,D) -> Real equals ( Sum ( upper_volume (f,D)));

      correctness ;

      :: INTEGRA1:def9

      func lower_sum (f,D) -> Real equals ( Sum ( lower_volume (f,D)));

      correctness ;

    end

    definition

      let A be non empty closed_interval Subset of REAL ;

      let f be PartFunc of A, REAL ;

      set S = ( divs A);

      :: INTEGRA1:def10

      func upper_sum_set (f) -> Function of ( divs A), REAL means

      : Def9: for D be Division of A holds (it . D) = ( upper_sum (f,D));

      existence

      proof

        defpred P[ Element of S, set] means ex D be Division of A st D = $1 & $2 = ( upper_sum (f,D));

        

         A1: for x be Element of S holds ex y be Element of REAL st P[x, y]

        proof

          let x be Element of S;

          reconsider x as Division of A by Def2;

          take ( upper_sum (f,x));

          thus thesis;

        end;

        consider g be Function of S, REAL such that

         A2: for x be Element of S holds P[x, (g . x)] from FUNCT_2:sch 3( A1);

        take g;

        let D be Division of A;

        reconsider D1 = D as Element of S by Def2;

         P[D1, (g . D1)] by A2;

        hence thesis;

      end;

      uniqueness

      proof

        let g1,g2 be Function of S, REAL such that

         A3: for D be Division of A holds (g1 . D) = ( upper_sum (f,D)) and

         A4: for D be Division of A holds (g2 . D) = ( upper_sum (f,D));

        let a be Element of S;

        reconsider d = a as Division of A by Def2;

        

        thus (g1 . a) = ( upper_sum (f,d)) by A3

        .= (g2 . a) by A4;

      end;

      :: INTEGRA1:def11

      func lower_sum_set (f) -> Function of ( divs A), REAL means

      : Def10: for D be Division of A holds (it . D) = ( lower_sum (f,D));

      existence

      proof

        defpred P[ Element of S, set] means ex D be Division of A st D = $1 & $2 = ( lower_sum (f,D));

        

         A5: for x be Element of S holds ex y be Element of REAL st P[x, y]

        proof

          let x be Element of S;

          reconsider x as Division of A by Def2;

          take ( lower_sum (f,x));

          thus thesis;

        end;

        consider g be Function of S, REAL such that

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

        take g;

        let D be Division of A;

        reconsider D1 = D as Element of S by Def2;

         P[D1, (g . D1)] by A6;

        hence thesis;

      end;

      uniqueness

      proof

        let g1,g2 be Function of S, REAL such that

         A7: for D be Division of A holds (g1 . D) = ( lower_sum (f,D)) and

         A8: for D be Division of A holds (g2 . D) = ( lower_sum (f,D));

        let a be Element of S;

        reconsider d = a as Division of A by Def2;

        

        thus (g1 . a) = ( lower_sum (f,d)) by A7

        .= (g2 . a) by A8;

      end;

    end

    definition

      let A be non empty closed_interval Subset of REAL ;

      let f be PartFunc of A, REAL ;

      :: INTEGRA1:def12

      attr f is upper_integrable means ( rng ( upper_sum_set f)) is bounded_below;

      :: INTEGRA1:def13

      attr f is lower_integrable means ( rng ( lower_sum_set f)) is bounded_above;

    end

    definition

      let A be non empty closed_interval Subset of REAL ;

      let f be PartFunc of A, REAL ;

      :: INTEGRA1:def14

      func upper_integral (f) -> Real equals ( lower_bound ( rng ( upper_sum_set f)));

      correctness ;

    end

    definition

      let A be non empty closed_interval Subset of REAL ;

      let f be PartFunc of A, REAL ;

      :: INTEGRA1:def15

      func lower_integral (f) -> Real equals ( upper_bound ( rng ( lower_sum_set f)));

      coherence ;

    end

    definition

      let A be non empty closed_interval Subset of REAL ;

      let f be PartFunc of A, REAL ;

      :: INTEGRA1:def16

      attr f is integrable means f is upper_integrable lower_integrable & ( upper_integral f) = ( lower_integral f);

    end

    definition

      let A be non empty closed_interval Subset of REAL ;

      let f be PartFunc of A, REAL ;

      :: INTEGRA1:def17

      func integral (f) -> Real equals ( upper_integral f);

      coherence ;

    end

    begin

    theorem :: INTEGRA1:10

    

     Th8: for f,g be PartFunc of X, REAL holds ( rng (f + g)) c= (( rng f) ++ ( rng g))

    proof

      let f,g be PartFunc of X, REAL ;

      let y be object;

      assume y in ( rng (f + g));

      then

      consider x1 be object such that

       A1: x1 in ( dom (f + g)) and

       A2: y = ((f + g) . x1) by FUNCT_1:def 3;

      

       A3: ( dom (f + g)) = (( dom f) /\ ( dom g)) by VALUED_1:def 1;

      then x1 in ( dom f) by A1, XBOOLE_0:def 4;

      then

       A4: (f . x1) in ( rng f) by FUNCT_1:def 3;

      x1 in ( dom g) by A1, A3, XBOOLE_0:def 4;

      then

       A5: (g . x1) in ( rng g) by FUNCT_1:def 3;

      ((f + g) . x1) = ((f . x1) + (g . x1)) by A1, VALUED_1:def 1;

      hence thesis by A2, A4, A5, MEMBER_1: 46;

    end;

    theorem :: INTEGRA1:11

    

     Th9: for f be real-valued Function holds f is bounded_below implies ( rng f) is bounded_below

    proof

      let f be real-valued Function;

      set X = ( dom f);

      

       AA: (f | X) = f;

      assume f is bounded_below;

      then

      consider a be Real such that

       A1: for x1 be object st x1 in (X /\ ( dom f)) holds a <= (f . x1) by AA, RFUNCT_1: 71;

      a is LowerBound of ( rng f)

      proof

        let y be ExtReal;

        assume y in ( rng f);

        then ex s be object st s in ( dom f) & y = (f . s) by FUNCT_1:def 3;

        hence thesis by A1;

      end;

      hence thesis;

    end;

    theorem :: INTEGRA1:12

    for f be real-valued Function st ( rng f) is bounded_below holds f is bounded_below

    proof

      let f be real-valued Function;

      set X = ( dom f);

      assume ( rng f) is bounded_below;

      then

      consider a be Real such that

       A1: a is LowerBound of ( rng f);

      

       AA: (f | X) = f;

      for x1 be object st x1 in (X /\ ( dom f)) holds a <= (f . x1)

      proof

        let x1 be object;

        assume x1 in (X /\ ( dom f));

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

        hence thesis by A1, XXREAL_2:def 2;

      end;

      hence thesis by AA, RFUNCT_1: 71;

    end;

    theorem :: INTEGRA1:13

    

     Th11: for f be real-valued Function st f is bounded_above holds ( rng f) is bounded_above

    proof

      let f be real-valued Function;

      set X = ( dom f);

      

       AA: (f | X) = f;

      assume f is bounded_above;

      then

      consider a be Real such that

       A1: for x1 be object st x1 in (X /\ ( dom f)) holds (f . x1) <= a by AA, RFUNCT_1: 70;

      a is UpperBound of ( rng f)

      proof

        let y be ExtReal;

        assume y in ( rng f);

        then ex s be object st s in ( dom f) & y = (f . s) by FUNCT_1:def 3;

        hence thesis by A1;

      end;

      hence thesis;

    end;

    theorem :: INTEGRA1:14

    for f be real-valued Function st ( rng f) is bounded_above holds f is bounded_above

    proof

      let f be real-valued Function;

      set X = ( dom f);

      assume ( rng f) is bounded_above;

      then

      consider a be Real such that

       A1: a is UpperBound of ( rng f);

      

       AA: (f | X) = f;

      for x1 be object st x1 in (X /\ ( dom f)) holds (f . x1) <= a

      proof

        let x1 be object;

        assume x1 in (X /\ ( dom f));

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

        hence thesis by A1, XXREAL_2:def 1;

      end;

      hence thesis by AA, RFUNCT_1: 70;

    end;

    theorem :: INTEGRA1:15

    for f be real-valued Function holds f is bounded implies ( rng f) is real-bounded by Th11, Th9;

    begin

    theorem :: INTEGRA1:16

    

     Th14: for A be non empty set holds (( chi (A,A)) | A) is constant

    proof

      let A be non empty set;

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

      for x be Element of A st x in (A /\ ( dom ( chi (A,A)))) holds (( chi (A,A)) /. x) = jj

      proof

        let x be Element of A;

        assume x in (A /\ ( dom ( chi (A,A))));

        then

         A1: x in ( dom ( chi (A,A))) by XBOOLE_0:def 4;

        (( chi (A,A)) . x) = 1 by FUNCT_3:def 3;

        hence thesis by A1, PARTFUN1:def 6;

      end;

      hence thesis by PARTFUN2: 35;

    end;

    theorem :: INTEGRA1:17

    

     Th15: for A be non empty Subset of X holds ( rng ( chi (A,A))) = {1}

    proof

      let A be non empty Subset of X;

      

       A1: (( chi (A,A)) | A) is constant by Th14;

      ( dom ( chi (A,A))) = A by FUNCT_3:def 3;

      then

       A2: A = (A /\ ( dom ( chi (A,A))));

      

       A3: ( dom ( chi (A,A))) = A by FUNCT_3:def 3;

      ex x be Element of X st x in ( dom ( chi (A,A))) & (( chi (A,A)) . x) = 1

      proof

        consider x be Element of X such that

         A4: x in ( dom ( chi (A,A))) by A3, SUBSET_1: 4;

        take x;

        thus thesis by A4, FUNCT_3:def 3;

      end;

      then

       A5: 1 in ( rng ( chi (A,A))) by FUNCT_1:def 3;

      A meets ( dom ( chi (A,A))) by A2;

      then ex y be Element of REAL st ( rng (( chi (A,A)) | A)) = {y} by A1, PARTFUN2: 37;

      hence thesis by A5, TARSKI:def 1;

    end;

    theorem :: INTEGRA1:18

    

     Th16: for A be non empty Subset of X, B be set holds B meets ( dom ( chi (A,A))) implies ( rng (( chi (A,A)) | B)) = {1}

    proof

      let A be non empty Subset of X;

      let B be set;

      

       A1: ( dom (( chi (A,A)) | B)) = (B /\ ( dom ( chi (A,A)))) by RELAT_1: 61;

      ( rng (( chi (A,A)) | B)) c= ( rng ( chi (A,A))) by RELAT_1: 70;

      then

       A2: ( rng (( chi (A,A)) | B)) c= {1} by Th15;

      assume (B /\ ( dom ( chi (A,A)))) <> {} ;

      then ( rng (( chi (A,A)) | B)) <> {} by A1, RELAT_1: 42;

      hence thesis by A2, ZFMISC_1: 33;

    end;

    theorem :: INTEGRA1:19

    

     Th17: i in ( dom D) implies ( vol ( divset (D,i))) = (( lower_volume (( chi (A,A)),D)) . i)

    proof

      

       A1: ( dom ( chi (A,A))) = A by FUNCT_3:def 3;

      assume

       A2: i in ( dom D);

      then

       A3: (( lower_volume (( chi (A,A)),D)) . i) = (( lower_bound ( rng (( chi (A,A)) | ( divset (D,i))))) * ( vol ( divset (D,i)))) by Def6;

      ( divset (D,i)) c= A by A2, Th6;

      then ( divset (D,i)) c= (( divset (D,i)) /\ ( dom ( chi (A,A)))) by A1, XBOOLE_1: 19;

      then (( divset (D,i)) /\ ( dom ( chi (A,A)))) <> {} ;

      then ( divset (D,i)) meets ( dom ( chi (A,A)));

      then

       A4: ( rng (( chi (A,A)) | ( divset (D,i)))) = {1} by Th16;

      

       A5: ( rng ( chi (A,A))) = {1} by Th15;

      then ( lower_bound ( rng ( chi (A,A)))) = 1 by SEQ_4: 9;

      hence thesis by A3, A5, A4;

    end;

    theorem :: INTEGRA1:20

    

     Th18: i in ( dom D) implies ( vol ( divset (D,i))) = (( upper_volume (( chi (A,A)),D)) . i)

    proof

      

       A1: ( dom ( chi (A,A))) = A by FUNCT_3:def 3;

      assume

       A2: i in ( dom D);

      then

       A3: (( upper_volume (( chi (A,A)),D)) . i) = (( upper_bound ( rng (( chi (A,A)) | ( divset (D,i))))) * ( vol ( divset (D,i)))) by Def5;

      ( divset (D,i)) c= A by A2, Th6;

      then ( divset (D,i)) c= (( divset (D,i)) /\ ( dom ( chi (A,A)))) by A1, XBOOLE_1: 19;

      then (( divset (D,i)) /\ ( dom ( chi (A,A)))) <> {} ;

      then ( divset (D,i)) meets ( dom ( chi (A,A)));

      then

       A4: ( rng (( chi (A,A)) | ( divset (D,i)))) = {1} by Th16;

      

       A5: ( rng ( chi (A,A))) = {1} by Th15;

      then ( upper_bound ( rng ( chi (A,A)))) = 1 by SEQ_4: 9;

      hence thesis by A3, A5, A4;

    end;

    theorem :: INTEGRA1:21

    ( len F) = ( len G) & ( len F) = ( len H) & (for k st k in ( dom F) holds (H . k) = ((F /. k) + (G /. k))) implies ( Sum H) = (( Sum F) + ( Sum G))

    proof

      assume that

       A1: ( len F) = ( len G) and

       A2: ( len F) = ( len H) and

       A3: for k st k in ( dom F) holds (H . k) = ((F /. k) + (G /. k));

      

       A4: F is Element of (( len F) -tuples_on REAL ) by FINSEQ_2: 92;

      

       A5: G is Element of (( len F) -tuples_on REAL ) by A1, FINSEQ_2: 92;

      then (F + G) is Element of (( len F) -tuples_on REAL ) by A4, FINSEQ_2: 120;

      then

       A6: ( len H) = ( len (F + G)) by A2, CARD_1:def 7;

      then

       A7: ( dom H) = ( Seg ( len (F + G))) by FINSEQ_1:def 3;

      

       A8: for k st k in ( dom F) holds (H . k) = ((F . k) + (G . k))

      proof

        let k;

        assume

         A9: k in ( dom F);

        then k in ( Seg ( len G)) by A1, FINSEQ_1:def 3;

        then k in ( dom G) by FINSEQ_1:def 3;

        then

         A10: (G /. k) = (G . k) by PARTFUN1:def 6;

        (F /. k) = (F . k) by A9, PARTFUN1:def 6;

        hence thesis by A3, A9, A10;

      end;

      for k be Nat st k in ( dom H) holds (H . k) = ((F + G) . k)

      proof

        let k be Nat;

        assume

         A11: k in ( dom H);

        then k in ( dom F) by A2, A6, A7, FINSEQ_1:def 3;

        then

         A12: (H . k) = ((F . k) + (G . k)) by A8;

        k in ( dom (F + G)) by A7, A11, FINSEQ_1:def 3;

        hence thesis by A12, VALUED_1:def 1;

      end;

      

      then ( Sum H) = ( Sum (F + G)) by A6, FINSEQ_2: 9

      .= (( Sum F) + ( Sum G)) by A4, A5, RVSUM_1: 89;

      hence thesis;

    end;

    theorem :: INTEGRA1:22

    

     Th20: ( len F) = ( len G) & ( len F) = ( len H) & (for k st k in ( dom F) holds (H . k) = ((F /. k) - (G /. k))) implies ( Sum H) = (( Sum F) - ( Sum G))

    proof

      assume that

       A1: ( len F) = ( len G) and

       A2: ( len F) = ( len H) and

       A3: for k st k in ( dom F) holds (H . k) = ((F /. k) - (G /. k));

      

       A4: F is Element of (( len F) -tuples_on REAL ) by FINSEQ_2: 92;

      

       A5: G is Element of (( len F) -tuples_on REAL ) by A1, FINSEQ_2: 92;

      then

       A6: (F - G) is Element of (( len F) -tuples_on REAL ) by A4, FINSEQ_2: 120;

      then

       A7: ( len H) = ( len (F - G)) by A2, CARD_1:def 7;

      then

       A8: ( dom H) = ( Seg ( len (F - G))) by FINSEQ_1:def 3;

      

       A9: for k st k in ( dom F) holds (H . k) = ((F . k) - (G . k))

      proof

        let k;

        assume

         A10: k in ( dom F);

        then k in ( Seg ( len G)) by A1, FINSEQ_1:def 3;

        then k in ( dom G) by FINSEQ_1:def 3;

        then

         A11: (G /. k) = (G . k) by PARTFUN1:def 6;

        (F /. k) = (F . k) by A10, PARTFUN1:def 6;

        hence thesis by A3, A10, A11;

      end;

      for k be Nat st k in ( dom H) holds (H . k) = ((F - G) . k)

      proof

        let k be Nat;

        assume

         A12: k in ( dom H);

        then k in ( Seg ( len F)) by A6, A8, CARD_1:def 7;

        then k in ( dom F) by FINSEQ_1:def 3;

        then

         A13: (H . k) = ((F . k) - (G . k)) by A9;

        k in ( dom (F - G)) by A8, A12, FINSEQ_1:def 3;

        hence thesis by A13, VALUED_1: 13;

      end;

      

      then ( Sum H) = ( Sum (F - G)) by A7, FINSEQ_2: 9

      .= (( Sum F) - ( Sum G)) by A4, A5, RVSUM_1: 90;

      hence thesis;

    end;

    theorem :: INTEGRA1:23

    

     Th21: ( Sum ( lower_volume (( chi (A,A)),D))) = ( vol A)

    proof

      deffunc F( Nat) = ( In (( vol ( divset (D,$1))), REAL ));

      consider p be FinSequence of REAL such that

       A1: ( len p) = ( len D) & for i be Nat st i in ( dom p) holds (p . i) = F(i) from FINSEQ_2:sch 1;

      

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

      

       A3: for i st i in ( Seg ( len D)) holds (p . i) = (( upper_bound ( divset (D,i))) - ( lower_bound ( divset (D,i))))

      proof

        let i;

        

         A4: ( In (( vol ( divset (D,i))), REAL )) = ( vol ( divset (D,i)));

        assume i in ( Seg ( len D));

        hence thesis by A1, A2, A4;

      end;

      (( len D) - 1) in NAT

      proof

        ex j be Nat st ( len D) = (1 + j) by NAT_1: 10, NAT_1: 14;

        hence thesis by ORDINAL1:def 12;

      end;

      then

      reconsider k = (( len D) - 1) as Element of NAT ;

      deffunc G( Nat) = ( In (( lower_bound ( divset (D,($1 + 1)))), REAL ));

      deffunc F( Nat) = ( In (( upper_bound ( divset (D,$1))), REAL ));

      consider s1 be FinSequence of REAL such that

       A5: ( len s1) = k & for i be Nat st i in ( dom s1) holds (s1 . i) = F(i) from FINSEQ_2:sch 1;

      consider s2 be FinSequence of REAL such that

       A6: ( len s2) = k & for i be Nat st i in ( dom s2) holds (s2 . i) = G(i) from FINSEQ_2:sch 1;

      

       A7: ( dom s2) = ( Seg k) by A6, FINSEQ_1:def 3;

      reconsider ub = ( upper_bound A), lb = ( lower_bound A) as Element of REAL by XREAL_0:def 1;

      ( len (s1 ^ <*( upper_bound A)*>)) = ( len ( <*( lower_bound A)*> ^ s2)) & ( len (s1 ^ <*( upper_bound A)*>)) = ( len p) & for i st i in ( dom (s1 ^ <*( upper_bound A)*>)) holds (p . i) = (((s1 ^ <*ub*>) /. i) - (( <*lb*> ^ s2) /. i))

      proof

        ( dom <*( upper_bound A)*>) = ( Seg 1) by FINSEQ_1:def 8;

        then ( len <*( upper_bound A)*>) = 1 by FINSEQ_1:def 3;

        then

         A8: ( len (s1 ^ <*( upper_bound A)*>)) = (k + 1) by A5, FINSEQ_1: 22;

        ( dom <*( lower_bound A)*>) = ( Seg 1) by FINSEQ_1:def 8;

        then ( len <*( lower_bound A)*>) = 1 by FINSEQ_1:def 3;

        hence

         A9: ( len (s1 ^ <*( upper_bound A)*>)) = ( len ( <*( lower_bound A)*> ^ s2)) by A6, A8, FINSEQ_1: 22;

        thus ( len (s1 ^ <*( upper_bound A)*>)) = ( len p) by A1, A8;

        let i;

        

         A10: ( In (( upper_bound ( divset (D,i))), REAL )) = ( upper_bound ( divset (D,i)));

        

         A11: ( In (( lower_bound ( divset (D,i))), REAL )) = ( lower_bound ( divset (D,i)));

        assume

         A12: i in ( dom (s1 ^ <*( upper_bound A)*>));

        then

         A13: ((s1 ^ <*ub*>) /. i) = ((s1 ^ <*ub*>) . i) by PARTFUN1:def 6;

        i in ( Seg ( len (s1 ^ <*( upper_bound A)*>))) by A12, FINSEQ_1:def 3;

        then i in ( dom ( <*( lower_bound A)*> ^ s2)) by A9, FINSEQ_1:def 3;

        then

         A14: (( <*lb*> ^ s2) /. i) = (( <*( lower_bound A)*> ^ s2) . i) by PARTFUN1:def 6;

        

         A15: ( len D) = 1 or ( len D) is non trivial by NAT_2:def 1;

        now

          per cases by A15, NAT_2: 29;

            suppose

             A16: ( len D) = 1;

            then

             A17: i in ( Seg 1) by A8, A12, FINSEQ_1:def 3;

            then

             A18: i = 1 by FINSEQ_1: 2, TARSKI:def 1;

            s1 = {} by A5, A16;

            then (s1 ^ <*( upper_bound A)*>) = <*( upper_bound A)*> by FINSEQ_1: 34;

            then

             A19: ((s1 ^ <*ub*>) /. i) = ( upper_bound A) by A13, A18, FINSEQ_1:def 8;

            

             A20: i in ( dom D) by A16, A17, FINSEQ_1:def 3;

            s2 = {} by A6, A16;

            then ( <*( lower_bound A)*> ^ s2) = <*( lower_bound A)*> by FINSEQ_1: 34;

            then

             A21: (( <*lb*> ^ s2) /. i) = ( lower_bound A) by A14, A18, FINSEQ_1:def 8;

            (D . i) = ( upper_bound A) by A16, A18, Def1;

            then

             A22: ( upper_bound ( divset (D,i))) = ( upper_bound A) by A18, A20, Def3;

            (p . i) = (( upper_bound ( divset (D,i))) - ( lower_bound ( divset (D,i)))) by A3, A16, A17;

            hence thesis by A18, A20, A19, A21, A22, Def3;

          end;

            suppose

             A23: ( len D) >= 2;

            1 = (2 - 1);

            then

             A24: k >= 1 by A23, XREAL_1: 9;

            now

              per cases ;

                suppose

                 A25: i = 1;

                then

                 A26: i in ( Seg 1) by FINSEQ_1: 2, TARSKI:def 1;

                then i in ( dom <*( lower_bound A)*>) by FINSEQ_1:def 8;

                then (( <*( lower_bound A)*> ^ s2) . i) = ( <*( lower_bound A)*> . i) by FINSEQ_1:def 7;

                then

                 A27: (( <*( lower_bound A)*> ^ s2) . i) = ( lower_bound A) by A25, FINSEQ_1:def 8;

                ( Seg 1) c= ( Seg k) by A24, FINSEQ_1: 5;

                then i in ( Seg k) by A26;

                then

                 A28: i in ( dom s1) by A5, FINSEQ_1:def 3;

                then ((s1 ^ <*( upper_bound A)*>) . i) = (s1 . i) by FINSEQ_1:def 7;

                then

                 A29: ((s1 ^ <*ub*>) . i) = ( upper_bound ( divset (D,i))) by A5, A28, A10;

                

                 A30: i in ( Seg 2) by A25, FINSEQ_1: 2, TARSKI:def 2;

                

                 A31: ( Seg 2) c= ( Seg ( len D)) by A23, FINSEQ_1: 5;

                then i in ( Seg ( len D)) by A30;

                then

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

                (p . i) = (( upper_bound ( divset (D,i))) - ( lower_bound ( divset (D,i)))) by A3, A31, A30;

                hence thesis by A13, A14, A25, A32, A29, A27, Def3;

              end;

                suppose

                 A33: i = ( len D);

                then (i - ( len s1)) in ( Seg 1) by A5, FINSEQ_1: 2, TARSKI:def 1;

                then

                 A34: (i - ( len s1)) in ( dom <*( upper_bound A)*>) by FINSEQ_1:def 8;

                i = ((i - ( len s1)) + ( len s1));

                then ((s1 ^ <*( upper_bound A)*>) . i) = ( <*( upper_bound A)*> . (i - ( len s1))) by A34, FINSEQ_1:def 7;

                then

                 A35: ((s1 ^ <*ub*>) /. i) = ( upper_bound A) by A5, A13, A33, FINSEQ_1:def 8;

                

                 A36: i <> 1 by A23, A33;

                i in ( Seg ( len D)) by A33, FINSEQ_1: 3;

                then

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

                (p . i) = (( upper_bound ( divset (D,i))) - ( lower_bound ( divset (D,i)))) by A3, A33, FINSEQ_1: 3;

                then (p . i) = (( upper_bound ( divset (D,i))) - (D . (i - 1))) by A37, A36, Def3;

                then

                 A38: (p . i) = ((D . i) - (D . (i - 1))) by A37, A36, Def3;

                

                 A39: (i - ( len <*( lower_bound A)*>)) = (i - 1) by FINSEQ_1: 40;

                (i - 1) <> 0 by A23, A33;

                then

                 A40: (i - 1) in ( Seg k) by A33, FINSEQ_1: 3;

                then

                 A41: (i - ( len <*( lower_bound A)*>)) in ( dom s2) by A6, A39, FINSEQ_1:def 3;

                (( len <*( lower_bound A)*>) + (i - ( len <*( lower_bound A)*>))) = i;

                then

                 A42: (( <*lb*> ^ s2) . i) = (s2 . (i - 1)) by A41, A39, FINSEQ_1:def 7;

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

                (( <*lb*> ^ s2) . i) = G(i1) by A6, A39, A41, A42

                .= ( lower_bound ( divset (D,i)));

                then (( <*( lower_bound A)*> ^ s2) . i) = (D . (i - 1)) by A37, A36, Def3;

                hence thesis by A14, A33, A35, A38, Def1;

              end;

                suppose

                 A43: i <> 1 & i <> ( len D);

                (( len s1) + ( len <*( upper_bound A)*>)) = (k + 1) by A5, FINSEQ_1: 39;

                then

                 A44: i in ( Seg ( len D)) by A12, FINSEQ_1:def 7;

                

                 A45: i in ( dom s1) & i in ( Seg k) & (i - 1) in ( Seg k) & ((i - 1) + 1) = i & (i - ( len <*( lower_bound A)*>)) in ( dom s2)

                proof

                  i <> 0 by A44, FINSEQ_1: 1;

                  then i is non trivial by A43, NAT_2:def 1;

                  then i >= (1 + 1) by NAT_2: 29;

                  then

                   A46: (i - 1) >= 1 by XREAL_1: 19;

                  

                   A47: 1 <= i by A44, FINSEQ_1: 1;

                  i <= ( len D) by A44, FINSEQ_1: 1;

                  then

                   A48: i < (k + 1) by A43, XXREAL_0: 1;

                  then

                   A49: i <= k by NAT_1: 13;

                  then i in ( Seg ( len s1)) by A5, A47, FINSEQ_1: 1;

                  hence i in ( dom s1) by FINSEQ_1:def 3;

                  thus i in ( Seg k) by A47, A49, FINSEQ_1: 1;

                  i <= k by A48, NAT_1: 13;

                  then (i - 1) <= (k - 1) by XREAL_1: 9;

                  then

                   A50: ((i - 1) + 0 ) <= ((k - 1) + 1) by XREAL_1: 7;

                  ex j be Nat st i = (1 + j) by A47, NAT_1: 10;

                  hence (i - 1) in ( Seg k) by A46, A50, FINSEQ_1: 1;

                  then

                   A51: (i - ( len <*( lower_bound A)*>)) in ( Seg ( len s2)) by A6, FINSEQ_1: 39;

                  thus ((i - 1) + 1) = i;

                  thus thesis by A51, FINSEQ_1:def 3;

                end;

                then

                 A52: (i - ( len <*( lower_bound A)*>)) in ( Seg ( len s2)) by FINSEQ_1:def 3;

                then (i - ( len <*( lower_bound A)*>)) <= ( len s2) by FINSEQ_1: 1;

                then

                 A53: i <= (( len <*( lower_bound A)*>) + ( len s2)) by XREAL_1: 20;

                1 <= (i - ( len <*( lower_bound A)*>)) by A52, FINSEQ_1: 1;

                then (( len <*( lower_bound A)*>) + 1) <= i by XREAL_1: 19;

                then (( <*( lower_bound A)*> ^ s2) . i) = (s2 . (i - ( len <*( lower_bound A)*>))) by A53, FINSEQ_1: 23;

                then (( <*( lower_bound A)*> ^ s2) . i) = (s2 . (i - 1)) by FINSEQ_1: 39;

                then

                 A54: (( <*( lower_bound A)*> ^ s2) . i) = ( lower_bound ( divset (D,i))) by A6, A7, A45, A11;

                ((s1 ^ <*( upper_bound A)*>) . i) = (s1 . i) by A45, FINSEQ_1:def 7;

                then ((s1 ^ <*( upper_bound A)*>) . i) = ( upper_bound ( divset (D,i))) by A5, A45, A10;

                hence thesis by A3, A13, A14, A44, A54;

              end;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      then ( Sum p) = (( Sum (s1 ^ <*ub*>)) - ( Sum ( <*lb*> ^ s2))) by Th20;

      then ( Sum p) = ((( Sum s1) + ( upper_bound A)) - ( Sum ( <*lb*> ^ s2))) by RVSUM_1: 74;

      then

       A55: ( Sum p) = ((( Sum s1) + ( upper_bound A)) - (( lower_bound A) + ( Sum s2))) by RVSUM_1: 76;

      

       A56: ( dom s1) = ( Seg k) by A5, FINSEQ_1:def 3;

      

       A57: for i st i in ( Seg k) holds ( upper_bound ( divset (D,i))) = ( lower_bound ( divset (D,(i + 1))))

      proof

        let i;

        

         A58: (1 + 0 ) <= (i + 1) by XREAL_1: 7;

        assume

         A59: i in ( Seg k);

        then i <= k by FINSEQ_1: 1;

        then (i + 1) <= (k + 1) by XREAL_1: 7;

        then (i + 1) in ( Seg ( len D)) by A58, FINSEQ_1: 1;

        then

         A60: (i + 1) in ( dom D) by FINSEQ_1:def 3;

        (k + 1) = ( len D);

        then k <= ( len D) by NAT_1: 11;

        then ( Seg k) c= ( Seg ( len D)) by FINSEQ_1: 5;

        then i in ( Seg ( len D)) by A59;

        then

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

        

         A62: ((i + 1) - 1) = i;

        now

          per cases ;

            suppose

             A63: i = 1;

            then ( upper_bound ( divset (D,i))) = (D . i) by A61, Def3;

            hence thesis by A60, A62, A63, Def3;

          end;

            suppose

             A64: i <> 1;

            i >= 1 by A59, FINSEQ_1: 1;

            then (i + 1) >= (1 + 1) by XREAL_1: 6;

            then

             A65: (i + 1) <> 1;

            ( upper_bound ( divset (D,i))) = (D . i) by A61, A64, Def3;

            hence thesis by A60, A62, A65, Def3;

          end;

        end;

        hence thesis;

      end;

      for i be Nat st i in ( dom s1) holds (s1 . i) = (s2 . i)

      proof

        let i be Nat;

        

         A66: ( In (( upper_bound ( divset (D,i))), REAL )) = ( upper_bound ( divset (D,i)));

        

         A67: ( In (( lower_bound ( divset (D,(i + 1)))), REAL )) = ( lower_bound ( divset (D,(i + 1))));

        assume

         A68: i in ( dom s1);

        then (s1 . i) = ( upper_bound ( divset (D,i))) by A5, A66;

        then (s1 . i) = ( lower_bound ( divset (D,(i + 1)))) by A57, A56, A68;

        hence thesis by A6, A7, A56, A68, A67;

      end;

      then

       A69: s1 = s2 by A5, A6, FINSEQ_2: 9;

      

       A70: ( len ( lower_volume (( chi (A,A)),D))) = ( len D) by Def6;

      then

       A71: ( dom ( lower_volume (( chi (A,A)),D))) = ( Seg ( len D)) by FINSEQ_1:def 3;

      for i be Nat st i in ( dom ( lower_volume (( chi (A,A)),D))) holds (( lower_volume (( chi (A,A)),D)) . i) = (p . i)

      proof

        let i be Nat;

        

         A72: ( In (( vol ( divset (D,i))), REAL )) = ( vol ( divset (D,i)));

        assume

         A73: i in ( dom ( lower_volume (( chi (A,A)),D)));

        then i in ( dom D) by A70, FINSEQ_3: 29;

        then (( lower_volume (( chi (A,A)),D)) . i) = ( vol ( divset (D,i))) by Th17;

        hence thesis by A1, A2, A71, A73, A72;

      end;

      hence thesis by A1, A69, A55, A70, FINSEQ_2: 9;

    end;

    theorem :: INTEGRA1:24

    

     Th22: ( Sum ( upper_volume (( chi (A,A)),D))) = ( vol A)

    proof

      

       A1: for i be Nat st 1 <= i & i <= ( len ( lower_volume (( chi (A,A)),D))) holds (( lower_volume (( chi (A,A)),D)) . i) = (( upper_volume (( chi (A,A)),D)) . i)

      proof

        let i be Nat;

        assume that

         A2: 1 <= i and

         A3: i <= ( len ( lower_volume (( chi (A,A)),D)));

        i <= ( len D) by A3, Def6;

        then

         A4: i in ( dom D) by A2, FINSEQ_3: 25;

        

        then (( lower_volume (( chi (A,A)),D)) . i) = ( vol ( divset (D,i))) by Th17

        .= (( upper_volume (( chi (A,A)),D)) . i) by A4, Th18;

        hence thesis;

      end;

      ( len ( lower_volume (( chi (A,A)),D))) = ( len D) by Def6

      .= ( len ( upper_volume (( chi (A,A)),D))) by Def5;

      then ( lower_volume (( chi (A,A)),D)) = ( upper_volume (( chi (A,A)),D)) by A1, FINSEQ_1: 14;

      hence thesis by Th21;

    end;

    begin

    registration

      let A be non empty closed_interval Subset of REAL ;

      let f be PartFunc of A, REAL ;

      let D be Division of A;

      cluster ( upper_volume (f,D)) -> non empty;

      coherence

      proof

        ( len ( upper_volume (f,D))) = ( len D) by Def5;

        hence thesis;

      end;

      cluster ( lower_volume (f,D)) -> non empty;

      coherence

      proof

        ( len ( lower_volume (f,D))) = ( len D) by Def6;

        hence thesis;

      end;

    end

    theorem :: INTEGRA1:25

    

     Th23: (f | A) is bounded_below implies (( lower_bound ( rng f)) * ( vol A)) <= ( lower_sum (f,D))

    proof

      assume

       A1: (f | A) is bounded_below;

      

       A2: for i st i in ( dom D) holds (( lower_bound ( rng f)) * ( vol ( divset (D,i)))) <= (( lower_bound ( rng (f | ( divset (D,i))))) * ( vol ( divset (D,i))))

      proof

        let i;

        

         A3: ( rng (f | ( divset (D,i)))) c= ( rng f) by RELAT_1: 70;

        

         A4: 0 <= ( vol ( divset (D,i))) by SEQ_4: 11, XREAL_1: 48;

        

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

        assume i in ( dom D);

        then ( dom (f | ( divset (D,i)))) = ( divset (D,i)) by A5, Th6, RELAT_1: 62;

        then

         A6: ( rng (f | ( divset (D,i)))) is non empty Subset of REAL by RELAT_1: 42;

        ( rng f) is bounded_below by A1, Th9;

        hence thesis by A3, A6, A4, SEQ_4: 47, XREAL_1: 64;

      end;

      

       A7: for i st i in ( dom D) holds (( lower_bound ( rng f)) * (( lower_volume (( chi (A,A)),D)) . i)) <= (( lower_bound ( rng (f | ( divset (D,i))))) * ( vol ( divset (D,i))))

      proof

        let i;

        assume

         A8: i in ( dom D);

        then (( lower_bound ( rng f)) * ( vol ( divset (D,i)))) <= (( lower_bound ( rng (f | ( divset (D,i))))) * ( vol ( divset (D,i)))) by A2;

        hence thesis by A8, Th17;

      end;

      ( Sum (( lower_bound ( rng f)) * ( lower_volume (( chi (A,A)),D)))) <= ( Sum ( lower_volume (f,D)))

      proof

        ( len ( lower_volume (( chi (A,A)),D))) = ( len (( lower_bound ( rng f)) * ( lower_volume (( chi (A,A)),D)))) by FINSEQ_2: 33;

        then

         A9: ( len (( lower_bound ( rng f)) * ( lower_volume (( chi (A,A)),D)))) = ( len D) by Def6;

        deffunc G( Nat) = ( In ((( lower_bound ( rng (f | ( divset (D,$1))))) * ( vol ( divset (D,$1)))), REAL ));

        deffunc F( set) = ( In ((( lower_bound ( rng f)) * (( lower_volume (( chi (A,A)),D)) . $1)), REAL ));

        consider p be FinSequence of REAL such that

         A10: ( len p) = ( len D) & for i be Nat st i in ( dom p) holds (p . i) = F(i) from FINSEQ_2:sch 1;

        

         A11: ( dom p) = ( Seg ( len D)) by A10, FINSEQ_1:def 3;

        for i be Nat st 1 <= i & i <= ( len p) holds (p . i) = ((( lower_bound ( rng f)) * ( lower_volume (( chi (A,A)),D))) . i)

        proof

          let i be Nat;

          assume that

           A12: 1 <= i and

           A13: i <= ( len p);

          i in ( Seg ( len D)) by A10, A12, A13, FINSEQ_1: 1;

          then (p . i) = F(i) by A10, A11;

          hence thesis by RVSUM_1: 44;

        end;

        then

         A14: p = (( lower_bound ( rng f)) * ( lower_volume (( chi (A,A)),D))) by A10, A9, FINSEQ_1: 14;

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

        consider q be FinSequence of REAL such that

         A15: ( len q) = ( len D) & for i be Nat st i in ( dom q) holds (q . i) = G(i) from FINSEQ_2:sch 1;

        

         A16: for i be Nat st i in ( dom q) holds (q . i) = (( lower_bound ( rng (f | ( divset (D,i))))) * ( vol ( divset (D,i))))

        proof

          let i be Nat;

          assume i in ( dom q);

          then (q . i) = G(i) by A15;

          hence thesis;

        end;

        

         A17: ( dom q) = ( dom D) by A15, FINSEQ_3: 29;

        then

         A18: q = ( lower_volume (f,D)) by A15, Def6, A16;

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

        now

          let i be Nat;

          assume

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

          then

           A20: (p . i) = F(i) by A10, A11;

          

           A21: i in ( dom D) by A19, FINSEQ_1:def 3;

          then (q . i) = G(i) by A15, A17;

          hence (p . i) <= (q . i) by A7, A20, A21;

        end;

        hence thesis by A18, A14, RVSUM_1: 82;

      end;

      then (( lower_bound ( rng f)) * ( Sum ( lower_volume (( chi (A,A)),D)))) <= ( Sum ( lower_volume (f,D))) by RVSUM_1: 87;

      hence thesis by Th21;

    end;

    theorem :: INTEGRA1:26

    (f | A) is bounded_above & i in ( dom D) implies (( upper_bound ( rng f)) * ( vol ( divset (D,i)))) >= (( upper_bound ( rng (f | ( divset (D,i))))) * ( vol ( divset (D,i))))

    proof

      

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

      assume (f | A) is bounded_above;

      then

       A2: ( rng f) is bounded_above by Th11;

      assume i in ( dom D);

      then ( dom (f | ( divset (D,i)))) = ( divset (D,i)) by A1, Th6, RELAT_1: 62;

      then

       A3: ( rng (f | ( divset (D,i)))) is non empty Subset of REAL by RELAT_1: 42;

      

       A4: 0 <= ( vol ( divset (D,i))) by SEQ_4: 11, XREAL_1: 48;

      ( rng (f | ( divset (D,i)))) c= ( rng f) by RELAT_1: 70;

      hence thesis by A3, A2, A4, SEQ_4: 48, XREAL_1: 64;

    end;

    theorem :: INTEGRA1:27

    

     Th25: (f | A) is bounded_above implies ( upper_sum (f,D)) <= (( upper_bound ( rng f)) * ( vol A))

    proof

      assume

       A1: (f | A) is bounded_above;

      

       A2: for i st i in ( Seg ( len D)) holds (( upper_bound ( rng f)) * ( vol ( divset (D,i)))) >= (( upper_bound ( rng (f | ( divset (D,i))))) * ( vol ( divset (D,i))))

      proof

        let i;

        

         A3: ( rng (f | ( divset (D,i)))) c= ( rng f) by RELAT_1: 70;

        

         A4: 0 <= ( vol ( divset (D,i))) by SEQ_4: 11, XREAL_1: 48;

        assume i in ( Seg ( len D));

        then

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

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

        then ( dom (f | ( divset (D,i)))) = ( divset (D,i)) by A5, Th6, RELAT_1: 62;

        then

         A6: ( rng (f | ( divset (D,i)))) is non empty Subset of REAL by RELAT_1: 42;

        ( rng f) is bounded_above by A1, Th11;

        hence thesis by A3, A6, A4, SEQ_4: 48, XREAL_1: 64;

      end;

      

       A7: for i st i in ( Seg ( len D)) holds (( upper_bound ( rng f)) * (( upper_volume (( chi (A,A)),D)) . i)) >= (( upper_bound ( rng (f | ( divset (D,i))))) * ( vol ( divset (D,i))))

      proof

        let i;

        assume

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

        then

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

        (( upper_bound ( rng f)) * ( vol ( divset (D,i)))) >= (( upper_bound ( rng (f | ( divset (D,i))))) * ( vol ( divset (D,i)))) by A2, A8;

        hence thesis by A9, Th18;

      end;

      ( Sum (( upper_bound ( rng f)) * ( upper_volume (( chi (A,A)),D)))) >= ( Sum ( upper_volume (f,D)))

      proof

        ( len ( upper_volume (( chi (A,A)),D))) = ( len (( upper_bound ( rng f)) * ( upper_volume (( chi (A,A)),D)))) by FINSEQ_2: 33;

        then

         A10: ( len (( upper_bound ( rng f)) * ( upper_volume (( chi (A,A)),D)))) = ( len D) by Def5;

        deffunc G( Nat) = ( In ((( upper_bound ( rng (f | ( divset (D,$1))))) * ( vol ( divset (D,$1)))), REAL ));

        deffunc F( set) = ( In ((( upper_bound ( rng f)) * (( upper_volume (( chi (A,A)),D)) . $1)), REAL ));

        consider p be FinSequence of REAL such that

         A11: ( len p) = ( len D) & for i be Nat st i in ( dom p) holds (p . i) = F(i) from FINSEQ_2:sch 1;

        

         A12: ( dom p) = ( Seg ( len D)) by A11, FINSEQ_1:def 3;

        for i be Nat st 1 <= i & i <= ( len p) holds (p . i) = ((( upper_bound ( rng f)) * ( upper_volume (( chi (A,A)),D))) . i)

        proof

          let i be Nat;

          assume that

           A13: 1 <= i and

           A14: i <= ( len p);

          i in ( Seg ( len D)) by A11, A13, A14, FINSEQ_1: 1;

          then (p . i) = F(i) by A11, A12;

          hence thesis by RVSUM_1: 44;

        end;

        then

         A15: p = (( upper_bound ( rng f)) * ( upper_volume (( chi (A,A)),D))) by A11, A10, FINSEQ_1: 14;

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

        consider q be FinSequence of REAL such that

         A16: ( len q) = ( len D) & for i be Nat st i in ( dom q) holds (q . i) = G(i) from FINSEQ_2:sch 1;

        

         A17: for i be Nat st i in ( dom q) holds (q . i) = (( upper_bound ( rng (f | ( divset (D,i))))) * ( vol ( divset (D,i))))

        proof

          let i be Nat;

          assume i in ( dom q);

          then (q . i) = G(i) by A16;

          hence thesis;

        end;

        

         A18: ( dom q) = ( dom D) by A16, FINSEQ_3: 29;

        then

         A19: q = ( upper_volume (f,D)) by A16, Def5, A17;

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

        now

          let i be Nat;

          assume

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

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

          then

           A21: (q . i) = G(i) by A16, A18;

          (p . i) = F(i) by A11, A12, A20;

          hence (q . i) <= (p . i) by A7, A20, A21;

        end;

        hence thesis by A19, A15, RVSUM_1: 82;

      end;

      then (( upper_bound ( rng f)) * ( Sum ( upper_volume (( chi (A,A)),D)))) >= ( Sum ( upper_volume (f,D))) by RVSUM_1: 87;

      hence thesis by Th22;

    end;

    theorem :: INTEGRA1:28

    

     Th26: (f | A) is bounded implies ( lower_sum (f,D)) <= ( upper_sum (f,D))

    proof

      deffunc F( Nat) = ( In ((( lower_bound ( rng (f | ( divset (D,$1))))) * ( vol ( divset (D,$1)))), REAL ));

      consider p be FinSequence of REAL such that

       A1: ( len p) = ( len D) & for i be Nat st i in ( dom p) holds (p . i) = F(i) from FINSEQ_2:sch 1;

      

       A2: for i be Nat st i in ( dom p) holds (p . i) = (( lower_bound ( rng (f | ( divset (D,i))))) * ( vol ( divset (D,i))))

      proof

        let i be Nat;

        assume i in ( dom p);

        then (p . i) = F(i) by A1;

        hence thesis;

      end;

      assume

       A3: (f | A) is bounded;

      then

       A4: ( rng f) is bounded_above by Th11;

      

       A5: ( dom p) = ( dom D) by A1, FINSEQ_3: 29;

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

      deffunc G( Nat) = ( In ((( upper_bound ( rng (f | ( divset (D,$1))))) * ( vol ( divset (D,$1)))), REAL ));

      consider q be FinSequence of REAL such that

       A6: ( len q) = ( len D) & for i be Nat st i in ( dom q) holds (q . i) = G(i) from FINSEQ_2:sch 1;

      

       A7: for i be Nat st i in ( dom q) holds (q . i) = (( upper_bound ( rng (f | ( divset (D,i))))) * ( vol ( divset (D,i))))

      proof

        let i be Nat;

        assume i in ( dom q);

        then (q . i) = G(i) by A6;

        hence thesis;

      end;

      

       A8: ( dom q) = ( dom D) by A6, FINSEQ_3: 29;

      then ( len q) = ( len D) by FINSEQ_3: 29;

      then

       A9: q = ( upper_volume (f,D)) by A7, Def5, A8;

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

      

       A10: ( rng f) is bounded_below by A3, Th9;

      for i be Nat st i in ( Seg ( len D)) holds (p . i) <= (q . i)

      proof

        let i be Nat;

        

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

        assume

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

        then

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

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

        then ( dom (f | ( divset (D,i)))) = ( divset (D,i)) by A11, Th6, RELAT_1: 62;

        then

         A14: ( rng (f | ( divset (D,i)))) is non empty Subset of REAL by RELAT_1: 42;

        

         A15: 0 <= ( vol ( divset (D,i))) by SEQ_4: 11, XREAL_1: 48;

        

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

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

        then (( lower_bound ( rng (f | ( divset (D,i))))) * ( vol ( divset (D,i)))) <= (( upper_bound ( rng (f | ( divset (D,i))))) * ( vol ( divset (D,i)))) by A16, A14, A15, SEQ_4: 11, XREAL_1: 64;

        then (p . i) <= (( upper_bound ( rng (f | ( divset (D,i))))) * ( vol ( divset (D,i)))) by A5, A13, A2;

        hence thesis by A8, A13, A7;

      end;

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

      hence thesis by A1, A5, A9, Def6, A2;

    end;

    definition

      let D1,D2 be FinSequence;

      :: INTEGRA1:def18

      pred D1 <= D2 means ( len D1) <= ( len D2) & ( rng D1) c= ( rng D2);

      reflexivity ;

    end

    notation

      let D1,D2 be FinSequence;

      synonym D2 >= D1 for D1 <= D2;

    end

    theorem :: INTEGRA1:29

    ( len D1) = 1 implies D1 <= D2

    proof

      

       A1: (D2 . ( len D2)) = ( upper_bound A) by Def1;

      assume

       A2: ( len D1) = 1;

      then (D1 . 1) = ( upper_bound A) by Def1;

      then D1 = <*( upper_bound A)*> by A2, FINSEQ_1: 40;

      then

       A3: ( rng D1) = {( upper_bound A)} by FINSEQ_1: 38;

      

       A4: ( len D2) in ( Seg ( len D2)) by FINSEQ_1: 3;

      hence ( len D1) <= ( len D2) by A2, FINSEQ_1: 1;

      ( len D2) in ( dom D2) by A4, FINSEQ_1:def 3;

      then ( upper_bound A) in ( rng D2) by A1, FUNCT_1:def 3;

      then ( rng D1) is Subset of ( rng D2) by A3, SUBSET_1: 41;

      hence thesis;

    end;

    theorem :: INTEGRA1:30

    

     Th28: (f | A) is bounded_above & ( len D1) = 1 implies ( upper_sum (f,D1)) >= ( upper_sum (f,D2))

    proof

      assume that

       A1: (f | A) is bounded_above and

       A2: ( len D1) = 1;

      1 in ( Seg ( len D1)) by A2, FINSEQ_1: 3;

      then

       A3: 1 in ( dom D1) by FINSEQ_1:def 3;

      then

       A4: ( lower_bound ( divset (D1,1))) = ( lower_bound A) by Def3;

      

       A5: ( divset (D1,1)) = [.( lower_bound ( divset (D1,1))), ( upper_bound ( divset (D1,1))).] by Th2;

      ( upper_bound ( divset (D1,1))) = (D1 . 1) by A3, Def3

      .= ( upper_bound A) by A2, Def1;

      then

       A6: ( divset (D1,1)) = A by A4, A5, Th2;

      

       A7: (( upper_volume (f,D1)) . 1) = (( upper_bound ( rng (f | ( divset (D1,1))))) * ( vol ( divset (D1,1)))) by A3, Def5;

      reconsider ubv = (( upper_bound ( rng (f | ( divset (D1,1))))) * ( vol ( divset (D1,1)))) as Element of REAL by XREAL_0:def 1;

      ( len ( upper_volume (f,D1))) = 1 by A2, Def5;

      

      then ( upper_sum (f,D1)) = ( Sum <*ubv*>) by A7, FINSEQ_1: 40

      .= (( upper_bound ( rng (f | A))) * ( vol A)) by A6, FINSOP_1: 11

      .= (( upper_bound ( rng f)) * ( vol A));

      hence thesis by A1, Th25;

    end;

    theorem :: INTEGRA1:31

    

     Th29: (f | A) is bounded_below & ( len D1) = 1 implies ( lower_sum (f,D1)) <= ( lower_sum (f,D2))

    proof

      assume that

       A1: (f | A) is bounded_below and

       A2: ( len D1) = 1;

      1 in ( Seg ( len D1)) by A2, FINSEQ_1: 3;

      then

       A3: 1 in ( dom D1) by FINSEQ_1:def 3;

      then

       A4: ( lower_bound ( divset (D1,1))) = ( lower_bound A) by Def3;

      ( upper_bound ( divset (D1,1))) = (D1 . 1) by A3, Def3

      .= ( upper_bound A) by A2, Def1;

      then ( divset (D1,1)) = [.( lower_bound A), ( upper_bound A).] by A4, Th2;

      then

       A5: ( divset (D1,1)) = A by Th2;

      

       A6: (( lower_volume (f,D1)) . 1) = (( lower_bound ( rng (f | ( divset (D1,1))))) * ( vol ( divset (D1,1)))) by A3, Def6;

      reconsider lbv = (( lower_bound ( rng (f | ( divset (D1,1))))) * ( vol ( divset (D1,1)))) as Element of REAL by XREAL_0:def 1;

      ( len ( lower_volume (f,D1))) = 1 by A2, Def6;

      

      then ( lower_sum (f,D1)) = ( Sum <*lbv*>) by A6, FINSEQ_1: 40

      .= (( lower_bound ( rng (f | A))) * ( vol A)) by A5, FINSOP_1: 11

      .= (( lower_bound ( rng f)) * ( vol A));

      hence thesis by A1, Th23;

    end;

    theorem :: INTEGRA1:32

    i in ( dom D) implies ex A1,A2 be non empty closed_interval Subset of REAL st A1 = [.( lower_bound A), (D . i).] & A2 = [.(D . i), ( upper_bound A).] & A = (A1 \/ A2)

    proof

      assume i in ( dom D);

      then

       A1: (D . i) in ( rng D) by FUNCT_1:def 3;

      ( rng D) c= A by Def1;

      then (D . i) in A by A1;

      then (D . i) in [.( lower_bound A), ( upper_bound A).] by Th2;

      then (D . i) in { a : ( lower_bound A) <= a & a <= ( upper_bound A) } by RCOMP_1:def 1;

      then

       A2: ex a st a = (D . i) & ( lower_bound A) <= a & a <= ( upper_bound A);

      then

      reconsider A1 = [.( lower_bound A), (D . i).] as non empty closed_interval Subset of REAL by MEASURE5: 14;

      reconsider A2 = [.(D . i), ( upper_bound A).] as non empty closed_interval Subset of REAL by A2, MEASURE5: 14;

      take A1, A2;

      (A1 \/ A2) = [.( lower_bound A), ( upper_bound A).] by A2, XXREAL_1: 174

      .= A by Th2;

      hence thesis;

    end;

    theorem :: INTEGRA1:33

    

     Th31: i in ( dom D1) & D1 <= D2 implies ex j st j in ( dom D2) & (D1 . i) = (D2 . j)

    proof

      assume i in ( dom D1);

      then

       A1: (D1 . i) in ( rng D1) by FUNCT_1:def 3;

      assume D1 <= D2;

      then ( rng D1) c= ( rng D2);

      then

      consider x1 be object such that

       A2: x1 in ( dom D2) and

       A3: (D1 . i) = (D2 . x1) by A1, FUNCT_1:def 3;

      reconsider x1 as Element of NAT by A2;

      take x1;

      thus thesis by A2, A3;

    end;

    definition

      let A, D1, D2;

      let i be Nat;

      assume

       A1: D1 <= D2;

      :: INTEGRA1:def19

      func indx (D2,D1,i) -> Element of NAT means

      : Def18: it in ( dom D2) & (D1 . i) = (D2 . it ) if i in ( dom D1)

      otherwise it = 0 ;

      existence by A1, Th31;

      uniqueness

      proof

        let m,n be Element of NAT ;

        hereby

          assume that i in ( dom D1) and

           A2: m in ( dom D2) and

           A3: (D1 . i) = (D2 . m) and

           A4: n in ( dom D2) and

           A5: (D1 . i) = (D2 . n);

          assume

           A6: m <> n;

          now

            per cases by A6, XXREAL_0: 1;

              suppose m < n;

              hence contradiction by A2, A3, A4, A5, SEQM_3:def 1;

            end;

              suppose n < m;

              hence contradiction by A2, A3, A4, A5, SEQM_3:def 1;

            end;

          end;

          hence contradiction;

        end;

        assume that not i in ( dom D1) and

         A7: m = 0 and

         A8: n = 0 ;

        thus thesis by A7, A8;

      end;

      correctness ;

    end

    theorem :: INTEGRA1:34

    

     Th32: for p be increasing FinSequence of REAL , n be Element of NAT holds n <= ( len p) implies (p /^ n) is increasing FinSequence of REAL

    proof

      let p be increasing FinSequence of REAL ;

      let n be Element of NAT ;

      assume

       A1: n <= ( len p);

      for i,j be Nat st i in ( dom (p /^ n)) & j in ( dom (p /^ n)) & i < j holds ((p /^ n) . i) < ((p /^ n) . j)

      proof

        let i,j be Nat;

        assume that

         A2: i in ( dom (p /^ n)) and

         A3: j in ( dom (p /^ n)) and

         A4: i < j;

        

         A5: (i + n) < (j + n) by A4, XREAL_1: 6;

        

         A6: j in ( Seg ( len (p /^ n))) by A3, FINSEQ_1:def 3;

        then 1 <= j by FINSEQ_1: 1;

        then

         A7: (1 + n) <= (j + n) by XREAL_1: 6;

        j <= ( len (p /^ n)) by A6, FINSEQ_1: 1;

        then j <= (( len p) - n) by A1, RFINSEQ:def 1;

        then

         A8: (j + n) <= ( len p) by XREAL_1: 19;

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

        then 1 <= (j + n) by A7, XXREAL_0: 2;

        then (j + n) in ( Seg ( len p)) by A8, FINSEQ_1: 1;

        then

         A9: (j + n) in ( dom p) by FINSEQ_1:def 3;

        

         A10: i in ( Seg ( len (p /^ n))) by A2, FINSEQ_1:def 3;

        then 1 <= i by FINSEQ_1: 1;

        then

         A11: (1 + n) <= (i + n) by XREAL_1: 6;

        i <= ( len (p /^ n)) by A10, FINSEQ_1: 1;

        then i <= (( len p) - n) by A1, RFINSEQ:def 1;

        then

         A12: (i + n) <= ( len p) by XREAL_1: 19;

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

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

        then (i + n) in ( Seg ( len p)) by A12, FINSEQ_1: 1;

        then

         A13: (i + n) in ( dom p) by FINSEQ_1:def 3;

        

         A14: ((p /^ n) . j) = (p . (j + n)) by A1, A3, RFINSEQ:def 1;

        ((p /^ n) . i) = (p . (i + n)) by A1, A2, RFINSEQ:def 1;

        hence thesis by A14, A13, A9, A5, SEQM_3:def 1;

      end;

      hence thesis by SEQM_3:def 1;

    end;

    theorem :: INTEGRA1:35

    

     Th33: for p be increasing FinSequence of REAL , i,j be Element of NAT holds j in ( dom p) & i <= j implies ( mid (p,i,j)) is increasing FinSequence of REAL

    proof

      let p be increasing FinSequence of REAL ;

      let i,j be Element of NAT ;

      assume that

       A1: j in ( dom p) and

       A2: i <= j;

      j in ( Seg ( len p)) by A1, FINSEQ_1:def 3;

      then j <= ( len p) by FINSEQ_1: 1;

      then i <= ( len p) by A2, XXREAL_0: 2;

      then (p /^ (i -' 1)) is increasing FinSequence of REAL by Th32, NAT_D: 44;

      then

       A3: ((p /^ (i -' 1)) | ( Seg ((j -' i) + 1))) is increasing FinSequence of REAL by FINSEQ_1: 18, SEQ_4: 139;

      ( mid (p,i,j)) = ((p /^ (i -' 1)) | ((j -' i) + 1)) by A2, FINSEQ_6:def 3;

      hence thesis by A3, FINSEQ_1:def 15;

    end;

    

     Lm1: for f be FinSequence holds i in ( dom f) & j in ( dom f) & i <= j implies ( len ( mid (f,i,j))) = ((j - i) + 1)

    proof

      let D be FinSequence;

      assume that

       A1: i in ( dom D) and

       A2: j in ( dom D) and

       A3: i <= j;

      j in ( Seg ( len D)) by A2, FINSEQ_1:def 3;

      then j <= ( len D) by FINSEQ_1: 1;

      then i <= ( len D) by A3, XXREAL_0: 2;

      then (i -' 1) <= ( len D) by NAT_D: 44;

      then

       A4: ( len (D /^ (i -' 1))) = (( len D) - (i -' 1)) by RFINSEQ:def 1;

      reconsider D1 = (D /^ (i -' 1)) as FinSequence;

      reconsider k = ((j -' i) + 1) as Element of NAT ;

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

      then 1 <= i by FINSEQ_1: 1;

      then (j - (i -' 1)) = (j - (i - 1)) by XREAL_1: 233;

      then

       A5: (j - (i -' 1)) = ((j - i) + 1);

      j in ( Seg ( len D)) by A2, FINSEQ_1:def 3;

      then j <= ( len D) by FINSEQ_1: 1;

      then (j - (i -' 1)) <= (( len D) - (i -' 1)) by XREAL_1: 9;

      then

       A6: ((j -' i) + 1) <= ( len (D /^ (i -' 1))) by A3, A4, A5, XREAL_1: 233;

      ( mid (D,i,j)) = ((D /^ (i -' 1)) | ((j -' i) + 1)) by A3, FINSEQ_6:def 3

      .= (D1 | ( Seg k)) by FINSEQ_1:def 15;

      then ( len ( mid (D,i,j))) = ((j -' i) + 1) by A6, FINSEQ_1: 17;

      hence thesis by A3, XREAL_1: 233;

    end;

    theorem :: INTEGRA1:36

    

     Th34: i in ( dom D) & j in ( dom D) & i <= j implies ex B be non empty closed_interval Subset of REAL st ( lower_bound B) = (( mid (D,i,j)) . 1) & ( upper_bound B) = (( mid (D,i,j)) . ( len ( mid (D,i,j)))) & ( mid (D,i,j)) is Division of B

    proof

      assume that

       A1: i in ( dom D) and

       A2: j in ( dom D) and

       A3: i <= j;

      j in ( Seg ( len D)) by A2, FINSEQ_1:def 3;

      then j <= ( len D) by FINSEQ_1: 1;

      then i <= ( len D) by A3, XXREAL_0: 2;

      then (i -' 1) <= ( len D) by NAT_D: 44;

      then

       A4: ( len (D /^ (i -' 1))) = (( len D) - (i -' 1)) by RFINSEQ:def 1;

      reconsider D1 = (D /^ (i -' 1)) as FinSequence of REAL ;

      reconsider k = ((j -' i) + 1) as Element of NAT ;

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

      then 1 <= i by FINSEQ_1: 1;

      then (j - (i -' 1)) = (j - (i - 1)) by XREAL_1: 233;

      then

       A5: (j - (i -' 1)) = ((j - i) + 1);

      j in ( Seg ( len D)) by A2, FINSEQ_1:def 3;

      then j <= ( len D) by FINSEQ_1: 1;

      then (j - (i -' 1)) <= (( len D) - (i -' 1)) by XREAL_1: 9;

      then

       A6: ((j -' i) + 1) <= ( len (D /^ (i -' 1))) by A3, A4, A5, XREAL_1: 233;

      

       A7: ( mid (D,i,j)) = ((D /^ (i -' 1)) | ((j -' i) + 1)) by A3, FINSEQ_6:def 3

      .= (D1 | ( Seg k)) by FINSEQ_1:def 15;

      then 0 < ( len ( mid (D,i,j))) by A6, FINSEQ_1: 17;

      then

      reconsider M = ( mid (D,i,j)) as non empty increasing FinSequence of REAL by A2, A3, Th33;

      ((j -' i) + 1) >= ( 0 + 1) by XREAL_1: 6;

      then

       A8: 1 <= ( len M) by A6, A7, FINSEQ_1: 17;

      then ( len M) in ( Seg ( len M)) by FINSEQ_1: 1;

      then

       A9: ( len M) in ( dom M) by FINSEQ_1:def 3;

      1 in ( Seg ( len M)) by A8, FINSEQ_1: 1;

      then

       A10: 1 in ( dom M) by FINSEQ_1:def 3;

      then (M . 1) <= (M . ( len M)) by A8, A9, SEQ_4: 137;

      then

      reconsider B = [.(M . 1), (M . ( len M)).] as non empty closed_interval Subset of REAL by MEASURE5: 14;

      

       A11: B = [.( lower_bound B), ( upper_bound B).] by Th2;

      then

       A12: ( lower_bound B) = (M . 1) by Th3;

      

       A13: (M . ( len M)) = ( upper_bound B) by A11, Th3;

      for x be Element of REAL st x in ( rng M) holds x in B

      proof

        let x be Element of REAL ;

        assume x in ( rng M);

        then

        consider i such that

         A14: i in ( dom M) and

         A15: x = (M . i) by PARTFUN1: 3;

        

         A16: i in ( Seg ( len M)) by A14, FINSEQ_1:def 3;

        then i <= ( len M) by FINSEQ_1: 1;

        then

         A17: (M . i) <= (M . ( len M)) by A9, A14, SEQ_4: 137;

        1 <= i by A16, FINSEQ_1: 1;

        then (M . 1) <= (M . i) by A10, A14, SEQ_4: 137;

        then (M . i) in { a : (M . 1) <= a & a <= (M . ( len M)) } by A17;

        hence thesis by A15, RCOMP_1:def 1;

      end;

      then ( rng M) c= B;

      then M is Division of B by A13, Def1;

      hence thesis by A12, A13;

    end;

    theorem :: INTEGRA1:37

    

     Th35: i in ( dom D) & j in ( dom D) & i <= j & (D . i) >= ( lower_bound B) & (D . j) = ( upper_bound B) implies ( mid (D,i,j)) is Division of B

    proof

      assume that

       A1: i in ( dom D) and

       A2: j in ( dom D) and

       A3: i <= j and

       A4: (D . i) >= ( lower_bound B) and

       A5: (D . j) = ( upper_bound B);

      

       A6: ((((j - i) + 1) + i) - 1) = j;

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

      then

       A7: 1 <= i by FINSEQ_1: 1;

       0 <= (j - i) by A3, XREAL_1: 48;

      then

       A8: ( 0 + 1) <= ((j - i) + 1) by XREAL_1: 6;

      j in ( Seg ( len D)) by A2, FINSEQ_1:def 3;

      then

       A9: j <= ( len D) by FINSEQ_1: 1;

      consider A1 be non empty closed_interval Subset of REAL such that

       A10: ( lower_bound A1) = (( mid (D,i,j)) . 1) and

       A11: ( upper_bound A1) = (( mid (D,i,j)) . ( len ( mid (D,i,j)))) and

       A12: ( mid (D,i,j)) is Division of A1 by A1, A2, A3, Th34;

      

       A13: ( len ( mid (D,i,j))) = ((j - i) + 1) by A1, A2, A3, Lm1;

      

       A14: ((1 + i) - 1) = i;

      for x be Element of REAL st x in A1 holds x in B

      proof

        let x be Element of REAL ;

        assume x in A1;

        then x in [.( lower_bound A1), ( upper_bound A1).] by Th2;

        then x in { a : ( lower_bound A1) <= a & a <= ( upper_bound A1) } by RCOMP_1:def 1;

        then

         A15: ex a st x = a & ( lower_bound A1) <= a & a <= ( upper_bound A1);

        then (D . i) <= x by A3, A10, A7, A9, A8, A14, FINSEQ_6: 122;

        then

         A16: ( lower_bound B) <= x by A4, XXREAL_0: 2;

        x <= ( upper_bound B) by A3, A5, A11, A13, A7, A9, A8, A6, A15, FINSEQ_6: 122;

        then x in { a : ( lower_bound B) <= a & a <= ( upper_bound B) } by A16;

        then x in [.( lower_bound B), ( upper_bound B).] by RCOMP_1:def 1;

        hence thesis by Th2;

      end;

      then

       A17: A1 c= B;

      ( rng ( mid (D,i,j))) c= A1 by A12, Def1;

      then

       A18: ( rng ( mid (D,i,j))) c= B by A17;

      (( mid (D,i,j)) . ( len ( mid (D,i,j)))) = (D . j) by A3, A13, A7, A9, A8, A6, FINSEQ_6: 122;

      hence thesis by A5, A12, A18, Def1;

    end;

    definition

      let p be FinSequence of REAL ;

      :: INTEGRA1:def20

      func PartSums (p) -> FinSequence of REAL means

      : Def19: ( len it ) = ( len p) & for i be Nat st i in ( dom p) holds (it . i) = ( Sum (p | i));

      existence

      proof

        deffunc F( Nat) = ( In (( Sum (p | $1)), REAL ));

        consider IT be FinSequence of REAL such that

         A1: ( len IT) = ( len p) & for i be Nat st i in ( dom IT) holds (IT . i) = F(i) from FINSEQ_2:sch 1;

        take IT;

        thus ( len IT) = ( len p) by A1;

        let i be Nat;

        assume i in ( dom p);

        then i in ( dom IT) by A1, FINSEQ_3: 29;

        then (IT . i) = F(i) by A1;

        hence thesis;

      end;

      uniqueness

      proof

        let p1,p2 be FinSequence of REAL such that

         A2: ( len p1) = ( len p) and

         A3: for i be Nat st i in ( dom p) holds (p1 . i) = ( Sum (p | i)) and

         A4: ( len p2) = ( len p) and

         A5: for i be Nat st i in ( dom p) holds (p2 . i) = ( Sum (p | i));

        for i be Nat st 1 <= i & i <= ( len p1) holds (p1 . i) = (p2 . i)

        proof

          let i be Nat;

          assume that

           A6: 1 <= i and

           A7: i <= ( len p1);

          

           A8: i in ( dom p) by A2, A6, A7, FINSEQ_3: 25;

          then (p1 . i) = ( Sum (p | i)) by A3;

          hence thesis by A5, A8;

        end;

        hence thesis by A2, A4, FINSEQ_1: 14;

      end;

    end

    theorem :: INTEGRA1:38

    

     Th36: D1 <= D2 & (f | A) is bounded_above implies for i be non zero Element of NAT holds (i in ( dom D1) implies ( Sum (( upper_volume (f,D1)) | i)) >= ( Sum (( upper_volume (f,D2)) | ( indx (D2,D1,i)))))

    proof

      assume that

       A1: D1 <= D2 and

       A2: (f | A) is bounded_above;

      for i be non zero Nat holds i in ( dom D1) implies ( Sum (( upper_volume (f,D1)) | i)) >= ( Sum (( upper_volume (f,D2)) | ( indx (D2,D1,i))))

      proof

        defpred P[ Nat] means $1 in ( dom D1) implies ( Sum (( upper_volume (f,D1)) | $1)) >= ( Sum (( upper_volume (f,D2)) | ( indx (D2,D1,$1))));

        

         A3: P[1]

        proof

          reconsider g = (f | ( divset (D1,1))) as PartFunc of ( divset (D1,1)), REAL by PARTFUN1: 10;

          set B = ( divset (D1,1));

          set DD1 = ( mid (D1,1,1));

          

           A4: ( dom g) = (( dom f) /\ ( divset (D1,1))) by RELAT_1: 61;

          assume

           A5: 1 in ( dom D1);

          then

           A6: (D1 . 1) = ( upper_bound B) by Def3;

          then

           A7: (D2 . ( indx (D2,D1,1))) = ( upper_bound B) by A1, A5, Def18;

          (D1 . 1) >= ( lower_bound B) by A6, SEQ_4: 11;

          then

          reconsider DD1 as Division of B by A5, A6, Th35;

          1 in ( Seg ( len D1)) by A5, FINSEQ_1:def 3;

          then

           A8: 1 <= ( len D1) by FINSEQ_1: 1;

          then

           A9: ( len ( mid (D1,1,1))) = ((1 -' 1) + 1) by FINSEQ_6: 118;

          

           A10: ( len ( upper_volume (g,DD1))) = ( len DD1) by Def5

          .= 1 by A9, XREAL_1: 235;

          

           A11: ( len ( mid (D1,1,1))) = 1 by A9, XREAL_1: 235;

          then

           A12: ( len ( mid (D1,1,1))) = ( len (D1 | 1));

          for k be Nat st 1 <= k & k <= ( len ( mid (D1,1,1))) holds (( mid (D1,1,1)) . k) = ((D1 | 1) . k)

          proof

            let k be Nat;

            assume that

             A13: 1 <= k and

             A14: k <= ( len ( mid (D1,1,1)));

            k in ( Seg ( len (D1 | 1))) by A12, A13, A14, FINSEQ_1: 1;

            then k in ( dom (D1 | 1)) by FINSEQ_1:def 3;

            then k in ( dom (D1 | ( Seg 1))) by FINSEQ_1:def 15;

            then

             A15: ((D1 | ( Seg 1)) . k) = (D1 . k) by FUNCT_1: 47;

            

             A16: k = 1 by A11, A13, A14, XXREAL_0: 1;

            then (( mid (D1,1,1)) . k) = (D1 . ((1 + 1) - 1)) by A8, FINSEQ_6: 118;

            hence thesis by A16, A15, FINSEQ_1:def 15;

          end;

          then

           A17: ( mid (D1,1,1)) = (D1 | 1) by A12, FINSEQ_1: 14;

          

           A18: for i be Nat st 1 <= i & i <= ( len ( upper_volume (g,DD1))) holds (( upper_volume (g,DD1)) . i) = ((( upper_volume (f,D1)) | 1) . i)

          proof

            let i be Nat;

            assume that

             A19: 1 <= i and

             A20: i <= ( len ( upper_volume (g,DD1)));

            

             A21: 1 in ( Seg 1) by FINSEQ_1: 3;

            ( dom (D1 | ( Seg 1))) = (( dom D1) /\ ( Seg 1)) by RELAT_1: 61;

            then

             A22: 1 in ( dom (D1 | ( Seg 1))) by A5, A21, XBOOLE_0:def 4;

            ( dom ( upper_volume (f,D1))) = ( Seg ( len ( upper_volume (f,D1)))) by FINSEQ_1:def 3

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

            

            then

             A23: ( dom (( upper_volume (f,D1)) | ( Seg 1))) = (( Seg ( len D1)) /\ ( Seg 1)) by RELAT_1: 61

            .= ( Seg 1) by A8, FINSEQ_1: 7;

            ( len DD1) = 1 by A9, XREAL_1: 235;

            then

             A24: 1 in ( dom DD1) by A21, FINSEQ_1:def 3;

            

             A25: ((( upper_volume (f,D1)) | 1) . i) = ((( upper_volume (f,D1)) | ( Seg 1)) . i) by FINSEQ_1:def 15

            .= ((( upper_volume (f,D1)) | ( Seg 1)) . 1) by A10, A19, A20, XXREAL_0: 1

            .= (( upper_volume (f,D1)) . 1) by A23, FINSEQ_1: 3, FUNCT_1: 47

            .= (( upper_bound ( rng (f | ( divset (D1,1))))) * ( vol ( divset (D1,1)))) by A5, Def5;

            

             A26: ( divset (D1,1)) = [.( lower_bound ( divset (D1,1))), ( upper_bound ( divset (D1,1))).] by Th2

            .= [.( lower_bound A), ( upper_bound ( divset (D1,1))).] by A5, Def3

            .= [.( lower_bound A), (D1 . 1).] by A5, Def3;

            

             A27: (( upper_volume (g,DD1)) . i) = (( upper_volume (g,DD1)) . 1) by A10, A19, A20, XXREAL_0: 1

            .= (( upper_bound ( rng (g | ( divset (DD1,1))))) * ( vol ( divset (DD1,1)))) by A24, Def5;

            ( divset (DD1,1)) = [.( lower_bound ( divset (DD1,1))), ( upper_bound ( divset (DD1,1))).] by Th2

            .= [.( lower_bound B), ( upper_bound ( divset (DD1,1))).] by A24, Def3

            .= [.( lower_bound B), (DD1 . 1).] by A24, Def3

            .= [.( lower_bound A), ((D1 | 1) . 1).] by A5, A17, Def3

            .= [.( lower_bound A), ((D1 | ( Seg 1)) . 1).] by FINSEQ_1:def 15

            .= [.( lower_bound A), (D1 . 1).] by A22, FUNCT_1: 47;

            hence thesis by A27, A26, A25;

          end;

          

           A28: (g | ( divset (D1,1))) is bounded_above

          proof

            consider a be Real such that

             A29: for x be object st x in (A /\ ( dom f)) holds (f . x) <= a by A2, RFUNCT_1: 70;

            for x be object st x in (( divset (D1,1)) /\ ( dom g)) holds (g . x) <= a

            proof

              let x be object;

              

               A30: ( dom g) c= ( dom f) by RELAT_1: 60;

              assume x in (( divset (D1,1)) /\ ( dom g));

              then

               A31: x in ( dom g) by XBOOLE_0:def 4;

              

               A32: (A /\ ( dom f)) = ( dom f) by XBOOLE_1: 28;

              then x in (A /\ ( dom f)) by A31, A30;

              then

              reconsider x as Element of A;

              (f . x) <= a by A29, A31, A32, A30;

              hence thesis by A31, FUNCT_1: 47;

            end;

            hence thesis by RFUNCT_1: 70;

          end;

          

           A33: ( rng D2) c= A by Def1;

          

           A34: ( indx (D2,D1,1)) in ( dom D2) by A1, A5, Def18;

          then

           A35: ( indx (D2,D1,1)) in ( Seg ( len D2)) by FINSEQ_1:def 3;

          then

           A36: 1 <= ( indx (D2,D1,1)) by FINSEQ_1: 1;

          

           A37: ( indx (D2,D1,1)) <= ( len D2) by A35, FINSEQ_1: 1;

          then 1 <= ( len D2) by A36, XXREAL_0: 2;

          then 1 in ( Seg ( len D2)) by FINSEQ_1: 1;

          then

           A38: 1 in ( dom D2) by FINSEQ_1:def 3;

          then (D2 . 1) in ( rng D2) by FUNCT_1:def 3;

          then (D2 . 1) in A by A33;

          then (D2 . 1) in [.( lower_bound A), ( upper_bound A).] by Th2;

          then (D2 . 1) in { a : ( lower_bound A) <= a & a <= ( upper_bound A) } by RCOMP_1:def 1;

          then ex a st (D2 . 1) = a & ( lower_bound A) <= a & a <= ( upper_bound A);

          then (D2 . 1) >= ( lower_bound B) by A5, Def3;

          then

          reconsider DD2 = ( mid (D2,1,( indx (D2,D1,1)))) as Division of B by A34, A36, A38, A7, Th35;

          ( indx (D2,D1,1)) in ( dom D2) by A1, A5, Def18;

          then

           A39: ( indx (D2,D1,1)) in ( Seg ( len D2)) by FINSEQ_1:def 3;

          then

           A40: 1 <= ( indx (D2,D1,1)) by FINSEQ_1: 1;

          

           A41: ( indx (D2,D1,1)) <= ( len D2) by A39, FINSEQ_1: 1;

          then

           A42: 1 <= ( len D2) by A40, XXREAL_0: 2;

          then ( len ( mid (D2,1,( indx (D2,D1,1))))) = ((( indx (D2,D1,1)) -' 1) + 1) by A40, A41, FINSEQ_6: 118;

          then

           A43: ( len ( mid (D2,1,( indx (D2,D1,1))))) = ((( indx (D2,D1,1)) - 1) + 1) by A40, XREAL_1: 233;

          then

           A44: ( len ( mid (D2,1,( indx (D2,D1,1))))) = ( len (D2 | ( indx (D2,D1,1)))) by A41, FINSEQ_1: 59;

          

           A45: for k be Nat st 1 <= k & k <= ( len ( mid (D2,1,( indx (D2,D1,1))))) holds (( mid (D2,1,( indx (D2,D1,1)))) . k) = ((D2 | ( indx (D2,D1,1))) . k)

          proof

            let k be Nat;

            assume that

             A46: 1 <= k and

             A47: k <= ( len ( mid (D2,1,( indx (D2,D1,1)))));

            k in ( Seg ( len (D2 | ( indx (D2,D1,1))))) by A44, A46, A47, FINSEQ_1: 1;

            then k in ( dom (D2 | ( indx (D2,D1,1)))) by FINSEQ_1:def 3;

            then k in ( dom (D2 | ( Seg ( indx (D2,D1,1))))) by FINSEQ_1:def 15;

            then

             A48: ((D2 | ( Seg ( indx (D2,D1,1)))) . k) = (D2 . k) by FUNCT_1: 47;

            (( mid (D2,1,( indx (D2,D1,1)))) . k) = (D2 . ((k + 1) -' 1)) by A40, A41, A42, A46, A47, FINSEQ_6: 118;

            then (( mid (D2,1,( indx (D2,D1,1)))) . k) = (D2 . ((k + 1) - 1)) by NAT_1: 11, XREAL_1: 233;

            hence thesis by A48, FINSEQ_1:def 15;

          end;

          then

           A49: ( mid (D2,1,( indx (D2,D1,1)))) = (D2 | ( indx (D2,D1,1))) by A44, FINSEQ_1: 14;

          

           A50: for i be Nat st 1 <= i & i <= ( len ( upper_volume (g,DD2))) holds (( upper_volume (g,DD2)) . i) = ((( upper_volume (f,D2)) | ( indx (D2,D1,1))) . i)

          proof

            let i be Nat;

            assume that

             A51: 1 <= i and

             A52: i <= ( len ( upper_volume (g,DD2)));

            

             A53: i <= ( len DD2) by A52, Def5;

            then

             A54: i in ( Seg ( len DD2)) by A51, FINSEQ_1: 1;

            then

             A55: i in ( dom DD2) by FINSEQ_1:def 3;

            ( divset (DD2,i)) = ( divset (D2,i))

            proof

              ( Seg ( indx (D2,D1,1))) c= ( Seg ( len D2)) by A41, FINSEQ_1: 5;

              then i in ( Seg ( len D2)) by A43, A54;

              then

               A56: i in ( dom D2) by FINSEQ_1:def 3;

              now

                per cases ;

                  suppose

                   A57: i = 1;

                  then

                   A58: 1 in ( dom (D2 | ( Seg ( indx (D2,D1,1))))) by A49, A55, FINSEQ_1:def 15;

                  then 1 in (( dom D2) /\ ( Seg ( indx (D2,D1,1)))) by RELAT_1: 61;

                  then

                   A59: 1 in ( dom D2) by XBOOLE_0:def 4;

                  

                   A60: ( divset (D2,i)) = [.( lower_bound ( divset (D2,1))), ( upper_bound ( divset (D2,1))).] by A57, Th2

                  .= [.( lower_bound A), ( upper_bound ( divset (D2,1))).] by A59, Def3

                  .= [.( lower_bound A), (D2 . 1).] by A59, Def3;

                  ( divset (DD2,i)) = [.( lower_bound ( divset (DD2,1))), ( upper_bound ( divset (DD2,1))).] by A57, Th2

                  .= [.( lower_bound B), ( upper_bound ( divset (DD2,1))).] by A55, A57, Def3

                  .= [.( lower_bound B), (DD2 . 1).] by A55, A57, Def3

                  .= [.( lower_bound B), ((D2 | ( indx (D2,D1,1))) . 1).] by A45, A53, A57

                  .= [.( lower_bound B), ((D2 | ( Seg ( indx (D2,D1,1)))) . 1).] by FINSEQ_1:def 15

                  .= [.( lower_bound B), (D2 . 1).] by A58, FUNCT_1: 47

                  .= [.( lower_bound A), (D2 . 1).] by A5, Def3;

                  hence thesis by A60;

                end;

                  suppose

                   A61: i <> 1;

                  

                   A62: (i - 1) in ( dom (D2 | ( Seg ( indx (D2,D1,1)))))

                  proof

                    i is non trivial by A51, A61, NAT_2:def 1;

                    then

                     A63: i >= (1 + 1) by NAT_2: 29;

                    then

                     A64: 1 <= (i - 1) by XREAL_1: 19;

                    

                     A65: ex j be Nat st i = (1 + j) by A51, NAT_1: 10;

                    

                     A66: (i - 1) <= (( indx (D2,D1,1)) - 0 ) by A43, A53, XREAL_1: 13;

                    then (i - 1) <= ( len D2) by A37, XXREAL_0: 2;

                    then (i - 1) in ( Seg ( len D2)) by A65, A64, FINSEQ_1: 1;

                    then

                     A67: (i - 1) in ( dom D2) by FINSEQ_1:def 3;

                    (i - 1) >= 1 by A63, XREAL_1: 19;

                    then (i - 1) in ( Seg ( indx (D2,D1,1))) by A65, A66, FINSEQ_1: 1;

                    then (i - 1) in (( dom D2) /\ ( Seg ( indx (D2,D1,1)))) by A67, XBOOLE_0:def 4;

                    hence thesis by RELAT_1: 61;

                  end;

                  (DD2 . (i - 1)) = ((D2 | ( indx (D2,D1,1))) . (i - 1)) by A44, A45, FINSEQ_1: 14

                  .= ((D2 | ( Seg ( indx (D2,D1,1)))) . (i - 1)) by FINSEQ_1:def 15;

                  then

                   A68: (DD2 . (i - 1)) = (D2 . (i - 1)) by A62, FUNCT_1: 47;

                  i <= ( len D2) by A43, A37, A53, XXREAL_0: 2;

                  then i in ( Seg ( len D2)) by A51, FINSEQ_1: 1;

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

                  then i in (( dom D2) /\ ( Seg ( indx (D2,D1,1)))) by A43, A54, XBOOLE_0:def 4;

                  then

                   A69: i in ( dom (D2 | ( Seg ( indx (D2,D1,1))))) by RELAT_1: 61;

                  (DD2 . i) = ((D2 | ( indx (D2,D1,1))) . i) by A44, A45, FINSEQ_1: 14

                  .= ((D2 | ( Seg ( indx (D2,D1,1)))) . i) by FINSEQ_1:def 15;

                  then

                   A70: (DD2 . i) = (D2 . i) by A69, FUNCT_1: 47;

                  

                   A71: ( divset (D2,i)) = [.( lower_bound ( divset (D2,i))), ( upper_bound ( divset (D2,i))).] by Th2

                  .= [.(D2 . (i - 1)), ( upper_bound ( divset (D2,i))).] by A56, A61, Def3

                  .= [.(D2 . (i - 1)), (D2 . i).] by A56, A61, Def3;

                  ( divset (DD2,i)) = [.( lower_bound ( divset (DD2,i))), ( upper_bound ( divset (DD2,i))).] by Th2

                  .= [.(DD2 . (i - 1)), ( upper_bound ( divset (DD2,i))).] by A55, A61, Def3

                  .= [.(D2 . (i - 1)), (D2 . i).] by A55, A61, A68, A70, Def3;

                  hence thesis by A71;

                end;

              end;

              hence thesis;

            end;

            then

             A72: (( upper_volume (g,DD2)) . i) = (( upper_bound ( rng (g | ( divset (D2,i))))) * ( vol ( divset (D2,i)))) by A55, Def5;

            ( Seg ( indx (D2,D1,1))) c= ( Seg ( len D2)) by A41, FINSEQ_1: 5;

            then i in ( Seg ( len D2)) by A43, A54;

            then

             A73: i in ( dom D2) by FINSEQ_1:def 3;

            

             A74: i in ( dom DD2) by A54, FINSEQ_1:def 3;

             A75:

            now

              per cases ;

                suppose

                 A76: i = 1;

                then 1 in ( dom (D2 | ( Seg ( indx (D2,D1,1))))) by A49, A74, FINSEQ_1:def 15;

                then 1 in (( dom D2) /\ ( Seg ( indx (D2,D1,1)))) by RELAT_1: 61;

                then

                 A77: 1 in ( dom D2) by XBOOLE_0:def 4;

                then

                 A78: (D2 . 1) <= (D2 . ( indx (D2,D1,1))) by A34, A36, SEQ_4: 137;

                ( lower_bound ( divset (D2,i))) = ( lower_bound A) by A76, A77, Def3;

                then

                 A79: ( lower_bound ( divset (D2,i))) = ( lower_bound ( divset (D1,1))) by A5, Def3;

                ( upper_bound ( divset (D2,i))) = (D2 . 1) by A76, A77, Def3;

                then ( upper_bound ( divset (D2,i))) <= (D1 . 1) by A1, A5, A78, Def18;

                then

                 A80: ( upper_bound ( divset (D2,i))) <= ( upper_bound ( divset (D1,1))) by A5, Def3;

                ( lower_bound ( divset (D1,1))) <= ( upper_bound ( divset (D1,1))) by SEQ_4: 11;

                hence ( lower_bound ( divset (D2,i))) in [.( lower_bound ( divset (D1,1))), ( upper_bound ( divset (D1,1))).] by A79, XXREAL_1: 1;

                ( lower_bound ( divset (D2,i))) <= ( upper_bound ( divset (D2,i))) by SEQ_4: 11;

                then ( upper_bound ( divset (D2,i))) in { r : ( lower_bound ( divset (D1,1))) <= r & r <= ( upper_bound ( divset (D1,1))) } by A79, A80;

                hence ( upper_bound ( divset (D2,i))) in [.( lower_bound ( divset (D1,1))), ( upper_bound ( divset (D1,1))).] by RCOMP_1:def 1;

              end;

                suppose

                 A81: i <> 1;

                then i is non trivial by A51, NAT_2:def 1;

                then i >= (1 + 1) by NAT_2: 29;

                then

                 A82: 1 <= (i - 1) by XREAL_1: 19;

                

                 A83: ex j be Nat st i = (1 + j) by A51, NAT_1: 10;

                

                 A84: ( rng D2) c= A by Def1;

                

                 A85: ( lower_bound ( divset (D2,i))) = (D2 . (i - 1)) by A73, A81, Def3;

                

                 A86: ( lower_bound ( divset (D1,1))) = ( lower_bound A) by A5, Def3;

                

                 A87: (i - 1) <= (( indx (D2,D1,1)) - 0 ) by A43, A53, XREAL_1: 13;

                then (i - 1) <= ( len D2) by A37, XXREAL_0: 2;

                then (i - 1) in ( Seg ( len D2)) by A83, A82, FINSEQ_1: 1;

                then

                 A88: (i - 1) in ( dom D2) by FINSEQ_1:def 3;

                then (D2 . (i - 1)) in ( rng D2) by FUNCT_1:def 3;

                then

                 A89: ( lower_bound ( divset (D2,i))) >= ( lower_bound ( divset (D1,1))) by A85, A86, A84, SEQ_4:def 2;

                

                 A90: ( upper_bound ( divset (D1,1))) = (D1 . 1) by A5, Def3;

                (D2 . (i - 1)) <= (D2 . ( indx (D2,D1,1))) by A34, A87, A88, SEQ_4: 137;

                then ( lower_bound ( divset (D2,i))) <= ( upper_bound ( divset (D1,1))) by A1, A5, A85, A90, Def18;

                then ( lower_bound ( divset (D2,i))) in { r : ( lower_bound ( divset (D1,1))) <= r & r <= ( upper_bound ( divset (D1,1))) } by A89;

                hence ( lower_bound ( divset (D2,i))) in [.( lower_bound ( divset (D1,1))), ( upper_bound ( divset (D1,1))).] by RCOMP_1:def 1;

                

                 A91: ( upper_bound ( divset (D2,i))) = (D2 . i) by A73, A81, Def3;

                (D2 . i) in ( rng D2) by A73, FUNCT_1:def 3;

                then

                 A92: ( upper_bound ( divset (D2,i))) >= ( lower_bound ( divset (D1,1))) by A91, A86, A84, SEQ_4:def 2;

                (D2 . i) <= (D2 . ( indx (D2,D1,1))) by A43, A34, A53, A73, SEQ_4: 137;

                then ( upper_bound ( divset (D2,i))) <= ( upper_bound ( divset (D1,1))) by A1, A5, A91, A90, Def18;

                then ( upper_bound ( divset (D2,i))) in { r : ( lower_bound ( divset (D1,1))) <= r & r <= ( upper_bound ( divset (D1,1))) } by A92;

                hence ( upper_bound ( divset (D2,i))) in [.( lower_bound ( divset (D1,1))), ( upper_bound ( divset (D1,1))).] by RCOMP_1:def 1;

              end;

            end;

            

             A93: ( divset (D1,1)) = [.( lower_bound ( divset (D1,1))), ( upper_bound ( divset (D1,1))).] by Th2;

            

             A94: ( Seg ( indx (D2,D1,1))) c= ( Seg ( len D2)) by A41, FINSEQ_1: 5;

            then i in ( Seg ( len D2)) by A43, A54;

            then

             A95: i in ( dom D2) by FINSEQ_1:def 3;

            ( divset (D2,i)) = [.( lower_bound ( divset (D2,i))), ( upper_bound ( divset (D2,i))).] by Th2;

            then

             A96: ( divset (D2,i)) c= ( divset (D1,1)) by A93, A75, XXREAL_2:def 12;

            

             A97: ( dom (( upper_volume (f,D2)) | ( Seg ( indx (D2,D1,1))))) = (( dom ( upper_volume (f,D2))) /\ ( Seg ( indx (D2,D1,1)))) by RELAT_1: 61

            .= (( Seg ( len ( upper_volume (f,D2)))) /\ ( Seg ( indx (D2,D1,1)))) by FINSEQ_1:def 3

            .= (( Seg ( len D2)) /\ ( Seg ( indx (D2,D1,1)))) by Def5

            .= ( Seg ( indx (D2,D1,1))) by A94, XBOOLE_1: 28;

            ((( upper_volume (f,D2)) | ( indx (D2,D1,1))) . i) = ((( upper_volume (f,D2)) | ( Seg ( indx (D2,D1,1)))) . i) by FINSEQ_1:def 15

            .= (( upper_volume (f,D2)) . i) by A43, A54, A97, FUNCT_1: 47

            .= (( upper_bound ( rng (f | ( divset (D2,i))))) * ( vol ( divset (D2,i)))) by A95, Def5;

            hence thesis by A72, A96, FUNCT_1: 51;

          end;

          ( len ( upper_volume (g,DD1))) = ( len (( upper_volume (f,D1)) | 1)) by A10;

          then

           A98: ( upper_volume (g,DD1)) = (( upper_volume (f,D1)) | 1) by A18, FINSEQ_1: 14;

          

           A99: ( indx (D2,D1,1)) <= ( len ( upper_volume (f,D2))) by A41, Def5;

          ( len ( upper_volume (g,DD2))) = ( indx (D2,D1,1)) by A43, Def5;

          then

           A100: ( len ( upper_volume (g,DD2))) = ( len (( upper_volume (f,D2)) | ( indx (D2,D1,1)))) by A99, FINSEQ_1: 59;

          ( dom g) = (A /\ ( divset (D1,1))) by A4, FUNCT_2:def 1;

          then ( dom g) = ( divset (D1,1)) by A5, Th6, XBOOLE_1: 28;

          then g is total by PARTFUN1:def 2;

          then ( upper_sum (g,DD1)) >= ( upper_sum (g,DD2)) by A11, A28, Th28;

          hence thesis by A98, A100, A50, FINSEQ_1: 14;

        end;

        

         A101: for k be non zero Nat st P[k] holds P[(k + 1)]

        proof

          let k be non zero Nat;

          assume

           A102: k in ( dom D1) implies ( Sum (( upper_volume (f,D1)) | k)) >= ( Sum (( upper_volume (f,D2)) | ( indx (D2,D1,k))));

          assume

           A103: (k + 1) in ( dom D1);

          then

           A104: (k + 1) in ( Seg ( len D1)) by FINSEQ_1:def 3;

          then

           A105: 1 <= (k + 1) by FINSEQ_1: 1;

          

           A106: (k + 1) <= ( len D1) by A104, FINSEQ_1: 1;

          now

            per cases ;

              suppose 1 = (k + 1);

              hence thesis by A3, A103;

            end;

              suppose

               A107: 1 <> (k + 1);

              set IDK = ( indx (D2,D1,k));

              set IDK1 = ( indx (D2,D1,(k + 1)));

              set K1D2 = (( upper_volume (f,D2)) | ( indx (D2,D1,(k + 1))));

              set KD1 = (( upper_volume (f,D1)) | k);

              set K1D1 = (( upper_volume (f,D1)) | (k + 1));

              set n = (k + 1);

              

               A108: (k + 1) <= ( len ( upper_volume (f,D1))) by A106, Def5;

              then

               A109: ( len K1D1) = (k + 1) by FINSEQ_1: 59;

              then

              consider p1,q1 be FinSequence of REAL such that

               A110: ( len p1) = k and

               A111: ( len q1) = 1 and

               A112: K1D1 = (p1 ^ q1) by FINSEQ_2: 23;

              

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

              then

               A114: k <= ( len D1) by A106, XXREAL_0: 2;

              then

               A115: k <= ( len ( upper_volume (f,D1))) by Def5;

              then

               A116: ( len p1) = ( len KD1) by A110, FINSEQ_1: 59;

              for i be Nat st 1 <= i & i <= ( len p1) holds (p1 . i) = (KD1 . i)

              proof

                let i be Nat;

                assume that

                 A117: 1 <= i and

                 A118: i <= ( len p1);

                

                 A119: i in ( Seg ( len p1)) by A117, A118, FINSEQ_1: 1;

                then

                 A120: i in ( dom KD1) by A116, FINSEQ_1:def 3;

                then

                 A121: i in ( dom (( upper_volume (f,D1)) | ( Seg k))) by FINSEQ_1:def 15;

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

                then

                 A122: ( Seg k) c= ( Seg (k + 1)) by FINSEQ_1: 5;

                

                 A123: ( dom K1D1) = ( Seg ( len K1D1)) by FINSEQ_1:def 3

                .= ( Seg (k + 1)) by A108, FINSEQ_1: 59;

                ( dom KD1) = ( Seg ( len KD1)) by FINSEQ_1:def 3

                .= ( Seg k) by A115, FINSEQ_1: 59;

                then i in ( dom K1D1) by A120, A122, A123;

                then

                 A124: i in ( dom (( upper_volume (f,D1)) | ( Seg (k + 1)))) by FINSEQ_1:def 15;

                

                 A125: (K1D1 . i) = ((( upper_volume (f,D1)) | ( Seg (k + 1))) . i) by FINSEQ_1:def 15

                .= (( upper_volume (f,D1)) . i) by A124, FUNCT_1: 47;

                

                 A126: (KD1 . i) = ((( upper_volume (f,D1)) | ( Seg k)) . i) by FINSEQ_1:def 15

                .= (( upper_volume (f,D1)) . i) by A121, FUNCT_1: 47;

                i in ( dom p1) by A119, FINSEQ_1:def 3;

                hence thesis by A112, A126, A125, FINSEQ_1:def 7;

              end;

              then

               A127: p1 = KD1 by A116, FINSEQ_1: 14;

              

               A128: ( indx (D2,D1,(k + 1))) in ( dom D2) by A1, A103, Def18;

              then

               A129: ( indx (D2,D1,(k + 1))) in ( Seg ( len D2)) by FINSEQ_1:def 3;

              then

               A130: 1 <= ( indx (D2,D1,(k + 1))) by FINSEQ_1: 1;

              n is non trivial by A107, NAT_2:def 1;

              then n >= 2 by NAT_2: 29;

              then k >= ((1 + 1) - 1) by XREAL_1: 20;

              then

               A131: k in ( Seg ( len D1)) by A114, FINSEQ_1: 1;

              then

               A132: k in ( dom D1) by FINSEQ_1:def 3;

              then

               A133: ( indx (D2,D1,k)) in ( dom D2) by A1, Def18;

              

               A134: ( indx (D2,D1,k)) < ( indx (D2,D1,(k + 1)))

              proof

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

                then

                 A135: (D1 . k) < (D1 . (k + 1)) by A103, A132, SEQM_3:def 1;

                assume ( indx (D2,D1,k)) >= ( indx (D2,D1,(k + 1)));

                then

                 A136: (D2 . ( indx (D2,D1,k))) >= (D2 . ( indx (D2,D1,(k + 1)))) by A133, A128, SEQ_4: 137;

                (D1 . k) = (D2 . ( indx (D2,D1,k))) by A1, A132, Def18;

                hence contradiction by A1, A103, A136, A135, Def18;

              end;

              

               A137: ( indx (D2,D1,(k + 1))) >= ( indx (D2,D1,k))

              proof

                assume ( indx (D2,D1,(k + 1))) < ( indx (D2,D1,k));

                then

                 A138: (D2 . ( indx (D2,D1,(k + 1)))) < (D2 . ( indx (D2,D1,k))) by A133, A128, SEQM_3:def 1;

                (D1 . (k + 1)) = (D2 . ( indx (D2,D1,(k + 1)))) by A1, A103, Def18;

                then (D1 . (k + 1)) < (D1 . k) by A1, A132, A138, Def18;

                hence contradiction by A103, A132, NAT_1: 11, SEQ_4: 137;

              end;

              then

              consider ID be Nat such that

               A139: ( indx (D2,D1,(k + 1))) = (( indx (D2,D1,k)) + ID) by NAT_1: 10;

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

              

               A140: ( len ( upper_volume (f,D2))) = ( len D2) by Def5;

              then

               A141: ( indx (D2,D1,(k + 1))) <= ( len ( upper_volume (f,D2))) by A129, FINSEQ_1: 1;

              then ( len K1D2) = (IDK + (IDK1 - IDK)) by FINSEQ_1: 59;

              then

              consider p2,q2 be FinSequence of REAL such that

               A142: ( len p2) = IDK and

               A143: ( len q2) = (IDK1 - IDK) and

               A144: K1D2 = (p2 ^ q2) by A139, FINSEQ_2: 23;

              ( indx (D2,D1,k)) in ( dom D2) by A1, A132, Def18;

              then

               A145: ( indx (D2,D1,k)) in ( Seg ( len ( upper_volume (f,D2)))) by A140, FINSEQ_1:def 3;

              then

               A146: 1 <= ( indx (D2,D1,k)) by FINSEQ_1: 1;

              set KD2 = (( upper_volume (f,D2)) | ( indx (D2,D1,k)));

              

               A147: ( Sum K1D2) = (( Sum p2) + ( Sum q2)) by A144, RVSUM_1: 75;

              

               A148: ( indx (D2,D1,k)) <= ( len ( upper_volume (f,D2))) by A145, FINSEQ_1: 1;

              then

               A149: ( len p2) = ( len KD2) by A142, FINSEQ_1: 59;

              for i be Nat st 1 <= i & i <= ( len p2) holds (p2 . i) = (KD2 . i)

              proof

                let i be Nat;

                assume that

                 A150: 1 <= i and

                 A151: i <= ( len p2);

                

                 A152: i in ( Seg ( len p2)) by A150, A151, FINSEQ_1: 1;

                then

                 A153: i in ( dom KD2) by A149, FINSEQ_1:def 3;

                then

                 A154: i in ( dom (( upper_volume (f,D2)) | ( Seg ( indx (D2,D1,k))))) by FINSEQ_1:def 15;

                

                 A155: ( dom K1D2) = ( Seg ( len K1D2)) by FINSEQ_1:def 3

                .= ( Seg ( indx (D2,D1,(k + 1)))) by A141, FINSEQ_1: 59;

                

                 A156: ( Seg ( indx (D2,D1,k))) c= ( Seg ( indx (D2,D1,(k + 1)))) by A137, FINSEQ_1: 5;

                ( dom KD2) = ( Seg ( len KD2)) by FINSEQ_1:def 3

                .= ( Seg ( indx (D2,D1,k))) by A148, FINSEQ_1: 59;

                then i in ( dom K1D2) by A153, A156, A155;

                then

                 A157: i in ( dom (( upper_volume (f,D2)) | ( Seg ( indx (D2,D1,(k + 1)))))) by FINSEQ_1:def 15;

                

                 A158: (K1D2 . i) = ((( upper_volume (f,D2)) | ( Seg ( indx (D2,D1,(k + 1))))) . i) by FINSEQ_1:def 15

                .= (( upper_volume (f,D2)) . i) by A157, FUNCT_1: 47;

                

                 A159: (KD2 . i) = ((( upper_volume (f,D2)) | ( Seg ( indx (D2,D1,k)))) . i) by FINSEQ_1:def 15

                .= (( upper_volume (f,D2)) . i) by A154, FUNCT_1: 47;

                i in ( dom p2) by A152, FINSEQ_1:def 3;

                hence thesis by A144, A159, A158, FINSEQ_1:def 7;

              end;

              then

               A160: p2 = KD2 by A149, FINSEQ_1: 14;

              

               A161: ( indx (D2,D1,(k + 1))) <= ( len D2) by A129, FINSEQ_1: 1;

              

               A162: ID = (( indx (D2,D1,(k + 1))) - ( indx (D2,D1,k))) by A139;

              

               A163: ( Sum q1) >= ( Sum q2)

              proof

                set MD2 = ( mid (D2,(( indx (D2,D1,k)) + 1),( indx (D2,D1,(k + 1)))));

                set MD1 = ( mid (D1,(k + 1),(k + 1)));

                set DD1 = ( divset (D1,(k + 1)));

                set g = (f | DD1);

                

                 A164: 1 <= (( indx (D2,D1,k)) + 1) by NAT_1: 11;

                reconsider g as PartFunc of DD1, REAL by PARTFUN1: 10;

                ((k + 1) - 1) = k;

                then

                 A165: ( lower_bound DD1) = (D1 . k) by A103, A107, Def3;

                (D2 . ( indx (D2,D1,(k + 1)))) = (D1 . (k + 1)) by A1, A103, Def18;

                then

                 A166: (D2 . ( indx (D2,D1,(k + 1)))) = ( upper_bound DD1) by A103, A107, Def3;

                

                 A167: (( indx (D2,D1,k)) + 1) <= ( indx (D2,D1,(k + 1))) by A134, NAT_1: 13;

                then

                 A168: (( indx (D2,D1,k)) + 1) <= ( len D2) by A161, XXREAL_0: 2;

                then (( indx (D2,D1,k)) + 1) in ( Seg ( len D2)) by A164, FINSEQ_1: 1;

                then

                 A169: (( indx (D2,D1,k)) + 1) in ( dom D2) by FINSEQ_1:def 3;

                then (D2 . (( indx (D2,D1,k)) + 1)) >= (D2 . ( indx (D2,D1,k))) by A133, NAT_1: 11, SEQ_4: 137;

                then (D2 . (( indx (D2,D1,k)) + 1)) >= ( lower_bound DD1) by A1, A132, A165, Def18;

                then

                reconsider MD2 as Division of DD1 by A128, A167, A169, A166, Th35;

                

                 A170: ((( indx (D2,D1,(k + 1))) -' (( indx (D2,D1,k)) + 1)) + 1) = ((( indx (D2,D1,(k + 1))) - (( indx (D2,D1,k)) + 1)) + 1) by A167, XREAL_1: 233

                .= (( indx (D2,D1,(k + 1))) - ( indx (D2,D1,k)));

                

                 A171: for n be Nat st 1 <= n & n <= ( len q2) holds (q2 . n) = (( upper_volume (g,MD2)) . n)

                proof

                  

                   A172: ( dom K1D2) = ( Seg ( len K1D2)) by FINSEQ_1:def 3

                  .= ( Seg ( indx (D2,D1,(k + 1)))) by A141, FINSEQ_1: 59;

                  then

                   A173: ( dom K1D2) c= ( Seg ( len D2)) by A161, FINSEQ_1: 5;

                  then

                   A174: ( dom K1D2) c= ( dom D2) by FINSEQ_1:def 3;

                  

                   A175: ( len ( mid (D2,(( indx (D2,D1,k)) + 1),( indx (D2,D1,(k + 1)))))) = ID by A130, A161, A139, A167, A168, A164, A170, FINSEQ_6: 118;

                  let n be Nat;

                  assume that

                   A176: 1 <= n and

                   A177: n <= ( len q2);

                  n in ( Seg ( len q2)) by A176, A177, FINSEQ_1: 1;

                  then

                   A178: n in ( dom q2) by FINSEQ_1:def 3;

                  then

                   A179: (( indx (D2,D1,k)) + n) in ( dom K1D2) by A142, A144, FINSEQ_1: 28;

                  then

                   A180: (( indx (D2,D1,k)) + n) in ( dom (( upper_volume (f,D2)) | ( Seg ( indx (D2,D1,(k + 1)))))) by FINSEQ_1:def 15;

                  

                   A181: (q2 . n) = (K1D2 . (( indx (D2,D1,k)) + n)) by A142, A144, A178, FINSEQ_1:def 7

                  .= ((( upper_volume (f,D2)) | ( Seg ( indx (D2,D1,(k + 1))))) . (( indx (D2,D1,k)) + n)) by FINSEQ_1:def 15

                  .= (( upper_volume (f,D2)) . (( indx (D2,D1,k)) + n)) by A180, FUNCT_1: 47

                  .= (( upper_bound ( rng (f | ( divset (D2,(( indx (D2,D1,k)) + n)))))) * ( vol ( divset (D2,(( indx (D2,D1,k)) + n))))) by A179, A174, Def5;

                  (( indx (D2,D1,k)) + n) in ( Seg ( len D2)) by A179, A173;

                  then

                   A182: (( indx (D2,D1,k)) + n) in ( dom D2) by FINSEQ_1:def 3;

                  (( indx (D2,D1,k)) + n) <= ( indx (D2,D1,(k + 1))) by A172, A179, FINSEQ_1: 1;

                  then

                   A183: n <= ID by A162, XREAL_1: 19;

                  then n in ( Seg ID) by A176, FINSEQ_1: 1;

                  then

                   A184: n in ( dom MD2) by A175, FINSEQ_1:def 3;

                  n in ( Seg ( len ( mid (D2,(( indx (D2,D1,k)) + 1),( indx (D2,D1,(k + 1))))))) by A176, A183, A175, FINSEQ_1: 1;

                  then

                   A185: n in ( dom ( mid (D2,(( indx (D2,D1,k)) + 1),( indx (D2,D1,(k + 1)))))) by FINSEQ_1:def 3;

                  

                   A186: 1 <= (( indx (D2,D1,k)) + n) by A172, A179, FINSEQ_1: 1;

                  

                   A187: ( divset (MD2,n)) = ( divset (D2,(( indx (D2,D1,k)) + n))) & ( divset (D2,(( indx (D2,D1,k)) + n))) c= ( divset (D1,(k + 1)))

                  proof

                    now

                      per cases ;

                        suppose

                         A188: n = 1;

                        then

                         A189: (( indx (D2,D1,k)) + 1) <= ( len D2) by A179, A173, FINSEQ_1: 1;

                        

                         A190: 1 <= (( indx (D2,D1,k)) + 1) by A172, A179, A188, FINSEQ_1: 1;

                        

                         A191: ( upper_bound ( divset (MD2,1))) = (( mid (D2,(( indx (D2,D1,k)) + 1),( indx (D2,D1,(k + 1))))) . 1) by A184, A188, Def3

                        .= (D2 . (1 + ( indx (D2,D1,k)))) by A130, A161, A190, A189, FINSEQ_6: 118;

                        

                         A192: (( indx (D2,D1,k)) + 1) <> 1 by A146, NAT_1: 13;

                        

                         A193: ((k + 1) - 1) = k;

                        

                         A194: ( lower_bound ( divset (MD2,1))) = ( lower_bound ( divset (D1,(k + 1)))) by A184, A188, Def3

                        .= (D1 . k) by A103, A107, A193, Def3;

                        

                         A195: ( divset (D2,(( indx (D2,D1,k)) + n))) = [.( lower_bound ( divset (D2,(( indx (D2,D1,k)) + 1)))), ( upper_bound ( divset (D2,(( indx (D2,D1,k)) + 1)))).] by A188, Th2

                        .= [.(D2 . ((( indx (D2,D1,k)) + 1) - 1)), ( upper_bound ( divset (D2,(( indx (D2,D1,k)) + 1)))).] by A169, A192, Def3

                        .= [.(D2 . ( indx (D2,D1,k))), (D2 . (( indx (D2,D1,k)) + 1)).] by A169, A192, Def3

                        .= [.(D1 . k), (D2 . (( indx (D2,D1,k)) + 1)).] by A1, A132, Def18;

                        hence ( divset (MD2,n)) = ( divset (D2,(( indx (D2,D1,k)) + n))) by A188, A194, A191, Th2;

                        ( divset (MD2,n)) = [.(D1 . k), (D2 . (( indx (D2,D1,k)) + 1)).] by A188, A194, A191, Th2;

                        hence thesis by A184, A195, Th6;

                      end;

                        suppose

                         A196: n <> 1;

                        

                         A197: (( indx (D2,D1,k)) + n) <> 1

                        proof

                          assume (( indx (D2,D1,k)) + n) = 1;

                          then ( indx (D2,D1,k)) = (1 - n);

                          then (n + 1) <= 1 by A146, XREAL_1: 19;

                          then n <= (1 - 1) by XREAL_1: 19;

                          hence contradiction by A176, NAT_1: 3;

                        end;

                        

                         A198: ( divset (D2,(( indx (D2,D1,k)) + n))) = [.( lower_bound ( divset (D2,(( indx (D2,D1,k)) + n)))), ( upper_bound ( divset (D2,(( indx (D2,D1,k)) + n)))).] by Th2

                        .= [.(D2 . ((( indx (D2,D1,k)) + n) - 1)), ( upper_bound ( divset (D2,(( indx (D2,D1,k)) + n)))).] by A182, A197, Def3

                        .= [.(D2 . ((( indx (D2,D1,k)) + n) - 1)), (D2 . (( indx (D2,D1,k)) + n)).] by A182, A197, Def3;

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

                        then (n - 1) <= n by XREAL_1: 20;

                        then

                         A199: (n - 1) <= ( len MD2) by A183, A175, XXREAL_0: 2;

                        consider n1 be Nat such that

                         A200: n = (1 + n1) by A176, NAT_1: 10;

                        n is non trivial by A176, A196, NAT_2:def 1;

                        then n >= (1 + 1) by NAT_2: 29;

                        then

                         A201: 1 <= (n - 1) by XREAL_1: 19;

                        

                         A202: (( indx (D2,D1,k)) + 1) <= ( indx (D2,D1,(k + 1))) by A134, NAT_1: 13;

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

                        

                         A203: ((n1 + (( indx (D2,D1,k)) + 1)) -' 1) = ((( indx (D2,D1,k)) + n) - 1) by A186, A200, XREAL_1: 233;

                        

                         A204: ((n + (( indx (D2,D1,k)) + 1)) -' 1) = (((n + ( indx (D2,D1,k))) + 1) - 1) by NAT_1: 11, XREAL_1: 233

                        .= (( indx (D2,D1,k)) + n);

                        

                         A205: ( lower_bound ( divset (MD2,n))) = (MD2 . (n - 1)) by A184, A196, Def3

                        .= (D2 . ((( indx (D2,D1,k)) + n) - 1)) by A130, A161, A168, A164, A202, A200, A203, A201, A199, FINSEQ_6: 118;

                        

                         A206: ( upper_bound ( divset (MD2,n))) = (MD2 . n) by A184, A196, Def3

                        .= (D2 . (( indx (D2,D1,k)) + n)) by A130, A161, A168, A164, A176, A183, A175, A202, A204, FINSEQ_6: 118;

                        hence ( divset (MD2,n)) = ( divset (D2,(( indx (D2,D1,k)) + n))) by A205, A198, Th2;

                        ( divset (MD2,n)) = [.(D2 . ((( indx (D2,D1,k)) + n) - 1)), (D2 . (( indx (D2,D1,k)) + n)).] by A205, A206, Th2;

                        hence thesis by A184, A198, Th6;

                      end;

                    end;

                    hence thesis;

                  end;

                  then (g | ( divset (MD2,n))) = (f | ( divset (D2,(( indx (D2,D1,k)) + n)))) by FUNCT_1: 51;

                  hence thesis by A185, A181, A187, Def5;

                end;

                ((k + 1) - 1) = k;

                then

                 A207: ( lower_bound DD1) = (D1 . k) by A103, A107, Def3;

                (D1 . (k + 1)) = ( upper_bound DD1) by A103, A107, Def3;

                then

                reconsider MD1 as Division of DD1 by A103, A113, A132, A207, Th35, SEQ_4: 137;

                

                 A208: (g | ( divset (D1,(k + 1)))) is bounded_above

                proof

                  consider a be Real such that

                   A209: for x be object st x in (A /\ ( dom f)) holds (f . x) <= a by A2, RFUNCT_1: 70;

                  for x be object st x in (( divset (D1,(k + 1))) /\ ( dom g)) holds (g . x) <= a

                  proof

                    let x be object;

                    

                     A210: ( dom g) c= ( dom f) by RELAT_1: 60;

                    assume x in (( divset (D1,(k + 1))) /\ ( dom g));

                    then

                     A211: x in ( dom g) by XBOOLE_0:def 4;

                    

                     A212: (A /\ ( dom f)) = ( dom f) by XBOOLE_1: 28;

                    then x in (A /\ ( dom f)) by A211, A210;

                    then

                    reconsider x as Element of A;

                    (f . x) <= a by A209, A211, A212, A210;

                    hence thesis by A211, FUNCT_1: 47;

                  end;

                  hence thesis by RFUNCT_1: 70;

                end;

                ( len MD1) = (((k + 1) -' (k + 1)) + 1) by A105, A106, FINSEQ_6: 118;

                then

                 A213: ( len MD1) = (((k + 1) - (k + 1)) + 1) by XREAL_1: 233;

                then

                 A214: ( dom q1) = ( dom MD1) by A111, FINSEQ_3: 29;

                

                 A215: for n be Nat st 1 <= n & n <= ( len q1) holds (q1 . n) = (( upper_volume (g,MD1)) . n)

                proof

                  (k + 1) in ( Seg ( len K1D1)) by A109, FINSEQ_1: 4;

                  then (k + 1) in ( dom K1D1) by FINSEQ_1:def 3;

                  then

                   A216: (k + 1) in ( dom (( upper_volume (f,D1)) | ( Seg (k + 1)))) by FINSEQ_1:def 15;

                  

                   A217: (MD1 . 1) = (D1 . (k + 1)) by A105, A106, FINSEQ_6: 118;

                  1 in ( Seg ( len MD1)) by A213, FINSEQ_1: 3;

                  then

                   A218: 1 in ( dom MD1) by FINSEQ_1:def 3;

                  ( divset (MD1,1)) = [.( lower_bound ( divset (MD1,1))), ( upper_bound ( divset (MD1,1))).] by Th2;

                  

                  then

                   A219: ( divset (MD1,1)) = [.( lower_bound DD1), ( upper_bound ( divset (MD1,1))).] by A218, Def3

                  .= [.( lower_bound DD1), (D1 . (k + 1)).] by A218, A217, Def3;

                  ((k + 1) - 1) = k;

                  then

                   A220: ( lower_bound DD1) = (D1 . k) by A103, A107, Def3;

                  let n be Nat;

                  assume that

                   A221: 1 <= n and

                   A222: n <= ( len q1);

                  

                   A223: n = 1 by A111, A221, A222, XXREAL_0: 1;

                  n in ( Seg ( len q1)) by A221, A222, FINSEQ_1: 1;

                  then

                   A224: n in ( dom q1) by FINSEQ_1:def 3;

                  ( upper_bound DD1) = (D1 . (k + 1)) by A103, A107, Def3;

                  then ( divset (D1,(k + 1))) = [.(D1 . k), (D1 . (k + 1)).] by A220, Th2;

                  then

                   A225: (( upper_volume (g,MD1)) . n) = (( upper_bound ( rng (g | ( divset (D1,(k + 1)))))) * ( vol ( divset (D1,(k + 1))))) by A214, A223, A224, A219, A220, Def5;

                  (K1D1 . (k + 1)) = ((( upper_volume (f,D1)) | ( Seg (k + 1))) . (k + 1)) by FINSEQ_1:def 15

                  .= (( upper_volume (f,D1)) . (k + 1)) by A216, FUNCT_1: 47;

                  

                  then (q1 . n) = (( upper_volume (f,D1)) . (k + 1)) by A110, A112, A223, A224, FINSEQ_1:def 7

                  .= (( upper_bound ( rng (f | ( divset (D1,(k + 1)))))) * ( vol ( divset (D1,(k + 1))))) by A103, Def5;

                  hence thesis by A225;

                end;

                ( len q1) = ( len ( upper_volume (g,MD1))) by A111, A213, Def5;

                then

                 A226: q1 = ( upper_volume (g,MD1)) by A215, FINSEQ_1: 14;

                ( dom g) = (( dom f) /\ ( divset (D1,(k + 1)))) by RELAT_1: 61;

                then ( dom g) = (A /\ ( divset (D1,(k + 1)))) by FUNCT_2:def 1;

                then ( dom g) = ( divset (D1,(k + 1))) by A103, Th6, XBOOLE_1: 28;

                then

                 A227: g is total by PARTFUN1:def 2;

                ( len MD1) = (((k + 1) -' (k + 1)) + 1) by A105, A106, FINSEQ_6: 118;

                then ( len MD1) = (((k + 1) - (k + 1)) + 1) by XREAL_1: 233;

                then

                 A228: ( upper_sum (g,MD1)) >= ( upper_sum (g,MD2)) by A208, A227, Th28;

                ( len ( upper_volume (g,MD2))) = ( len ( mid (D2,(( indx (D2,D1,k)) + 1),( indx (D2,D1,(k + 1)))))) by Def5

                .= (( indx (D2,D1,(k + 1))) - ( indx (D2,D1,k))) by A130, A161, A167, A168, A164, A170, FINSEQ_6: 118;

                hence thesis by A143, A226, A171, A228, FINSEQ_1: 14;

              end;

              ( Sum K1D1) = (( Sum p1) + ( Sum q1)) by A112, RVSUM_1: 75;

              then ( Sum q1) = (( Sum K1D1) - ( Sum p1));

              then ( Sum K1D1) >= (( Sum q2) + ( Sum p1)) by A163, XREAL_1: 19;

              then (( Sum K1D1) - ( Sum q2)) >= ( Sum p1) by XREAL_1: 19;

              then (( Sum K1D1) - ( Sum q2)) >= ( Sum p2) by A102, A131, A127, A160, FINSEQ_1:def 3, XXREAL_0: 2;

              hence thesis by A147, XREAL_1: 19;

            end;

          end;

          hence thesis;

        end;

        thus for k be non zero Nat holds P[k] from NAT_1:sch 10( A3, A101);

      end;

      hence thesis;

    end;

    theorem :: INTEGRA1:39

    

     Th37: D1 <= D2 & (f | A) is bounded_below implies for i be non zero Element of NAT holds (i in ( dom D1) implies ( Sum (( lower_volume (f,D1)) | i)) <= ( Sum (( lower_volume (f,D2)) | ( indx (D2,D1,i)))))

    proof

      assume that

       A1: D1 <= D2 and

       A2: (f | A) is bounded_below;

      for i be non zero Nat holds i in ( dom D1) implies ( Sum (( lower_volume (f,D1)) | i)) <= ( Sum (( lower_volume (f,D2)) | ( indx (D2,D1,i))))

      proof

        defpred P[ Nat] means $1 in ( dom D1) implies ( Sum (( lower_volume (f,D1)) | $1)) <= ( Sum (( lower_volume (f,D2)) | ( indx (D2,D1,$1))));

        

         A3: P[1]

        proof

          set g = (f | ( divset (D1,1)));

          set B = ( divset (D1,1));

          set DD2 = ( mid (D2,1,( indx (D2,D1,1))));

          set DD1 = ( mid (D1,1,1));

          reconsider g as PartFunc of ( divset (D1,1)), REAL by PARTFUN1: 10;

          

           A4: ( dom g) = (( dom f) /\ ( divset (D1,1))) by RELAT_1: 61;

          assume

           A5: 1 in ( dom D1);

          then

           A6: (D1 . 1) = ( upper_bound B) by Def3;

          then

           A7: (D2 . ( indx (D2,D1,1))) = ( upper_bound B) by A1, A5, Def18;

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

          then

          reconsider DD1 as Division of B by A5, A6, Th35;

          1 in ( Seg ( len D1)) by A5, FINSEQ_1:def 3;

          then

           A8: 1 <= ( len D1) by FINSEQ_1: 1;

          then

           A9: ( len ( mid (D1,1,1))) = ((1 -' 1) + 1) by FINSEQ_6: 118;

          

           A10: ( len ( lower_volume (g,DD1))) = ( len DD1) by Def6

          .= 1 by A9, XREAL_1: 235;

          

           A11: ( len ( mid (D1,1,1))) = 1 by A9, XREAL_1: 235;

          then

           A12: ( len ( mid (D1,1,1))) = ( len (D1 | 1));

          for k be Nat st 1 <= k & k <= ( len ( mid (D1,1,1))) holds (( mid (D1,1,1)) . k) = ((D1 | 1) . k)

          proof

            let k be Nat;

            assume that

             A13: 1 <= k and

             A14: k <= ( len ( mid (D1,1,1)));

            k in ( Seg ( len (D1 | 1))) by A12, A13, A14, FINSEQ_1: 1;

            then k in ( dom (D1 | 1)) by FINSEQ_1:def 3;

            then k in ( dom (D1 | ( Seg 1))) by FINSEQ_1:def 15;

            then

             A15: ((D1 | ( Seg 1)) . k) = (D1 . k) by FUNCT_1: 47;

            

             A16: k = 1 by A11, A13, A14, XXREAL_0: 1;

            then (( mid (D1,1,1)) . k) = (D1 . ((1 + 1) - 1)) by A8, FINSEQ_6: 118;

            hence thesis by A16, A15, FINSEQ_1:def 15;

          end;

          then

           A17: ( mid (D1,1,1)) = (D1 | 1) by A12, FINSEQ_1: 14;

          

           A18: for i be Nat st 1 <= i & i <= ( len ( lower_volume (g,DD1))) holds (( lower_volume (g,DD1)) . i) = ((( lower_volume (f,D1)) | 1) . i)

          proof

            let i be Nat;

            assume that

             A19: 1 <= i and

             A20: i <= ( len ( lower_volume (g,DD1)));

            

             A21: 1 in ( Seg 1) by FINSEQ_1: 3;

            ( dom (D1 | ( Seg 1))) = (( dom D1) /\ ( Seg 1)) by RELAT_1: 61;

            then

             A22: 1 in ( dom (D1 | ( Seg 1))) by A5, A21, XBOOLE_0:def 4;

            ( dom ( lower_volume (f,D1))) = ( Seg ( len ( lower_volume (f,D1)))) by FINSEQ_1:def 3

            .= ( Seg ( len D1)) by Def6;

            

            then

             A23: ( dom (( lower_volume (f,D1)) | ( Seg 1))) = (( Seg ( len D1)) /\ ( Seg 1)) by RELAT_1: 61

            .= ( Seg 1) by A8, FINSEQ_1: 7;

            ( len DD1) = 1 by A9, XREAL_1: 235;

            then

             A24: 1 in ( dom DD1) by A21, FINSEQ_1:def 3;

            

             A25: ((( lower_volume (f,D1)) | 1) . i) = ((( lower_volume (f,D1)) | ( Seg 1)) . i) by FINSEQ_1:def 15

            .= ((( lower_volume (f,D1)) | ( Seg 1)) . 1) by A10, A19, A20, XXREAL_0: 1

            .= (( lower_volume (f,D1)) . 1) by A23, FINSEQ_1: 3, FUNCT_1: 47

            .= (( lower_bound ( rng (f | ( divset (D1,1))))) * ( vol ( divset (D1,1)))) by A5, Def6;

            

             A26: ( divset (D1,1)) = [.( lower_bound ( divset (D1,1))), ( upper_bound ( divset (D1,1))).] by Th2

            .= [.( lower_bound A), ( upper_bound ( divset (D1,1))).] by A5, Def3

            .= [.( lower_bound A), (D1 . 1).] by A5, Def3;

            

             A27: (( lower_volume (g,DD1)) . i) = (( lower_volume (g,DD1)) . 1) by A10, A19, A20, XXREAL_0: 1

            .= (( lower_bound ( rng (g | ( divset (DD1,1))))) * ( vol ( divset (DD1,1)))) by A24, Def6;

            ( divset (DD1,1)) = [.( lower_bound ( divset (DD1,1))), ( upper_bound ( divset (DD1,1))).] by Th2

            .= [.( lower_bound B), ( upper_bound ( divset (DD1,1))).] by A24, Def3

            .= [.( lower_bound B), (DD1 . 1).] by A24, Def3

            .= [.( lower_bound A), ((D1 | 1) . 1).] by A5, A17, Def3

            .= [.( lower_bound A), ((D1 | ( Seg 1)) . 1).] by FINSEQ_1:def 15

            .= [.( lower_bound A), (D1 . 1).] by A22, FUNCT_1: 47;

            hence thesis by A27, A26, A25;

          end;

          

           A28: (g | ( divset (D1,1))) is bounded_below

          proof

            consider a be Real such that

             A29: for x be object st x in (A /\ ( dom f)) holds a <= (f . x) by A2, RFUNCT_1: 71;

            for x be object st x in (( divset (D1,1)) /\ ( dom g)) holds a <= (g . x)

            proof

              let x be object;

              

               A30: ( dom g) c= ( dom f) by RELAT_1: 60;

              assume x in (( divset (D1,1)) /\ ( dom g));

              then

               A31: x in ( dom g) by XBOOLE_0:def 4;

              

               A32: (A /\ ( dom f)) = ( dom f) by XBOOLE_1: 28;

              then

              reconsider x as Element of A by A31, A30, XBOOLE_0:def 4;

              a <= (f . x) by A29, A31, A32, A30;

              hence thesis by A31, FUNCT_1: 47;

            end;

            hence thesis by RFUNCT_1: 71;

          end;

          

           A33: ( rng D2) c= A by Def1;

          

           A34: ( indx (D2,D1,1)) in ( dom D2) by A1, A5, Def18;

          then

           A35: ( indx (D2,D1,1)) in ( Seg ( len D2)) by FINSEQ_1:def 3;

          then

           A36: 1 <= ( indx (D2,D1,1)) by FINSEQ_1: 1;

          

           A37: ( indx (D2,D1,1)) <= ( len D2) by A35, FINSEQ_1: 1;

          then 1 <= ( len D2) by A36, XXREAL_0: 2;

          then 1 in ( Seg ( len D2)) by FINSEQ_1: 1;

          then

           A38: 1 in ( dom D2) by FINSEQ_1:def 3;

          then (D2 . 1) in ( rng D2) by FUNCT_1:def 3;

          then (D2 . 1) in A by A33;

          then (D2 . 1) in [.( lower_bound A), ( upper_bound A).] by Th2;

          then (D2 . 1) in { a : ( lower_bound A) <= a & a <= ( upper_bound A) } by RCOMP_1:def 1;

          then ex a st (D2 . 1) = a & ( lower_bound A) <= a & a <= ( upper_bound A);

          then (D2 . 1) >= ( lower_bound B) by A5, Def3;

          then

          reconsider DD2 as Division of B by A34, A36, A38, A7, Th35;

          ( indx (D2,D1,1)) in ( dom D2) by A1, A5, Def18;

          then

           A39: ( indx (D2,D1,1)) in ( Seg ( len D2)) by FINSEQ_1:def 3;

          then

           A40: 1 <= ( indx (D2,D1,1)) by FINSEQ_1: 1;

          

           A41: ( indx (D2,D1,1)) <= ( len D2) by A39, FINSEQ_1: 1;

          then

           A42: 1 <= ( len D2) by A40, XXREAL_0: 2;

          then ( len ( mid (D2,1,( indx (D2,D1,1))))) = ((( indx (D2,D1,1)) -' 1) + 1) by A40, A41, FINSEQ_6: 118;

          then

           A43: ( len ( mid (D2,1,( indx (D2,D1,1))))) = ((( indx (D2,D1,1)) - 1) + 1) by A40, XREAL_1: 233;

          then

           A44: ( len ( mid (D2,1,( indx (D2,D1,1))))) = ( len (D2 | ( indx (D2,D1,1)))) by A41, FINSEQ_1: 59;

          

           A45: for k be Nat st 1 <= k & k <= ( len ( mid (D2,1,( indx (D2,D1,1))))) holds (( mid (D2,1,( indx (D2,D1,1)))) . k) = ((D2 | ( indx (D2,D1,1))) . k)

          proof

            let k be Nat;

            assume that

             A46: 1 <= k and

             A47: k <= ( len ( mid (D2,1,( indx (D2,D1,1)))));

            k in ( Seg ( len (D2 | ( indx (D2,D1,1))))) by A44, A46, A47, FINSEQ_1: 1;

            then k in ( dom (D2 | ( indx (D2,D1,1)))) by FINSEQ_1:def 3;

            then k in ( dom (D2 | ( Seg ( indx (D2,D1,1))))) by FINSEQ_1:def 15;

            then

             A48: ((D2 | ( Seg ( indx (D2,D1,1)))) . k) = (D2 . k) by FUNCT_1: 47;

            (( mid (D2,1,( indx (D2,D1,1)))) . k) = (D2 . ((k + 1) -' 1)) by A40, A41, A42, A46, A47, FINSEQ_6: 118;

            then (( mid (D2,1,( indx (D2,D1,1)))) . k) = (D2 . ((k + 1) - 1)) by NAT_1: 11, XREAL_1: 233;

            hence thesis by A48, FINSEQ_1:def 15;

          end;

          then

           A49: ( mid (D2,1,( indx (D2,D1,1)))) = (D2 | ( indx (D2,D1,1))) by A44, FINSEQ_1: 14;

          

           A50: for i be Nat st 1 <= i & i <= ( len ( lower_volume (g,DD2))) holds (( lower_volume (g,DD2)) . i) = ((( lower_volume (f,D2)) | ( indx (D2,D1,1))) . i)

          proof

            let i be Nat;

            assume that

             A51: 1 <= i and

             A52: i <= ( len ( lower_volume (g,DD2)));

            

             A53: i <= ( len DD2) by A52, Def6;

            then

             A54: i in ( Seg ( len DD2)) by A51, FINSEQ_1: 1;

            then

             A55: i in ( dom DD2) by FINSEQ_1:def 3;

            ( divset (DD2,i)) = ( divset (D2,i))

            proof

              ( Seg ( indx (D2,D1,1))) c= ( Seg ( len D2)) by A41, FINSEQ_1: 5;

              then i in ( Seg ( len D2)) by A43, A54;

              then

               A56: i in ( dom D2) by FINSEQ_1:def 3;

              now

                per cases ;

                  suppose

                   A57: i = 1;

                  then

                   A58: 1 in ( dom (D2 | ( Seg ( indx (D2,D1,1))))) by A49, A55, FINSEQ_1:def 15;

                  then 1 in (( dom D2) /\ ( Seg ( indx (D2,D1,1)))) by RELAT_1: 61;

                  then

                   A59: 1 in ( dom D2) by XBOOLE_0:def 4;

                  

                   A60: ( divset (D2,i)) = [.( lower_bound ( divset (D2,1))), ( upper_bound ( divset (D2,1))).] by A57, Th2

                  .= [.( lower_bound A), ( upper_bound ( divset (D2,1))).] by A59, Def3

                  .= [.( lower_bound A), (D2 . 1).] by A59, Def3;

                  ( divset (DD2,i)) = [.( lower_bound ( divset (DD2,1))), ( upper_bound ( divset (DD2,1))).] by A57, Th2

                  .= [.( lower_bound B), ( upper_bound ( divset (DD2,1))).] by A55, A57, Def3

                  .= [.( lower_bound B), (DD2 . 1).] by A55, A57, Def3

                  .= [.( lower_bound B), ((D2 | ( indx (D2,D1,1))) . 1).] by A45, A53, A57

                  .= [.( lower_bound B), ((D2 | ( Seg ( indx (D2,D1,1)))) . 1).] by FINSEQ_1:def 15

                  .= [.( lower_bound B), (D2 . 1).] by A58, FUNCT_1: 47

                  .= [.( lower_bound A), (D2 . 1).] by A5, Def3;

                  hence thesis by A60;

                end;

                  suppose

                   A61: i <> 1;

                  

                   A62: (i - 1) in ( dom (D2 | ( Seg ( indx (D2,D1,1)))))

                  proof

                    i is non trivial by A51, A61, NAT_2:def 1;

                    then

                     A63: i >= (1 + 1) by NAT_2: 29;

                    then

                     A64: 1 <= (i - 1) by XREAL_1: 19;

                    

                     A65: ex j be Nat st i = (1 + j) by A51, NAT_1: 10;

                    

                     A66: (i - 1) <= (( indx (D2,D1,1)) - 0 ) by A43, A53, XREAL_1: 13;

                    then (i - 1) <= ( len D2) by A37, XXREAL_0: 2;

                    then (i - 1) in ( Seg ( len D2)) by A65, A64, FINSEQ_1: 1;

                    then

                     A67: (i - 1) in ( dom D2) by FINSEQ_1:def 3;

                    (i - 1) >= 1 by A63, XREAL_1: 19;

                    then (i - 1) in ( Seg ( indx (D2,D1,1))) by A65, A66, FINSEQ_1: 1;

                    then (i - 1) in (( dom D2) /\ ( Seg ( indx (D2,D1,1)))) by A67, XBOOLE_0:def 4;

                    hence thesis by RELAT_1: 61;

                  end;

                  (DD2 . (i - 1)) = ((D2 | ( indx (D2,D1,1))) . (i - 1)) by A44, A45, FINSEQ_1: 14

                  .= ((D2 | ( Seg ( indx (D2,D1,1)))) . (i - 1)) by FINSEQ_1:def 15;

                  then

                   A68: (DD2 . (i - 1)) = (D2 . (i - 1)) by A62, FUNCT_1: 47;

                  i <= ( len D2) by A43, A37, A53, XXREAL_0: 2;

                  then i in ( Seg ( len D2)) by A51, FINSEQ_1: 1;

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

                  then i in (( dom D2) /\ ( Seg ( indx (D2,D1,1)))) by A43, A54, XBOOLE_0:def 4;

                  then

                   A69: i in ( dom (D2 | ( Seg ( indx (D2,D1,1))))) by RELAT_1: 61;

                  (DD2 . i) = ((D2 | ( indx (D2,D1,1))) . i) by A44, A45, FINSEQ_1: 14

                  .= ((D2 | ( Seg ( indx (D2,D1,1)))) . i) by FINSEQ_1:def 15;

                  then

                   A70: (DD2 . i) = (D2 . i) by A69, FUNCT_1: 47;

                  

                   A71: ( divset (D2,i)) = [.( lower_bound ( divset (D2,i))), ( upper_bound ( divset (D2,i))).] by Th2

                  .= [.(D2 . (i - 1)), ( upper_bound ( divset (D2,i))).] by A56, A61, Def3

                  .= [.(D2 . (i - 1)), (D2 . i).] by A56, A61, Def3;

                  ( divset (DD2,i)) = [.( lower_bound ( divset (DD2,i))), ( upper_bound ( divset (DD2,i))).] by Th2

                  .= [.(DD2 . (i - 1)), ( upper_bound ( divset (DD2,i))).] by A55, A61, Def3

                  .= [.(D2 . (i - 1)), (D2 . i).] by A55, A61, A68, A70, Def3;

                  hence thesis by A71;

                end;

              end;

              hence thesis;

            end;

            then

             A72: (( lower_volume (g,DD2)) . i) = (( lower_bound ( rng (g | ( divset (D2,i))))) * ( vol ( divset (D2,i)))) by A55, Def6;

            ( Seg ( indx (D2,D1,1))) c= ( Seg ( len D2)) by A41, FINSEQ_1: 5;

            then i in ( Seg ( len D2)) by A43, A54;

            then

             A73: i in ( dom D2) by FINSEQ_1:def 3;

            

             A74: i in ( dom DD2) by A54, FINSEQ_1:def 3;

             A75:

            now

              per cases ;

                suppose

                 A76: i = 1;

                then 1 in ( dom (D2 | ( Seg ( indx (D2,D1,1))))) by A49, A74, FINSEQ_1:def 15;

                then 1 in (( dom D2) /\ ( Seg ( indx (D2,D1,1)))) by RELAT_1: 61;

                then

                 A77: 1 in ( dom D2) by XBOOLE_0:def 4;

                then (D2 . 1) <= (D2 . ( indx (D2,D1,1))) by A34, A36, SEQ_4: 137;

                then

                 A78: (D2 . 1) <= (D1 . 1) by A1, A5, Def18;

                ( lower_bound ( divset (D2,i))) = ( lower_bound A) by A76, A77, Def3;

                then

                 A79: ( lower_bound ( divset (D2,i))) = ( lower_bound ( divset (D1,1))) by A5, Def3;

                ( upper_bound ( divset (D2,i))) = (D2 . 1) by A76, A77, Def3;

                then

                 A80: ( upper_bound ( divset (D2,i))) <= ( upper_bound ( divset (D1,1))) by A5, A78, Def3;

                ( lower_bound ( divset (D1,1))) <= ( upper_bound ( divset (D1,1))) by SEQ_4: 11;

                hence ( lower_bound ( divset (D2,i))) in [.( lower_bound ( divset (D1,1))), ( upper_bound ( divset (D1,1))).] by A79, XXREAL_1: 1;

                ( lower_bound ( divset (D2,i))) <= ( upper_bound ( divset (D2,i))) by SEQ_4: 11;

                then ( upper_bound ( divset (D2,i))) in { r : ( lower_bound ( divset (D1,1))) <= r & r <= ( upper_bound ( divset (D1,1))) } by A79, A80;

                hence ( upper_bound ( divset (D2,i))) in [.( lower_bound ( divset (D1,1))), ( upper_bound ( divset (D1,1))).] by RCOMP_1:def 1;

              end;

                suppose

                 A81: i <> 1;

                then i is non trivial by A51, NAT_2:def 1;

                then i >= (1 + 1) by NAT_2: 29;

                then

                 A82: 1 <= (i - 1) by XREAL_1: 19;

                

                 A83: ex j be Nat st i = (1 + j) by A51, NAT_1: 10;

                

                 A84: ( rng D2) c= A by Def1;

                

                 A85: ( lower_bound ( divset (D2,i))) = (D2 . (i - 1)) by A73, A81, Def3;

                

                 A86: ( lower_bound ( divset (D1,1))) = ( lower_bound A) by A5, Def3;

                

                 A87: (i - 1) <= (( indx (D2,D1,1)) - 0 ) by A43, A53, XREAL_1: 13;

                then (i - 1) <= ( len D2) by A37, XXREAL_0: 2;

                then (i - 1) in ( Seg ( len D2)) by A83, A82, FINSEQ_1: 1;

                then

                 A88: (i - 1) in ( dom D2) by FINSEQ_1:def 3;

                then (D2 . (i - 1)) in ( rng D2) by FUNCT_1:def 3;

                then

                 A89: ( lower_bound ( divset (D2,i))) >= ( lower_bound ( divset (D1,1))) by A85, A86, A84, SEQ_4:def 2;

                

                 A90: ( upper_bound ( divset (D1,1))) = (D1 . 1) by A5, Def3;

                (D2 . (i - 1)) <= (D2 . ( indx (D2,D1,1))) by A34, A87, A88, SEQ_4: 137;

                then ( lower_bound ( divset (D2,i))) <= ( upper_bound ( divset (D1,1))) by A1, A5, A85, A90, Def18;

                then ( lower_bound ( divset (D2,i))) in { r : ( lower_bound ( divset (D1,1))) <= r & r <= ( upper_bound ( divset (D1,1))) } by A89;

                hence ( lower_bound ( divset (D2,i))) in [.( lower_bound ( divset (D1,1))), ( upper_bound ( divset (D1,1))).] by RCOMP_1:def 1;

                

                 A91: ( upper_bound ( divset (D2,i))) = (D2 . i) by A73, A81, Def3;

                (D2 . i) in ( rng D2) by A73, FUNCT_1:def 3;

                then

                 A92: ( upper_bound ( divset (D2,i))) >= ( lower_bound ( divset (D1,1))) by A91, A86, A84, SEQ_4:def 2;

                (D2 . i) <= (D2 . ( indx (D2,D1,1))) by A43, A34, A53, A73, SEQ_4: 137;

                then ( upper_bound ( divset (D2,i))) <= ( upper_bound ( divset (D1,1))) by A1, A5, A91, A90, Def18;

                then ( upper_bound ( divset (D2,i))) in { r : ( lower_bound ( divset (D1,1))) <= r & r <= ( upper_bound ( divset (D1,1))) } by A92;

                hence ( upper_bound ( divset (D2,i))) in [.( lower_bound ( divset (D1,1))), ( upper_bound ( divset (D1,1))).] by RCOMP_1:def 1;

              end;

            end;

            

             A93: ( divset (D1,1)) = [.( lower_bound ( divset (D1,1))), ( upper_bound ( divset (D1,1))).] by Th2;

            

             A94: ( Seg ( indx (D2,D1,1))) c= ( Seg ( len D2)) by A41, FINSEQ_1: 5;

            then i in ( Seg ( len D2)) by A43, A54;

            then

             A95: i in ( dom D2) by FINSEQ_1:def 3;

            ( divset (D2,i)) = [.( lower_bound ( divset (D2,i))), ( upper_bound ( divset (D2,i))).] by Th2;

            then

             A96: ( divset (D2,i)) c= ( divset (D1,1)) by A93, A75, XXREAL_2:def 12;

            

             A97: ( dom (( lower_volume (f,D2)) | ( Seg ( indx (D2,D1,1))))) = (( dom ( lower_volume (f,D2))) /\ ( Seg ( indx (D2,D1,1)))) by RELAT_1: 61

            .= (( Seg ( len ( lower_volume (f,D2)))) /\ ( Seg ( indx (D2,D1,1)))) by FINSEQ_1:def 3

            .= (( Seg ( len D2)) /\ ( Seg ( indx (D2,D1,1)))) by Def6

            .= ( Seg ( indx (D2,D1,1))) by A94, XBOOLE_1: 28;

            ((( lower_volume (f,D2)) | ( indx (D2,D1,1))) . i) = ((( lower_volume (f,D2)) | ( Seg ( indx (D2,D1,1)))) . i) by FINSEQ_1:def 15

            .= (( lower_volume (f,D2)) . i) by A43, A54, A97, FUNCT_1: 47

            .= (( lower_bound ( rng (f | ( divset (D2,i))))) * ( vol ( divset (D2,i)))) by A95, Def6;

            hence thesis by A72, A96, FUNCT_1: 51;

          end;

          ( len ( lower_volume (g,DD1))) = ( len (( lower_volume (f,D1)) | 1)) by A10;

          then

           A98: ( lower_volume (g,DD1)) = (( lower_volume (f,D1)) | 1) by A18, FINSEQ_1: 14;

          

           A99: ( indx (D2,D1,1)) <= ( len ( lower_volume (f,D2))) by A41, Def6;

          ( len ( lower_volume (g,DD2))) = ( indx (D2,D1,1)) by A43, Def6;

          then

           A100: ( len ( lower_volume (g,DD2))) = ( len (( lower_volume (f,D2)) | ( indx (D2,D1,1)))) by A99, FINSEQ_1: 59;

          ( dom g) = (A /\ ( divset (D1,1))) by A4, FUNCT_2:def 1;

          then ( dom g) = ( divset (D1,1)) by A5, Th6, XBOOLE_1: 28;

          then g is total by PARTFUN1:def 2;

          then ( lower_sum (g,DD1)) <= ( lower_sum (g,DD2)) by A11, A28, Th29;

          hence thesis by A98, A100, A50, FINSEQ_1: 14;

        end;

        

         A101: for k be non zero Nat st P[k] holds P[(k + 1)]

        proof

          let k be non zero Nat;

          assume

           A102: k in ( dom D1) implies ( Sum (( lower_volume (f,D1)) | k)) <= ( Sum (( lower_volume (f,D2)) | ( indx (D2,D1,k))));

          assume

           A103: (k + 1) in ( dom D1);

          then

           A104: (k + 1) in ( Seg ( len D1)) by FINSEQ_1:def 3;

          then

           A105: 1 <= (k + 1) by FINSEQ_1: 1;

          

           A106: (k + 1) <= ( len D1) by A104, FINSEQ_1: 1;

          now

            per cases ;

              suppose 1 = (k + 1);

              hence thesis by A3, A103;

            end;

              suppose

               A107: 1 <> (k + 1);

              set IDK = ( indx (D2,D1,k));

              set IDK1 = ( indx (D2,D1,(k + 1)));

              set K1D2 = (( lower_volume (f,D2)) | ( indx (D2,D1,(k + 1))));

              set KD1 = (( lower_volume (f,D1)) | k);

              set K1D1 = (( lower_volume (f,D1)) | (k + 1));

              set n = (k + 1);

              

               A108: (k + 1) <= ( len ( lower_volume (f,D1))) by A106, Def6;

              then

               A109: ( len K1D1) = (k + 1) by FINSEQ_1: 59;

              then

              consider p1,q1 be FinSequence of REAL such that

               A110: ( len p1) = k and

               A111: ( len q1) = 1 and

               A112: K1D1 = (p1 ^ q1) by FINSEQ_2: 23;

              

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

              then

               A114: k <= ( len D1) by A106, XXREAL_0: 2;

              then

               A115: k <= ( len ( lower_volume (f,D1))) by Def6;

              then

               A116: ( len p1) = ( len KD1) by A110, FINSEQ_1: 59;

              for i be Nat st 1 <= i & i <= ( len p1) holds (p1 . i) = (KD1 . i)

              proof

                let i be Nat;

                assume that

                 A117: 1 <= i and

                 A118: i <= ( len p1);

                

                 A119: i in ( Seg ( len p1)) by A117, A118, FINSEQ_1: 1;

                then

                 A120: i in ( dom KD1) by A116, FINSEQ_1:def 3;

                then

                 A121: i in ( dom (( lower_volume (f,D1)) | ( Seg k))) by FINSEQ_1:def 15;

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

                then

                 A122: ( Seg k) c= ( Seg (k + 1)) by FINSEQ_1: 5;

                

                 A123: ( dom K1D1) = ( Seg ( len K1D1)) by FINSEQ_1:def 3

                .= ( Seg (k + 1)) by A108, FINSEQ_1: 59;

                ( dom KD1) = ( Seg ( len KD1)) by FINSEQ_1:def 3

                .= ( Seg k) by A115, FINSEQ_1: 59;

                then i in ( dom K1D1) by A120, A122, A123;

                then

                 A124: i in ( dom (( lower_volume (f,D1)) | ( Seg (k + 1)))) by FINSEQ_1:def 15;

                

                 A125: (K1D1 . i) = ((( lower_volume (f,D1)) | ( Seg (k + 1))) . i) by FINSEQ_1:def 15

                .= (( lower_volume (f,D1)) . i) by A124, FUNCT_1: 47;

                

                 A126: (KD1 . i) = ((( lower_volume (f,D1)) | ( Seg k)) . i) by FINSEQ_1:def 15

                .= (( lower_volume (f,D1)) . i) by A121, FUNCT_1: 47;

                i in ( dom p1) by A119, FINSEQ_1:def 3;

                hence thesis by A112, A126, A125, FINSEQ_1:def 7;

              end;

              then

               A127: p1 = KD1 by A116, FINSEQ_1: 14;

              

               A128: ( indx (D2,D1,(k + 1))) in ( dom D2) by A1, A103, Def18;

              then

               A129: ( indx (D2,D1,(k + 1))) in ( Seg ( len D2)) by FINSEQ_1:def 3;

              then

               A130: 1 <= ( indx (D2,D1,(k + 1))) by FINSEQ_1: 1;

              n is non trivial by A107, NAT_2:def 1;

              then n >= 2 by NAT_2: 29;

              then k >= ((1 + 1) - 1) by XREAL_1: 20;

              then

               A131: k in ( Seg ( len D1)) by A114, FINSEQ_1: 1;

              then

               A132: k in ( dom D1) by FINSEQ_1:def 3;

              then

               A133: ( indx (D2,D1,k)) in ( dom D2) by A1, Def18;

              

               A134: ( indx (D2,D1,k)) < ( indx (D2,D1,(k + 1)))

              proof

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

                then

                 A135: (D1 . k) < (D1 . (k + 1)) by A103, A132, SEQM_3:def 1;

                assume ( indx (D2,D1,k)) >= ( indx (D2,D1,(k + 1)));

                then

                 A136: (D2 . ( indx (D2,D1,k))) >= (D2 . ( indx (D2,D1,(k + 1)))) by A133, A128, SEQ_4: 137;

                (D1 . k) = (D2 . ( indx (D2,D1,k))) by A1, A132, Def18;

                hence contradiction by A1, A103, A136, A135, Def18;

              end;

              

               A137: ( indx (D2,D1,(k + 1))) >= ( indx (D2,D1,k))

              proof

                assume ( indx (D2,D1,(k + 1))) < ( indx (D2,D1,k));

                then

                 A138: (D2 . ( indx (D2,D1,(k + 1)))) < (D2 . ( indx (D2,D1,k))) by A133, A128, SEQM_3:def 1;

                (D1 . (k + 1)) = (D2 . ( indx (D2,D1,(k + 1)))) by A1, A103, Def18;

                then (D1 . (k + 1)) < (D1 . k) by A1, A132, A138, Def18;

                hence contradiction by A103, A132, NAT_1: 11, SEQ_4: 137;

              end;

              then

              consider ID be Nat such that

               A139: ( indx (D2,D1,(k + 1))) = (( indx (D2,D1,k)) + ID) by NAT_1: 10;

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

              

               A140: ( len ( lower_volume (f,D2))) = ( len D2) by Def6;

              then

               A141: ( indx (D2,D1,(k + 1))) <= ( len ( lower_volume (f,D2))) by A129, FINSEQ_1: 1;

              then ( len K1D2) = (IDK + (IDK1 - IDK)) by FINSEQ_1: 59;

              then

              consider p2,q2 be FinSequence of REAL such that

               A142: ( len p2) = IDK and

               A143: ( len q2) = (IDK1 - IDK) and

               A144: K1D2 = (p2 ^ q2) by A139, FINSEQ_2: 23;

              

               A145: ( indx (D2,D1,(k + 1))) <= ( len D2) by A129, FINSEQ_1: 1;

              ( indx (D2,D1,k)) in ( dom D2) by A1, A132, Def18;

              then

               A146: ( indx (D2,D1,k)) in ( Seg ( len D2)) by FINSEQ_1:def 3;

              then

               A147: 1 <= ( indx (D2,D1,k)) by FINSEQ_1: 1;

              

               A148: ( Sum q1) <= ( Sum q2)

              proof

                set MD2 = ( mid (D2,(( indx (D2,D1,k)) + 1),( indx (D2,D1,(k + 1)))));

                set MD1 = ( mid (D1,(k + 1),(k + 1)));

                set DD1 = ( divset (D1,(k + 1)));

                set g = (f | DD1);

                

                 A149: 1 <= (( indx (D2,D1,k)) + 1) by NAT_1: 11;

                reconsider g as PartFunc of DD1, REAL by PARTFUN1: 10;

                ((k + 1) - 1) = k;

                then

                 A150: ( lower_bound DD1) = (D1 . k) by A103, A107, Def3;

                ( dom g) = (( dom f) /\ ( divset (D1,(k + 1)))) by RELAT_1: 61;

                then ( dom g) = (A /\ ( divset (D1,(k + 1)))) by FUNCT_2:def 1;

                then ( dom g) = ( divset (D1,(k + 1))) by A103, Th6, XBOOLE_1: 28;

                then

                 A151: g is total by PARTFUN1:def 2;

                

                 A152: ( upper_bound ( divset (D1,(k + 1)))) = (D1 . (k + 1)) by A103, A107, Def3;

                

                 A153: (D2 . ( indx (D2,D1,(k + 1)))) = (D1 . (k + 1)) by A1, A103, Def18;

                

                 A154: (( indx (D2,D1,k)) + 1) <= ( indx (D2,D1,(k + 1))) by A134, NAT_1: 13;

                then

                 A155: (( indx (D2,D1,k)) + 1) <= ( len D2) by A145, XXREAL_0: 2;

                then (( indx (D2,D1,k)) + 1) in ( Seg ( len D2)) by A149, FINSEQ_1: 1;

                then

                 A156: (( indx (D2,D1,k)) + 1) in ( dom D2) by FINSEQ_1:def 3;

                then (D2 . (( indx (D2,D1,k)) + 1)) >= (D2 . ( indx (D2,D1,k))) by A133, NAT_1: 11, SEQ_4: 137;

                then (D2 . (( indx (D2,D1,k)) + 1)) >= ( lower_bound DD1) by A1, A132, A150, Def18;

                then

                reconsider MD2 as Division of DD1 by A128, A154, A156, A153, A152, Th35;

                

                 A157: ((( indx (D2,D1,(k + 1))) -' (( indx (D2,D1,k)) + 1)) + 1) = ((( indx (D2,D1,(k + 1))) - (( indx (D2,D1,k)) + 1)) + 1) by A154, XREAL_1: 233

                .= (( indx (D2,D1,(k + 1))) - ( indx (D2,D1,k)));

                

                 A158: for n be Nat st 1 <= n & n <= ( len q2) holds (q2 . n) = (( lower_volume (g,MD2)) . n)

                proof

                  let n be Nat;

                  assume that

                   A159: 1 <= n and

                   A160: n <= ( len q2);

                  n in ( Seg ( len q2)) by A159, A160, FINSEQ_1: 1;

                  then

                   A161: n in ( dom q2) by FINSEQ_1:def 3;

                  then

                   A162: (( indx (D2,D1,k)) + n) in ( dom K1D2) by A142, A144, FINSEQ_1: 28;

                  then

                   A163: (( indx (D2,D1,k)) + n) in ( dom (( lower_volume (f,D2)) | ( Seg ( indx (D2,D1,(k + 1)))))) by FINSEQ_1:def 15;

                  

                   A164: ( len ( mid (D2,(( indx (D2,D1,k)) + 1),( indx (D2,D1,(k + 1)))))) = ID by A130, A145, A139, A154, A155, A149, A157, FINSEQ_6: 118;

                  

                   A165: ( dom K1D2) = ( Seg ( len K1D2)) by FINSEQ_1:def 3

                  .= ( Seg ( indx (D2,D1,(k + 1)))) by A141, FINSEQ_1: 59;

                  then (( indx (D2,D1,k)) + n) <= ( indx (D2,D1,(k + 1))) by A162, FINSEQ_1: 1;

                  then

                   A166: n <= (( indx (D2,D1,(k + 1))) - ( indx (D2,D1,k))) by XREAL_1: 19;

                  then n in ( Seg ( len ( mid (D2,(( indx (D2,D1,k)) + 1),( indx (D2,D1,(k + 1))))))) by A139, A159, A164, FINSEQ_1: 1;

                  then

                   A167: n in ( dom MD2) by FINSEQ_1:def 3;

                  

                   A168: ( Seg ( indx (D2,D1,(k + 1)))) c= ( Seg ( len D2)) by A145, FINSEQ_1: 5;

                  then (( indx (D2,D1,k)) + n) in ( Seg ( len D2)) by A165, A162;

                  then

                   A169: (( indx (D2,D1,k)) + n) in ( dom D2) by FINSEQ_1:def 3;

                  

                   A170: (q2 . n) = (K1D2 . (( indx (D2,D1,k)) + n)) by A142, A144, A161, FINSEQ_1:def 7

                  .= ((( lower_volume (f,D2)) | ( Seg ( indx (D2,D1,(k + 1))))) . (( indx (D2,D1,k)) + n)) by FINSEQ_1:def 15

                  .= (( lower_volume (f,D2)) . (( indx (D2,D1,k)) + n)) by A163, FUNCT_1: 47

                  .= (( lower_bound ( rng (f | ( divset (D2,(( indx (D2,D1,k)) + n)))))) * ( vol ( divset (D2,(( indx (D2,D1,k)) + n))))) by A169, Def6;

                  

                   A171: 1 <= (( indx (D2,D1,k)) + n) by A165, A162, FINSEQ_1: 1;

                  

                   A172: ( divset (MD2,n)) = ( divset (D2,(( indx (D2,D1,k)) + n))) & ( divset (D2,(( indx (D2,D1,k)) + n))) c= ( divset (D1,(k + 1)))

                  proof

                    now

                      per cases ;

                        suppose

                         A173: n = 1;

                        then

                         A174: 1 <= (( indx (D2,D1,k)) + 1) by A165, A162, FINSEQ_1: 1;

                        

                         A175: (( indx (D2,D1,k)) + 1) <= ( len D2) by A165, A162, A168, A173, FINSEQ_1: 1;

                        

                         A176: ( upper_bound ( divset (MD2,1))) = (( mid (D2,(( indx (D2,D1,k)) + 1),( indx (D2,D1,(k + 1))))) . 1) by A167, A173, Def3

                        .= (D2 . (1 + ( indx (D2,D1,k)))) by A130, A145, A174, A175, FINSEQ_6: 118;

                        

                         A177: (( indx (D2,D1,k)) + 1) <> 1 by A147, NAT_1: 13;

                        

                         A178: ((k + 1) - 1) = k;

                        

                         A179: ( lower_bound ( divset (MD2,1))) = ( lower_bound ( divset (D1,(k + 1)))) by A167, A173, Def3

                        .= (D1 . k) by A103, A107, A178, Def3;

                        

                         A180: ( divset (D2,(( indx (D2,D1,k)) + n))) = [.( lower_bound ( divset (D2,(( indx (D2,D1,k)) + 1)))), ( upper_bound ( divset (D2,(( indx (D2,D1,k)) + 1)))).] by A173, Th2

                        .= [.(D2 . ((( indx (D2,D1,k)) + 1) - 1)), ( upper_bound ( divset (D2,(( indx (D2,D1,k)) + 1)))).] by A156, A177, Def3

                        .= [.(D2 . ( indx (D2,D1,k))), (D2 . (( indx (D2,D1,k)) + 1)).] by A156, A177, Def3

                        .= [.(D1 . k), (D2 . (( indx (D2,D1,k)) + 1)).] by A1, A132, Def18;

                        hence ( divset (MD2,n)) = ( divset (D2,(( indx (D2,D1,k)) + n))) by A173, A179, A176, Th2;

                        ( divset (MD2,n)) = [.(D1 . k), (D2 . (( indx (D2,D1,k)) + 1)).] by A173, A179, A176, Th2;

                        hence thesis by A167, A180, Th6;

                      end;

                        suppose

                         A181: n <> 1;

                        

                         A182: (( indx (D2,D1,k)) + n) <> 1

                        proof

                          assume (( indx (D2,D1,k)) + n) = 1;

                          then ( indx (D2,D1,k)) = (1 - n);

                          then (n + 1) <= 1 by A147, XREAL_1: 19;

                          then n <= (1 - 1) by XREAL_1: 19;

                          hence contradiction by A159, NAT_1: 3;

                        end;

                        

                         A183: ( divset (D2,(( indx (D2,D1,k)) + n))) = [.( lower_bound ( divset (D2,(( indx (D2,D1,k)) + n)))), ( upper_bound ( divset (D2,(( indx (D2,D1,k)) + n)))).] by Th2

                        .= [.(D2 . ((( indx (D2,D1,k)) + n) - 1)), ( upper_bound ( divset (D2,(( indx (D2,D1,k)) + n)))).] by A169, A182, Def3

                        .= [.(D2 . ((( indx (D2,D1,k)) + n) - 1)), (D2 . (( indx (D2,D1,k)) + n)).] by A169, A182, Def3;

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

                        then (n - 1) <= n by XREAL_1: 20;

                        then

                         A184: (n - 1) <= ( len MD2) by A139, A166, A164, XXREAL_0: 2;

                        

                         A185: (( indx (D2,D1,k)) + 1) <= ( indx (D2,D1,(k + 1))) by A134, NAT_1: 13;

                        n is non trivial by A159, A181, NAT_2:def 1;

                        then n >= (1 + 1) by NAT_2: 29;

                        then

                         A186: 1 <= (n - 1) by XREAL_1: 19;

                        consider n1 be Nat such that

                         A187: n = (1 + n1) by A159, NAT_1: 10;

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

                        

                         A188: ((n1 + (( indx (D2,D1,k)) + 1)) -' 1) = ((( indx (D2,D1,k)) + n) - 1) by A171, A187, XREAL_1: 233;

                        

                         A189: ((n + (( indx (D2,D1,k)) + 1)) -' 1) = (((n + ( indx (D2,D1,k))) + 1) - 1) by NAT_1: 11, XREAL_1: 233

                        .= (( indx (D2,D1,k)) + n);

                        

                         A190: ( lower_bound ( divset (MD2,n))) = (MD2 . (n - 1)) by A167, A181, Def3

                        .= (D2 . ((( indx (D2,D1,k)) + n) - 1)) by A130, A145, A155, A149, A185, A187, A188, A186, A184, FINSEQ_6: 118;

                        

                         A191: ( upper_bound ( divset (MD2,n))) = (MD2 . n) by A167, A181, Def3

                        .= (D2 . (( indx (D2,D1,k)) + n)) by A130, A145, A139, A155, A149, A159, A166, A164, A185, A189, FINSEQ_6: 118;

                        hence ( divset (MD2,n)) = ( divset (D2,(( indx (D2,D1,k)) + n))) by A190, A183, Th2;

                        ( divset (MD2,n)) = [.(D2 . ((( indx (D2,D1,k)) + n) - 1)), (D2 . (( indx (D2,D1,k)) + n)).] by A190, A191, Th2;

                        hence thesis by A167, A183, Th6;

                      end;

                    end;

                    hence thesis;

                  end;

                  then (g | ( divset (MD2,n))) = (f | ( divset (D2,(( indx (D2,D1,k)) + n)))) by FUNCT_1: 51;

                  hence thesis by A167, A170, A172, Def6;

                end;

                ((k + 1) - 1) = k;

                then

                 A192: ( lower_bound DD1) = (D1 . k) by A103, A107, Def3;

                (D1 . (k + 1)) = ( upper_bound DD1) by A103, A107, Def3;

                then

                reconsider MD1 as Division of DD1 by A103, A113, A132, A192, Th35, SEQ_4: 137;

                

                 A193: (g | ( divset (D1,(k + 1)))) is bounded_below

                proof

                  consider a be Real such that

                   A194: for x be object st x in (A /\ ( dom f)) holds a <= (f . x) by A2, RFUNCT_1: 71;

                  for x be object st x in (( divset (D1,(k + 1))) /\ ( dom g)) holds a <= (g . x)

                  proof

                    let x be object;

                    

                     A195: ( dom g) c= ( dom f) by RELAT_1: 60;

                    assume x in (( divset (D1,(k + 1))) /\ ( dom g));

                    then

                     A196: x in ( dom g) by XBOOLE_0:def 4;

                    

                     A197: (A /\ ( dom f)) = ( dom f) by XBOOLE_1: 28;

                    then

                    reconsider x as Element of A by A196, A195, XBOOLE_0:def 4;

                    a <= (f . x) by A194, A196, A197, A195;

                    hence thesis by A196, FUNCT_1: 47;

                  end;

                  hence thesis by RFUNCT_1: 71;

                end;

                ( len MD1) = (((k + 1) -' (k + 1)) + 1) by A105, A106, FINSEQ_6: 118;

                then

                 A198: ( len MD1) = (((k + 1) - (k + 1)) + 1) by XREAL_1: 233;

                

                 A199: for n be Nat st 1 <= n & n <= ( len q1) holds (q1 . n) = (( lower_volume (g,MD1)) . n)

                proof

                  (k + 1) in ( Seg ( len K1D1)) by A109, FINSEQ_1: 4;

                  then (k + 1) in ( dom K1D1) by FINSEQ_1:def 3;

                  then

                   A200: (k + 1) in ( dom (( lower_volume (f,D1)) | ( Seg (k + 1)))) by FINSEQ_1:def 15;

                  

                   A201: (K1D1 . (k + 1)) = ((( lower_volume (f,D1)) | ( Seg (k + 1))) . (k + 1)) by FINSEQ_1:def 15

                  .= (( lower_volume (f,D1)) . (k + 1)) by A200, FUNCT_1: 47;

                  

                   A202: (MD1 . 1) = (D1 . (k + 1)) by A105, A106, FINSEQ_6: 118;

                  1 in ( Seg 1) by FINSEQ_1: 3;

                  then

                   A203: 1 in ( dom MD1) by A198, FINSEQ_1:def 3;

                  then

                   A204: ( upper_bound ( divset (MD1,1))) = (MD1 . 1) by Def3;

                  let n be Nat;

                  assume that

                   A205: 1 <= n and

                   A206: n <= ( len q1);

                  

                   A207: n = 1 by A111, A205, A206, XXREAL_0: 1;

                  ( lower_bound ( divset (MD1,1))) = ( lower_bound DD1) by A203, Def3;

                  then

                   A208: ( divset (MD1,1)) = [.( lower_bound DD1), (D1 . (k + 1)).] by A204, A202, Th2;

                  ((k + 1) - 1) = k;

                  then

                   A209: ( lower_bound DD1) = (D1 . k) by A103, A107, Def3;

                  ( upper_bound DD1) = (D1 . (k + 1)) by A103, A107, Def3;

                  then

                   A210: ( divset (D1,(k + 1))) = [.(D1 . k), (D1 . (k + 1)).] by A209, Th2;

                  

                   A211: n in ( Seg ( len q1)) by A205, A206, FINSEQ_1: 1;

                  then n in ( dom MD1) by A111, A198, FINSEQ_1:def 3;

                  then

                   A212: (( lower_volume (g,MD1)) . n) = (( lower_bound ( rng (g | ( divset (D1,(k + 1)))))) * ( vol ( divset (D1,(k + 1))))) by A207, A208, A209, A210, Def6;

                  n in ( dom q1) by A211, FINSEQ_1:def 3;

                  

                  then (q1 . n) = (( lower_volume (f,D1)) . (k + 1)) by A110, A112, A207, A201, FINSEQ_1:def 7

                  .= (( lower_bound ( rng (f | ( divset (D1,(k + 1)))))) * ( vol ( divset (D1,(k + 1))))) by A103, Def6;

                  hence thesis by A212;

                end;

                ( len q1) = ( len ( lower_volume (g,MD1))) by A111, A198, Def6;

                then

                 A213: q1 = ( lower_volume (g,MD1)) by A199, FINSEQ_1: 14;

                ( len MD1) = (((k + 1) -' (k + 1)) + 1) by A105, A106, FINSEQ_6: 118;

                then ( len MD1) = (((k + 1) - (k + 1)) + 1) by XREAL_1: 233;

                then

                 A214: ( lower_sum (g,MD1)) <= ( lower_sum (g,MD2)) by A193, A151, Th29;

                ( len ( lower_volume (g,MD2))) = ( len ( mid (D2,(( indx (D2,D1,k)) + 1),( indx (D2,D1,(k + 1)))))) by Def6

                .= (( indx (D2,D1,(k + 1))) - ( indx (D2,D1,k))) by A130, A145, A154, A155, A149, A157, FINSEQ_6: 118;

                hence thesis by A143, A213, A158, A214, FINSEQ_1: 14;

              end;

              set KD2 = (( lower_volume (f,D2)) | ( indx (D2,D1,k)));

              

               A215: ( Sum K1D2) = (( Sum p2) + ( Sum q2)) by A144, RVSUM_1: 75;

              

               A216: ( indx (D2,D1,k)) <= ( len ( lower_volume (f,D2))) by A140, A146, FINSEQ_1: 1;

              then

               A217: ( len p2) = ( len KD2) by A142, FINSEQ_1: 59;

              for i be Nat st 1 <= i & i <= ( len p2) holds (p2 . i) = (KD2 . i)

              proof

                let i be Nat;

                assume that

                 A218: 1 <= i and

                 A219: i <= ( len p2);

                

                 A220: i in ( Seg ( len p2)) by A218, A219, FINSEQ_1: 1;

                then

                 A221: i in ( dom KD2) by A217, FINSEQ_1:def 3;

                then

                 A222: i in ( dom (( lower_volume (f,D2)) | ( Seg ( indx (D2,D1,k))))) by FINSEQ_1:def 15;

                

                 A223: ( dom K1D2) = ( Seg ( len K1D2)) by FINSEQ_1:def 3

                .= ( Seg ( indx (D2,D1,(k + 1)))) by A141, FINSEQ_1: 59;

                

                 A224: ( Seg ( indx (D2,D1,k))) c= ( Seg ( indx (D2,D1,(k + 1)))) by A137, FINSEQ_1: 5;

                ( dom KD2) = ( Seg ( len KD2)) by FINSEQ_1:def 3

                .= ( Seg ( indx (D2,D1,k))) by A216, FINSEQ_1: 59;

                then i in ( dom K1D2) by A221, A224, A223;

                then

                 A225: i in ( dom (( lower_volume (f,D2)) | ( Seg ( indx (D2,D1,(k + 1)))))) by FINSEQ_1:def 15;

                

                 A226: (K1D2 . i) = ((( lower_volume (f,D2)) | ( Seg ( indx (D2,D1,(k + 1))))) . i) by FINSEQ_1:def 15

                .= (( lower_volume (f,D2)) . i) by A225, FUNCT_1: 47;

                

                 A227: (KD2 . i) = ((( lower_volume (f,D2)) | ( Seg ( indx (D2,D1,k)))) . i) by FINSEQ_1:def 15

                .= (( lower_volume (f,D2)) . i) by A222, FUNCT_1: 47;

                i in ( dom p2) by A220, FINSEQ_1:def 3;

                hence thesis by A144, A227, A226, FINSEQ_1:def 7;

              end;

              then

               A228: p2 = KD2 by A217, FINSEQ_1: 14;

              ( Sum K1D1) = (( Sum p1) + ( Sum q1)) by A112, RVSUM_1: 75;

              then ( Sum q1) = (( Sum K1D1) - ( Sum p1));

              then ( Sum K1D1) <= (( Sum q2) + ( Sum p1)) by A148, XREAL_1: 20;

              then (( Sum K1D1) - ( Sum q2)) <= ( Sum p1) by XREAL_1: 20;

              then (( Sum K1D1) - ( Sum q2)) <= ( Sum p2) by A102, A131, A127, A228, FINSEQ_1:def 3, XXREAL_0: 2;

              hence thesis by A215, XREAL_1: 20;

            end;

          end;

          hence thesis;

        end;

        thus for n be non zero Nat holds P[n] from NAT_1:sch 10( A3, A101);

      end;

      hence thesis;

    end;

    theorem :: INTEGRA1:40

    

     Th38: D1 <= D2 & i in ( dom D1) & (f | A) is bounded_above implies (( PartSums ( upper_volume (f,D1))) . i) >= (( PartSums ( upper_volume (f,D2))) . ( indx (D2,D1,i)))

    proof

      assume that

       A1: D1 <= D2 and

       A2: i in ( dom D1) and

       A3: (f | A) is bounded_above;

      

       A4: ( len ( upper_volume (f,D2))) = ( len D2) by Def5;

      i in ( Seg ( len D1)) by A2, FINSEQ_1:def 3;

      then i in ( Seg ( len ( upper_volume (f,D1)))) by Def5;

      then i in ( dom ( upper_volume (f,D1))) by FINSEQ_1:def 3;

      then

       A5: (( PartSums ( upper_volume (f,D1))) . i) = ( Sum (( upper_volume (f,D1)) | i)) by Def19;

      ( indx (D2,D1,i)) in ( dom D2) by A1, A2, Def18;

      then ( indx (D2,D1,i)) in ( Seg ( len ( upper_volume (f,D2)))) by A4, FINSEQ_1:def 3;

      then

       A6: ( indx (D2,D1,i)) in ( dom ( upper_volume (f,D2))) by FINSEQ_1:def 3;

      i in ( Seg ( len D1)) by A2, FINSEQ_1:def 3;

      then i is non zero Element of NAT by FINSEQ_1: 1;

      then (( PartSums ( upper_volume (f,D1))) . i) >= ( Sum (( upper_volume (f,D2)) | ( indx (D2,D1,i)))) by A1, A2, A3, A5, Th36;

      hence thesis by A6, Def19;

    end;

    theorem :: INTEGRA1:41

    

     Th39: D1 <= D2 & i in ( dom D1) & (f | A) is bounded_below implies (( PartSums ( lower_volume (f,D1))) . i) <= (( PartSums ( lower_volume (f,D2))) . ( indx (D2,D1,i)))

    proof

      assume that

       A1: D1 <= D2 and

       A2: i in ( dom D1) and

       A3: (f | A) is bounded_below;

      

       A4: ( len ( lower_volume (f,D2))) = ( len D2) by Def6;

      i in ( Seg ( len D1)) by A2, FINSEQ_1:def 3;

      then i in ( Seg ( len ( lower_volume (f,D1)))) by Def6;

      then i in ( dom ( lower_volume (f,D1))) by FINSEQ_1:def 3;

      then

       A5: (( PartSums ( lower_volume (f,D1))) . i) = ( Sum (( lower_volume (f,D1)) | i)) by Def19;

      ( indx (D2,D1,i)) in ( dom D2) by A1, A2, Def18;

      then ( indx (D2,D1,i)) in ( Seg ( len ( lower_volume (f,D2)))) by A4, FINSEQ_1:def 3;

      then

       A6: ( indx (D2,D1,i)) in ( dom ( lower_volume (f,D2))) by FINSEQ_1:def 3;

      i in ( Seg ( len D1)) by A2, FINSEQ_1:def 3;

      then i is non zero Element of NAT by FINSEQ_1: 1;

      then (( PartSums ( lower_volume (f,D1))) . i) <= ( Sum (( lower_volume (f,D2)) | ( indx (D2,D1,i)))) by A1, A2, A3, A5, Th37;

      hence thesis by A6, Def19;

    end;

    theorem :: INTEGRA1:42

    

     Th40: (( PartSums ( upper_volume (f,D))) . ( len D)) = ( upper_sum (f,D))

    proof

      ( len ( upper_volume (f,D))) = ( len D) by Def5;

      then ( len D) in ( Seg ( len ( upper_volume (f,D)))) by FINSEQ_1: 3;

      then ( len D) in ( dom ( upper_volume (f,D))) by FINSEQ_1:def 3;

      then

       A1: (( PartSums ( upper_volume (f,D))) . ( len D)) = ( Sum (( upper_volume (f,D)) | ( len D))) by Def19;

      ( dom ( upper_volume (f,D))) = ( Seg ( len ( upper_volume (f,D)))) by FINSEQ_1:def 3;

      then ( dom ( upper_volume (f,D))) = ( Seg ( len D)) by Def5;

      then (( upper_volume (f,D)) | ( Seg ( len D))) = ( upper_volume (f,D));

      hence thesis by A1, FINSEQ_1:def 15;

    end;

    theorem :: INTEGRA1:43

    

     Th41: (( PartSums ( lower_volume (f,D))) . ( len D)) = ( lower_sum (f,D))

    proof

      ( len ( lower_volume (f,D))) = ( len D) by Def6;

      then ( len D) in ( Seg ( len ( lower_volume (f,D)))) by FINSEQ_1: 3;

      then ( len D) in ( dom ( lower_volume (f,D))) by FINSEQ_1:def 3;

      then

       A1: (( PartSums ( lower_volume (f,D))) . ( len D)) = ( Sum (( lower_volume (f,D)) | ( len D))) by Def19;

      ( dom ( lower_volume (f,D))) = ( Seg ( len ( lower_volume (f,D)))) by FINSEQ_1:def 3;

      then ( dom ( lower_volume (f,D))) = ( Seg ( len D)) by Def6;

      then (( lower_volume (f,D)) | ( Seg ( len D))) = ( lower_volume (f,D));

      hence thesis by A1, FINSEQ_1:def 15;

    end;

    theorem :: INTEGRA1:44

    

     Th42: D1 <= D2 implies ( indx (D2,D1,( len D1))) = ( len D2)

    proof

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

      then

       A1: ( len D1) in ( dom D1) by FINSEQ_1:def 3;

      assume

       A2: D1 <= D2;

      then (D1 . ( len D1)) = (D2 . ( indx (D2,D1,( len D1)))) by A1, Def18;

      then

       A3: (D2 . ( indx (D2,D1,( len D1)))) = ( upper_bound A) by Def1;

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

      then

       A4: ( len D2) in ( dom D2) by FINSEQ_1:def 3;

      assume

       A5: ( indx (D2,D1,( len D1))) <> ( len D2);

      

       A6: ( indx (D2,D1,( len D1))) in ( dom D2) by A2, A1, Def18;

      then ( indx (D2,D1,( len D1))) in ( Seg ( len D2)) by FINSEQ_1:def 3;

      then ( indx (D2,D1,( len D1))) <= ( len D2) by FINSEQ_1: 1;

      then ( indx (D2,D1,( len D1))) < ( len D2) by A5, XXREAL_0: 1;

      then (D2 . ( indx (D2,D1,( len D1)))) < (D2 . ( len D2)) by A4, A6, SEQM_3:def 1;

      hence contradiction by A3, Def1;

    end;

    theorem :: INTEGRA1:45

    

     Th43: D1 <= D2 & (f | A) is bounded_above implies ( upper_sum (f,D2)) <= ( upper_sum (f,D1))

    proof

      assume that

       A1: D1 <= D2 and

       A2: (f | A) is bounded_above;

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

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

      then (( PartSums ( upper_volume (f,D1))) . ( len D1)) >= (( PartSums ( upper_volume (f,D2))) . ( indx (D2,D1,( len D1)))) by A1, A2, Th38;

      then ( upper_sum (f,D1)) >= (( PartSums ( upper_volume (f,D2))) . ( indx (D2,D1,( len D1)))) by Th40;

      then ( upper_sum (f,D1)) >= (( PartSums ( upper_volume (f,D2))) . ( len D2)) by A1, Th42;

      hence thesis by Th40;

    end;

    theorem :: INTEGRA1:46

    

     Th44: D1 <= D2 & (f | A) is bounded_below implies ( lower_sum (f,D2)) >= ( lower_sum (f,D1))

    proof

      assume that

       A1: D1 <= D2 and

       A2: (f | A) is bounded_below;

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

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

      then (( PartSums ( lower_volume (f,D1))) . ( len D1)) <= (( PartSums ( lower_volume (f,D2))) . ( indx (D2,D1,( len D1)))) by A1, A2, Th39;

      then ( lower_sum (f,D1)) <= (( PartSums ( lower_volume (f,D2))) . ( indx (D2,D1,( len D1)))) by Th41;

      then ( lower_sum (f,D1)) <= (( PartSums ( lower_volume (f,D2))) . ( len D2)) by A1, Th42;

      hence thesis by Th41;

    end;

    theorem :: INTEGRA1:47

    

     Th45: ex D be Division of A st D1 <= D & D2 <= D

    proof

      consider D3 be FinSequence of REAL such that

       A1: ( rng D3) = ( rng (D1 ^ D2)) and

       A2: ( len D3) = ( card ( rng (D1 ^ D2))) and

       A3: D3 is increasing by SEQ_4: 140;

      reconsider D3 as non empty increasing FinSequence of REAL by A1, A3;

      

       A4: ( rng D2) c= A by Def1;

      ( rng D1) c= A by Def1;

      then (( rng D1) \/ ( rng D2)) c= A by A4, XBOOLE_1: 8;

      then

       A5: ( rng D3) c= A by A1, FINSEQ_1: 31;

      (D3 . ( len D3)) = ( upper_bound A)

      proof

        assume

         A6: (D3 . ( len D3)) <> ( upper_bound A);

        now

          per cases by A6, XXREAL_0: 1;

            suppose

             A7: (D3 . ( len D3)) > ( upper_bound A);

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

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

            then (D3 . ( len D3)) in ( rng D3) by FUNCT_1:def 3;

            then (D3 . ( len D3)) in A by A5;

            then (D3 . ( len D3)) in [.( lower_bound A), ( upper_bound A).] by Th2;

            then (D3 . ( len D3)) in { r : ( lower_bound A) <= r & r <= ( upper_bound A) } by RCOMP_1:def 1;

            then ex a st a = (D3 . ( len D3)) & ( lower_bound A) <= a & a <= ( upper_bound A);

            hence contradiction by A7;

          end;

            suppose

             A8: (D3 . ( len D3)) < ( upper_bound A);

            

             A9: ( rng D1) c= ( rng (D1 ^ D2)) by FINSEQ_1: 29;

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

            then

             A10: ( len D1) in ( dom D1) by FINSEQ_1:def 3;

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

            then

             A11: ( len D3) in ( dom D3) by FINSEQ_1:def 3;

            (D1 . ( len D1)) = ( upper_bound A) by Def1;

            then ( upper_bound A) in ( rng D1) by A10, FUNCT_1:def 3;

            then

            consider k be Nat such that

             A12: k in ( dom D3) and

             A13: (D3 . k) = ( upper_bound A) by A1, A9, FINSEQ_2: 10;

            k in ( Seg ( len D3)) by A12, FINSEQ_1:def 3;

            then k <= ( len D3) by FINSEQ_1: 1;

            hence contradiction by A8, A11, A12, A13, SEQ_4: 137;

          end;

        end;

        hence thesis;

      end;

      then

      reconsider D3 as Division of A by A5, Def1;

      ( len D2) = ( card ( rng D2)) by FINSEQ_4: 62;

      then

       A14: ( len D2) <= ( len D3) by A2, FINSEQ_1: 30, NAT_1: 43;

      take D3;

      

       A15: ( rng D1) c= ( rng (D1 ^ D2)) by FINSEQ_1: 29;

      

       A16: ( rng D2) c= ( rng (D1 ^ D2)) by FINSEQ_1: 30;

      ( len D1) = ( card ( rng D1)) by FINSEQ_4: 62;

      then ( len D1) <= ( len D3) by A2, FINSEQ_1: 29, NAT_1: 43;

      hence thesis by A1, A15, A16, A14;

    end;

    theorem :: INTEGRA1:48

    

     Th46: (f | A) is bounded implies ( lower_sum (f,D1)) <= ( upper_sum (f,D2))

    proof

      consider D such that

       A1: D1 <= D and

       A2: D2 <= D by Th45;

      assume

       A3: (f | A) is bounded;

      then

       A4: ( lower_sum (f,D)) <= ( upper_sum (f,D)) by Th26;

      ( upper_sum (f,D)) <= ( upper_sum (f,D2)) by A3, A2, Th43;

      then

       A5: ( lower_sum (f,D)) <= ( upper_sum (f,D2)) by A4, XXREAL_0: 2;

      ( lower_sum (f,D1)) <= ( lower_sum (f,D)) by A3, A1, Th44;

      hence thesis by A5, XXREAL_0: 2;

    end;

    begin

    theorem :: INTEGRA1:49

    

     Th47: (f | A) is bounded implies ( upper_integral f) >= ( lower_integral f)

    proof

      assume

       A1: (f | A) is bounded;

      

       A2: for b be Real st b in ( rng ( upper_sum_set f)) holds ( lower_integral f) <= b

      proof

        let b be Real;

        assume b in ( rng ( upper_sum_set f));

        then

        consider D1 be Element of ( divs A) such that D1 in ( dom ( upper_sum_set f)) and

         A3: b = (( upper_sum_set f) . D1) by PARTFUN1: 3;

        reconsider D1 as Division of A by Def2;

        

         A4: for a be Real st a in ( rng ( lower_sum_set f)) holds a <= ( upper_sum (f,D1))

        proof

          let a be Real;

          assume a in ( rng ( lower_sum_set f));

          then

          consider D2 be Element of ( divs A) such that D2 in ( dom ( lower_sum_set f)) and

           A5: a = (( lower_sum_set f) . D2) by PARTFUN1: 3;

          reconsider D2 as Division of A by Def2;

          a = ( lower_sum (f,D2)) by A5, Def10;

          hence thesis by A1, Th46;

        end;

        b = ( upper_sum (f,D1)) by A3, Def9;

        hence thesis by A4, SEQ_4: 45;

      end;

      thus thesis by A2, SEQ_4: 43;

    end;

    theorem :: INTEGRA1:50

    

     Th48: for X,Y be Subset of REAL holds (( -- X) ++ ( -- Y)) = ( -- (X ++ Y))

    proof

      let X,Y be Subset of REAL ;

      for z be object st z in ( -- (X ++ Y)) holds z in (( -- X) ++ ( -- Y))

      proof

        let z be object;

        assume

         A1: z in ( -- (X ++ Y));

        reconsider XY = (X ++ Y) as Subset of REAL by MEMBERED: 3;

        z in ( -- XY) by A1;

        then

        consider x be Real such that

         A2: x in XY and

         A3: z = ( - x) by MEASURE6: 72;

        consider a,b be Real such that

         A4: a in X and

         A5: b in Y and

         A6: x = (a + b) by A2, MEASURE6: 21;

        

         A7: ( - a) in ( -- X) by A4, MEMBER_1: 11;

        

         A8: ( - b) in ( -- Y) by A5, MEMBER_1: 11;

        z = (( - a) + ( - b)) by A3, A6;

        hence thesis by A7, A8, MEMBER_1: 46;

      end;

      then

       A9: ( -- (X ++ Y)) c= (( -- X) ++ ( -- Y));

      for z be object st z in (( -- X) ++ ( -- Y)) holds z in ( -- (X ++ Y))

      proof

        let z be object;

        assume

         A10: z in (( -- X) ++ ( -- Y));

        consider x,y be Real such that

         A11: x in ( -- X) and

         A12: y in ( -- Y) and

         A13: z = (x + y) by A10, MEASURE6: 21;

        consider b be Real such that

         A14: b in Y and

         A15: y = ( - b) by A12, MEASURE6: 72;

        reconsider X as Subset of REAL ;

        consider a be Real such that

         A16: a in X and

         A17: x = ( - a) by A11, MEASURE6: 72;

        

         A18: (a + b) in (X ++ Y) by A16, A14, MEMBER_1: 46;

        z = ( - (a + b)) by A13, A17, A15;

        hence thesis by A18, MEMBER_1: 11;

      end;

      then (( -- X) ++ ( -- Y)) c= ( -- (X ++ Y));

      hence thesis by A9;

    end;

    theorem :: INTEGRA1:51

    

     Th49: for X,Y be Subset of REAL st X is bounded_above & Y is bounded_above holds (X ++ Y) is bounded_above

    proof

      let X,Y be Subset of REAL ;

      assume that

       A1: X is bounded_above and

       A2: Y is bounded_above;

      

       A3: ( -- Y) is bounded_below by A2, MEASURE6: 41;

      ( -- X) is bounded_below by A1, MEASURE6: 41;

      then

       A4: (( -- X) ++ ( -- Y)) is bounded_below by A3, SEQ_4: 124;

      reconsider XY = (X ++ Y) as Subset of REAL by MEMBERED: 3;

      ( -- XY) is bounded_below by Th48, A4;

      hence thesis by MEASURE6: 41;

    end;

    theorem :: INTEGRA1:52

    

     Th50: for X,Y be non empty Subset of REAL st X is bounded_above & Y is bounded_above holds ( upper_bound (X ++ Y)) = (( upper_bound X) + ( upper_bound Y))

    proof

      let X,Y be non empty Subset of REAL ;

      assume that

       A1: X is bounded_above and

       A2: Y is bounded_above;

      

       A3: ( -- Y) is bounded_below by A2, MEASURE6: 41;

      

       A4: ( -- X) is bounded_below by A1, MEASURE6: 41;

      then ( lower_bound (( -- X) ++ ( -- Y))) = (( lower_bound ( -- X)) + ( lower_bound ( -- Y))) by A3, SEQ_4: 125;

      

      then

       A5: ( lower_bound (( -- X) ++ ( -- Y))) = (( - ( upper_bound ( -- ( -- X)))) + ( lower_bound ( -- Y))) by A4, MEASURE6: 43

      .= (( - ( upper_bound X)) + ( - ( upper_bound ( -- ( -- Y))))) by A3, MEASURE6: 43

      .= ( - (( upper_bound X) + ( upper_bound Y)));

      

       A6: (( -- X) ++ ( -- Y)) = ( -- (X ++ Y)) by Th48;

      then

       A7: ( -- (X ++ Y)) is bounded_below by A4, A3, SEQ_4: 124;

      reconsider XY = (X ++ Y) as Subset of REAL by MEMBERED: 3;

      ( - ( upper_bound ( -- ( -- XY)))) = ( - (( upper_bound X) + ( upper_bound Y))) by A6, A5, A7, MEASURE6: 43;

      then ( upper_bound XY) = (( upper_bound X) + ( upper_bound Y));

      hence thesis;

    end;

    theorem :: INTEGRA1:53

    

     Th51: i in ( dom D) & (f | A) is bounded_above & (g | A) is bounded_above implies (( upper_volume ((f + g),D)) . i) <= ((( upper_volume (f,D)) . i) + (( upper_volume (g,D)) . i))

    proof

      assume

       A1: i in ( dom D);

      ( dom (f + g)) = (A /\ A) by FUNCT_2:def 1;

      then ( dom ((f + g) | ( divset (D,i)))) = ( divset (D,i)) by A1, Th6, RELAT_1: 62;

      then

       A2: ( rng ((f + g) | ( divset (D,i)))) is non empty by RELAT_1: 42;

      ((f + g) | ( divset (D,i))) = ((f | ( divset (D,i))) + (g | ( divset (D,i)))) by RFUNCT_1: 44;

      then

       A3: ( rng ((f + g) | ( divset (D,i)))) c= (( rng (f | ( divset (D,i)))) ++ ( rng (g | ( divset (D,i))))) by Th8;

      assume (f | A) is bounded_above;

      then ( rng f) is bounded_above by Th11;

      then

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

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

      then ( dom (g | ( divset (D,i)))) = ( divset (D,i)) by A1, Th6, RELAT_1: 62;

      then

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

      

       A6: 0 <= ( vol ( divset (D,i))) by SEQ_4: 11, XREAL_1: 48;

      assume (g | A) is bounded_above;

      then ( rng g) is bounded_above by Th11;

      then

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

      then

       A8: (( rng (f | ( divset (D,i)))) ++ ( rng (g | ( divset (D,i))))) is bounded_above by A4, Th49;

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

      then ( dom (f | ( divset (D,i)))) = ( divset (D,i)) by A1, Th6, RELAT_1: 62;

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

      then ( upper_bound (( rng (f | ( divset (D,i)))) ++ ( rng (g | ( divset (D,i)))))) = (( upper_bound ( rng (f | ( divset (D,i))))) + ( upper_bound ( rng (g | ( divset (D,i)))))) by A4, A7, A5, Th50;

      then (( upper_bound ( rng ((f + g) | ( divset (D,i))))) * ( vol ( divset (D,i)))) <= ((( upper_bound ( rng (f | ( divset (D,i))))) + ( upper_bound ( rng (g | ( divset (D,i)))))) * ( vol ( divset (D,i)))) by A8, A2, A6, A3, SEQ_4: 48, XREAL_1: 64;

      then (( upper_volume ((f + g),D)) . i) <= ((( upper_bound ( rng (f | ( divset (D,i))))) * ( vol ( divset (D,i)))) + (( upper_bound ( rng (g | ( divset (D,i))))) * ( vol ( divset (D,i))))) by A1, Def5;

      then (( upper_volume ((f + g),D)) . i) <= ((( upper_volume (f,D)) . i) + (( upper_bound ( rng (g | ( divset (D,i))))) * ( vol ( divset (D,i))))) by A1, Def5;

      hence thesis by A1, Def5;

    end;

    theorem :: INTEGRA1:54

    

     Th52: i in ( dom D) & (f | A) is bounded_below & (g | A) is bounded_below implies ((( lower_volume (f,D)) . i) + (( lower_volume (g,D)) . i)) <= (( lower_volume ((f + g),D)) . i)

    proof

      assume that

       A1: i in ( dom D) and

       A2: (f | A) is bounded_below and

       A3: (g | A) is bounded_below;

      

       A4: 0 <= ( vol ( divset (D,i))) by SEQ_4: 11, XREAL_1: 48;

      ( dom (f + g)) = (A /\ A) by FUNCT_2:def 1;

      then ( dom ((f + g) | ( divset (D,i)))) = ( divset (D,i)) by A1, Th6, RELAT_1: 62;

      then

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

      ( rng g) is bounded_below by A3, Th9;

      then

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

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

      then ( dom (g | ( divset (D,i)))) = ( divset (D,i)) by A1, Th6, RELAT_1: 62;

      then

       A7: ( rng (g | ( divset (D,i)))) is non empty by RELAT_1: 42;

      ((f + g) | ( divset (D,i))) = ((f | ( divset (D,i))) + (g | ( divset (D,i)))) by RFUNCT_1: 44;

      then

       A8: ( rng ((f + g) | ( divset (D,i)))) c= (( rng (f | ( divset (D,i)))) ++ ( rng (g | ( divset (D,i))))) by Th8;

      ( rng f) is bounded_below by A2, Th9;

      then

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

      then

       A10: (( rng (f | ( divset (D,i)))) ++ ( rng (g | ( divset (D,i))))) is bounded_below by A6, SEQ_4: 124;

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

      then ( dom (f | ( divset (D,i)))) = ( divset (D,i)) by A1, Th6, RELAT_1: 62;

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

      then ( lower_bound (( rng (f | ( divset (D,i)))) ++ ( rng (g | ( divset (D,i)))))) = (( lower_bound ( rng (f | ( divset (D,i))))) + ( lower_bound ( rng (g | ( divset (D,i)))))) by A9, A6, A7, SEQ_4: 125;

      then (( lower_bound ( rng ((f + g) | ( divset (D,i))))) * ( vol ( divset (D,i)))) >= ((( lower_bound ( rng (f | ( divset (D,i))))) + ( lower_bound ( rng (g | ( divset (D,i)))))) * ( vol ( divset (D,i)))) by A10, A5, A4, A8, SEQ_4: 47, XREAL_1: 64;

      then (( lower_volume ((f + g),D)) . i) >= ((( lower_bound ( rng (f | ( divset (D,i))))) * ( vol ( divset (D,i)))) + (( lower_bound ( rng (g | ( divset (D,i))))) * ( vol ( divset (D,i))))) by A1, Def6;

      then (( lower_volume ((f + g),D)) . i) >= ((( lower_volume (f,D)) . i) + (( lower_bound ( rng (g | ( divset (D,i))))) * ( vol ( divset (D,i))))) by A1, Def6;

      hence thesis by A1, Def6;

    end;

    theorem :: INTEGRA1:55

    

     Th53: (f | A) is bounded_above & (g | A) is bounded_above implies ( upper_sum ((f + g),D)) <= (( upper_sum (f,D)) + ( upper_sum (g,D)))

    proof

      assume that

       A1: (f | A) is bounded_above and

       A2: (g | A) is bounded_above;

      set H = ( upper_volume ((f + g),D));

      set G = ( upper_volume (g,D));

      set F = ( upper_volume (f,D));

      ( len G) = ( len D) by Def5;

      then

       A3: G is Element of (( len D) -tuples_on REAL ) by FINSEQ_2: 92;

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

      then

       A4: F is Element of (( len D) -tuples_on REAL ) by FINSEQ_2: 92;

      

       A5: for j be Nat st j in ( Seg ( len D)) holds (H . j) <= ((F + G) . j)

      proof

        let j be Nat;

        assume j in ( Seg ( len D));

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

        then (( upper_volume ((f + g),D)) . j) <= ((( upper_volume (f,D)) . j) + (( upper_volume (g,D)) . j)) by A1, A2, Th51;

        hence thesis by A4, A3, RVSUM_1: 11;

      end;

      ( len H) = ( len D) by Def5;

      then

       A6: H is Element of (( len D) -tuples_on REAL ) by FINSEQ_2: 92;

      (F + G) is Element of (( len D) -tuples_on REAL ) by A4, A3, FINSEQ_2: 120;

      then ( Sum H) <= ( Sum (F + G)) by A6, A5, RVSUM_1: 82;

      hence thesis by A4, A3, RVSUM_1: 89;

    end;

    theorem :: INTEGRA1:56

    

     Th54: (f | A) is bounded_below & (g | A) is bounded_below implies (( lower_sum (f,D)) + ( lower_sum (g,D))) <= ( lower_sum ((f + g),D))

    proof

      assume that

       A1: (f | A) is bounded_below and

       A2: (g | A) is bounded_below;

      set H = ( lower_volume ((f + g),D));

      set G = ( lower_volume (g,D));

      set F = ( lower_volume (f,D));

      ( len G) = ( len D) by Def6;

      then

       A3: G is Element of (( len D) -tuples_on REAL ) by FINSEQ_2: 92;

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

      then

       A4: F is Element of (( len D) -tuples_on REAL ) by FINSEQ_2: 92;

      

       A5: for j be Nat st j in ( Seg ( len D)) holds ((F + G) . j) <= (H . j)

      proof

        let j be Nat;

        assume j in ( Seg ( len D));

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

        then ((( lower_volume (f,D)) . j) + (( lower_volume (g,D)) . j)) <= (( lower_volume ((f + g),D)) . j) by A1, A2, Th52;

        hence thesis by A4, A3, RVSUM_1: 11;

      end;

      ( len H) = ( len D) by Def6;

      then

       A6: H is Element of (( len D) -tuples_on REAL ) by FINSEQ_2: 92;

      (F + G) is Element of (( len D) -tuples_on REAL ) by A4, A3, FINSEQ_2: 120;

      then ( Sum (F + G)) <= ( Sum H) by A6, A5, RVSUM_1: 82;

      hence thesis by A4, A3, RVSUM_1: 89;

    end;

    theorem :: INTEGRA1:57

    (f | A) is bounded & (g | A) is bounded & f is integrable & g is integrable implies (f + g) is integrable & ( integral (f + g)) = (( integral f) + ( integral g))

    proof

      assume that

       A1: (f | A) is bounded and

       A2: (g | A) is bounded and

       A3: f is integrable and

       A4: g is integrable;

      

       A5: (( lower_integral f) + ( lower_integral g)) = (( upper_integral f) + ( lower_integral g)) by A3

      .= (( integral f) + ( integral g)) by A4;

      

       A6: ((f + g) | (A /\ A)) is bounded by A1, A2, RFUNCT_1: 83;

      for D be object st D in (( divs A) /\ ( dom ( lower_sum_set (f + g)))) holds (( lower_sum_set (f + g)) . D) <= ((( upper_bound ( rng f)) * ( vol A)) + (( upper_bound ( rng g)) * ( vol A)))

      proof

        let D be object;

        assume D in (( divs A) /\ ( dom ( lower_sum_set (f + g))));

        then

        reconsider D as Division of A by Def2;

        (( lower_sum_set (f + g)) . D) = ( lower_sum ((f + g),D)) by Def10;

        then

         A7: (( lower_sum_set (f + g)) . D) <= ( upper_sum ((f + g),D)) by A6, Th26;

        ( upper_sum (f,D)) <= (( upper_bound ( rng f)) * ( vol A)) by A1, Th25;

        then

         A8: (( upper_sum (f,D)) + ( upper_sum (g,D))) <= ((( upper_bound ( rng f)) * ( vol A)) + ( upper_sum (g,D))) by XREAL_1: 6;

        ( upper_sum (g,D)) <= (( upper_bound ( rng g)) * ( vol A)) by A2, Th25;

        then

         A9: ((( upper_bound ( rng f)) * ( vol A)) + ( upper_sum (g,D))) <= ((( upper_bound ( rng f)) * ( vol A)) + (( upper_bound ( rng g)) * ( vol A))) by XREAL_1: 6;

        ( upper_sum ((f + g),D)) <= (( upper_sum (f,D)) + ( upper_sum (g,D))) by A1, A2, Th53;

        then (( lower_sum_set (f + g)) . D) <= (( upper_sum (f,D)) + ( upper_sum (g,D))) by A7, XXREAL_0: 2;

        then (( lower_sum_set (f + g)) . D) <= ((( upper_bound ( rng f)) * ( vol A)) + ( upper_sum (g,D))) by A8, XXREAL_0: 2;

        hence thesis by A9, XXREAL_0: 2;

      end;

      then (( lower_sum_set (f + g)) | ( divs A)) is bounded_above by RFUNCT_1: 70;

      then

       A10: ( rng ( lower_sum_set (f + g))) is bounded_above by Th11;

      then

       A11: (f + g) is lower_integrable;

      for D be object st D in (( divs A) /\ ( dom ( upper_sum_set (f + g)))) holds ((( lower_bound ( rng f)) * ( vol A)) + (( lower_bound ( rng g)) * ( vol A))) <= (( upper_sum_set (f + g)) . D)

      proof

        let D be object;

        assume D in (( divs A) /\ ( dom ( upper_sum_set (f + g))));

        then

        reconsider D as Division of A by Def2;

        (( upper_sum_set (f + g)) . D) = ( upper_sum ((f + g),D)) by Def9;

        then

         A12: ( lower_sum ((f + g),D)) <= (( upper_sum_set (f + g)) . D) by A6, Th26;

        (( lower_bound ( rng f)) * ( vol A)) <= ( lower_sum (f,D)) by A1, Th23;

        then

         A13: ((( lower_bound ( rng f)) * ( vol A)) + ( lower_sum (g,D))) <= (( lower_sum (f,D)) + ( lower_sum (g,D))) by XREAL_1: 6;

        (( lower_bound ( rng g)) * ( vol A)) <= ( lower_sum (g,D)) by A2, Th23;

        then

         A14: ((( lower_bound ( rng f)) * ( vol A)) + (( lower_bound ( rng g)) * ( vol A))) <= ((( lower_bound ( rng f)) * ( vol A)) + ( lower_sum (g,D))) by XREAL_1: 6;

        (( lower_sum (f,D)) + ( lower_sum (g,D))) <= ( lower_sum ((f + g),D)) by A1, A2, Th54;

        then (( lower_sum (f,D)) + ( lower_sum (g,D))) <= (( upper_sum_set (f + g)) . D) by A12, XXREAL_0: 2;

        then ((( lower_bound ( rng f)) * ( vol A)) + ( lower_sum (g,D))) <= (( upper_sum_set (f + g)) . D) by A13, XXREAL_0: 2;

        hence thesis by A14, XXREAL_0: 2;

      end;

      then (( upper_sum_set (f + g)) | ( divs A)) is bounded_below by RFUNCT_1: 71;

      then

       A15: ( rng ( upper_sum_set (f + g))) is bounded_below by Th9;

      

       A16: for D st D in (( divs A) /\ ( dom ( upper_sum_set (f + g)))) holds ((( upper_sum_set f) . D) + (( upper_sum_set g) . D)) >= ( upper_integral (f + g))

      proof

        let D;

        (( upper_sum (f,D)) + ( upper_sum (g,D))) >= ( upper_sum ((f + g),D)) by A1, A2, Th53;

        then

         A17: ((( upper_sum_set f) . D) + ( upper_sum (g,D))) >= ( upper_sum ((f + g),D)) by Def9;

        assume D in (( divs A) /\ ( dom ( upper_sum_set (f + g))));

        then D in ( dom ( upper_sum_set (f + g))) by XBOOLE_0:def 4;

        then (( upper_sum_set (f + g)) . D) in ( rng ( upper_sum_set (f + g))) by FUNCT_1:def 3;

        then

         A18: (( upper_sum_set (f + g)) . D) >= ( upper_integral (f + g)) by A15, SEQ_4:def 2;

        ((( upper_sum_set f) . D) + (( upper_sum_set g) . D)) >= ( upper_sum ((f + g),D)) by A17, Def9;

        then ((( upper_sum_set f) . D) + (( upper_sum_set g) . D)) >= (( upper_sum_set (f + g)) . D) by Def9;

        hence thesis by A18, XXREAL_0: 2;

      end;

      

       A19: ( dom ( upper_sum_set (f + g))) = ( divs A) by FUNCT_2:def 1;

      

       A20: for a1 be Real st a1 in ( rng ( upper_sum_set f)) holds a1 >= (( upper_integral (f + g)) - ( upper_integral g))

      proof

        let a1 be Real;

        assume a1 in ( rng ( upper_sum_set f));

        then

        consider D1 be Element of ( divs A) such that D1 in ( dom ( upper_sum_set f)) and

         A21: a1 = (( upper_sum_set f) . D1) by PARTFUN1: 3;

        reconsider D1 as Division of A by Def2;

        

         A22: a1 = ( upper_sum (f,D1)) by A21, Def9;

        for a2 be Real st a2 in ( rng ( upper_sum_set g)) holds a2 >= (( upper_integral (f + g)) - a1)

        proof

          let a2 be Real;

          assume a2 in ( rng ( upper_sum_set g));

          then

          consider D2 be Element of ( divs A) such that D2 in ( dom ( upper_sum_set g)) and

           A23: a2 = (( upper_sum_set g) . D2) by PARTFUN1: 3;

          reconsider D2 as Division of A by Def2;

          consider D such that

           A24: D1 <= D and

           A25: D2 <= D by Th45;

          

           A26: D in ( divs A) by Def2;

          (( upper_sum_set g) . D) = ( upper_sum (g,D)) by Def9;

          then

           A27: (( upper_sum_set g) . D) <= ( upper_sum (g,D2)) by A2, A25, Th43;

          (( upper_sum_set f) . D) = ( upper_sum (f,D)) by Def9;

          then (( upper_sum_set f) . D) <= ( upper_sum (f,D1)) by A1, A24, Th43;

          then

           A28: ((( upper_sum_set f) . D) + (( upper_sum_set g) . D)) <= (( upper_sum (f,D1)) + ( upper_sum (g,D2))) by A27, XREAL_1: 7;

          ((( upper_sum_set f) . D) + (( upper_sum_set g) . D)) >= ( upper_integral (f + g)) by A19, A16, A26;

          then

           A29: (( upper_sum (f,D1)) + ( upper_sum (g,D2))) >= ( upper_integral (f + g)) by A28, XXREAL_0: 2;

          a2 = ( upper_sum (g,D2)) by A23, Def9;

          hence thesis by A22, A29, XREAL_1: 20;

        end;

        then ( lower_bound ( rng ( upper_sum_set g))) >= (( upper_integral (f + g)) - a1) by SEQ_4: 43;

        then (a1 + ( lower_bound ( rng ( upper_sum_set g)))) >= ( upper_integral (f + g)) by XREAL_1: 20;

        hence thesis by XREAL_1: 20;

      end;

      ( upper_integral f) >= (( upper_integral (f + g)) - ( upper_integral g)) by A20, SEQ_4: 43;

      then

       A30: (( integral f) + ( upper_integral g)) >= ( upper_integral (f + g)) by XREAL_1: 20;

      

       A31: for D st D in (( divs A) /\ ( dom ( lower_sum_set (f + g)))) holds ((( lower_sum_set f) . D) + (( lower_sum_set g) . D)) <= ( lower_integral (f + g))

      proof

        let D;

        (( lower_sum (f,D)) + ( lower_sum (g,D))) <= ( lower_sum ((f + g),D)) by A1, A2, Th54;

        then

         A32: ((( lower_sum_set f) . D) + ( lower_sum (g,D))) <= ( lower_sum ((f + g),D)) by Def10;

        assume D in (( divs A) /\ ( dom ( lower_sum_set (f + g))));

        then D in ( dom ( lower_sum_set (f + g))) by XBOOLE_0:def 4;

        then (( lower_sum_set (f + g)) . D) in ( rng ( lower_sum_set (f + g))) by FUNCT_1:def 3;

        then

         A33: (( lower_sum_set (f + g)) . D) <= ( lower_integral (f + g)) by A10, SEQ_4:def 1;

        ((( lower_sum_set f) . D) + (( lower_sum_set g) . D)) <= ( lower_sum ((f + g),D)) by A32, Def10;

        then ((( lower_sum_set f) . D) + (( lower_sum_set g) . D)) <= (( lower_sum_set (f + g)) . D) by Def10;

        hence thesis by A33, XXREAL_0: 2;

      end;

      

       A34: ( dom ( lower_sum_set (f + g))) = ( divs A) by FUNCT_2:def 1;

      

       A35: for a1 be Real st a1 in ( rng ( lower_sum_set f)) holds a1 <= (( lower_integral (f + g)) - ( lower_integral g))

      proof

        let a1 be Real;

        assume a1 in ( rng ( lower_sum_set f));

        then

        consider D1 be Element of ( divs A) such that D1 in ( dom ( lower_sum_set f)) and

         A36: a1 = (( lower_sum_set f) . D1) by PARTFUN1: 3;

        reconsider D1 as Division of A by Def2;

        

         A37: a1 = ( lower_sum (f,D1)) by A36, Def10;

        for a2 be Real st a2 in ( rng ( lower_sum_set g)) holds a2 <= (( lower_integral (f + g)) - a1)

        proof

          let a2 be Real;

          assume a2 in ( rng ( lower_sum_set g));

          then

          consider D2 be Element of ( divs A) such that D2 in ( dom ( lower_sum_set g)) and

           A38: a2 = (( lower_sum_set g) . D2) by PARTFUN1: 3;

          reconsider D2 as Division of A by Def2;

          consider D such that

           A39: D1 <= D and

           A40: D2 <= D by Th45;

          

           A41: D in ( divs A) by Def2;

          (( lower_sum_set g) . D) = ( lower_sum (g,D)) by Def10;

          then

           A42: (( lower_sum_set g) . D) >= ( lower_sum (g,D2)) by A2, A40, Th44;

          (( lower_sum_set f) . D) = ( lower_sum (f,D)) by Def10;

          then (( lower_sum_set f) . D) >= ( lower_sum (f,D1)) by A1, A39, Th44;

          then

           A43: ((( lower_sum_set f) . D) + (( lower_sum_set g) . D)) >= (( lower_sum (f,D1)) + ( lower_sum (g,D2))) by A42, XREAL_1: 7;

          ((( lower_sum_set f) . D) + (( lower_sum_set g) . D)) <= ( lower_integral (f + g)) by A34, A31, A41;

          then

           A44: (( lower_sum (f,D1)) + ( lower_sum (g,D2))) <= ( lower_integral (f + g)) by A43, XXREAL_0: 2;

          a2 = ( lower_sum (g,D2)) by A38, Def10;

          hence thesis by A37, A44, XREAL_1: 19;

        end;

        then ( upper_bound ( rng ( lower_sum_set g))) <= (( lower_integral (f + g)) - a1) by SEQ_4: 45;

        then (a1 + ( upper_bound ( rng ( lower_sum_set g)))) <= ( lower_integral (f + g)) by XREAL_1: 19;

        hence thesis by XREAL_1: 19;

      end;

      ( upper_bound ( rng ( lower_sum_set f))) <= (( lower_integral (f + g)) - ( lower_integral g)) by A35, SEQ_4: 45;

      then

       A45: (( lower_integral f) + ( lower_integral g)) <= ( lower_integral (f + g)) by XREAL_1: 19;

      

       A46: ( upper_integral (f + g)) >= ( lower_integral (f + g)) by A6, Th47;

      then (( integral f) + ( integral g)) <= ( upper_integral (f + g)) by A45, A5, XXREAL_0: 2;

      then ( upper_integral (f + g)) = (( integral f) + ( integral g)) by A30, XXREAL_0: 1;

      then

       A47: ( upper_integral (f + g)) = ( lower_integral (f + g)) by A45, A46, A5, XXREAL_0: 1;

      (f + g) is upper_integrable by A15;

      hence thesis by A11, A45, A5, A30, A47, XXREAL_0: 1;

    end;

    theorem :: INTEGRA1:58

    for f be FinSequence holds i in ( dom f) & j in ( dom f) & i <= j implies ( len ( mid (f,i,j))) = ((j - i) + 1) by Lm1;