integra2.miz



    begin

    reserve a,b,r,x,y for Real,

i,j,k,n for Nat,

x1 for set,

p for FinSequence of REAL ;

    theorem :: INTEGRA2:1

    for A be non empty closed_interval Subset of REAL , x be Real holds x in A iff ( lower_bound A) <= x & x <= ( upper_bound A)

    proof

      let A be non empty closed_interval Subset of REAL ;

      let x be Real;

      hereby

        assume x in A;

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

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

        then ex a st a = x & ( lower_bound A) <= a & a <= ( upper_bound A);

        hence ( lower_bound A) <= x & x <= ( upper_bound A);

      end;

      assume

       A1: ( lower_bound A) <= x & x <= ( upper_bound A);

      x in { a : ( lower_bound A) <= a & a <= ( upper_bound A) } by A1;

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

      hence thesis by INTEGRA1: 4;

    end;

    

     LM: for p be FinSequence of REAL st for n be Nat st n in ( dom p) & (n + 1) in ( dom p) holds (p . n) <= (p . (n + 1)) holds for i, j st i in ( dom p) & j in ( dom p) & i <= j holds (p . i) <= (p . j)

    proof

      let p be FinSequence of REAL ;

      assume

       A0: for n be Nat st n in ( dom p) & (n + 1) in ( dom p) holds (p . n) <= (p . (n + 1));

      let i, j;

      assume

       A1: i in ( dom p);

      defpred P[ Nat] means for i, j st j = (i + $1) & i in ( dom p) & j in ( dom p) holds (p . i) <= (p . j);

      assume

       A2: j in ( dom p);

      

       A3: for k st P[k] holds P[(k + 1)]

      proof

        let k;

        assume

         A4: P[k];

         P[(k + 1)]

        proof

          let i, j;

          reconsider l = (i + k) as Nat;

          assume j = (i + (k + 1));

          then

           A5: j = (l + 1);

          assume

           A6: i in ( dom p);

          then 1 <= i by FINSEQ_3: 25;

          then

           A7: (1 + 0 ) <= l by XREAL_1: 7;

          assume

           A8: j in ( dom p);

          then j <= ( len p) by FINSEQ_3: 25;

          then l < ( len p) by A5, NAT_1: 13;

          then

           A9: l in ( dom p) by A7, FINSEQ_3: 25;

          then

           A10: (p . i) <= (p . l) by A4, A6;

          (p . l) <= (p . j) by A0, A8, A5, A9;

          hence thesis by A10, XXREAL_0: 2;

        end;

        hence thesis;

      end;

      

       A11: P[ 0 ];

      

       A12: for k holds P[k] from NAT_1:sch 2( A11, A3);

      assume i <= j;

      then

      consider n be Nat such that

       A13: j = (i + n) by NAT_1: 10;

      reconsider n as Nat;

      j = (i + n) by A13;

      hence thesis by A1, A2, A12;

    end;

    definition

      let IT be FinSequence of REAL ;

      :: original: non-decreasing

      redefine

      :: INTEGRA2:def1

      attr IT is non-decreasing means

      : Def1: for n be Nat st n in ( dom IT) & (n + 1) in ( dom IT) holds (IT . n) <= (IT . (n + 1));

      compatibility

      proof

        thus IT is non-decreasing implies for n st n in ( dom IT) & (n + 1) in ( dom IT) holds (IT . n) <= (IT . (n + 1)) by NAT_1: 11, VALUED_0:def 15;

        assume for n be Nat st n in ( dom IT) & (n + 1) in ( dom IT) holds (IT . n) <= (IT . (n + 1));

        then for e1,e2 be ExtReal st e1 in ( dom IT) & e2 in ( dom IT) & e1 <= e2 holds (IT . e1) <= (IT . e2) by LM;

        hence thesis by VALUED_0:def 15;

      end;

    end

    registration

      cluster non-decreasing for FinSequence of REAL ;

      existence

      proof

        take f = ( <*> REAL );

        let n;

        assume that

         A1: n in ( dom f) and (n + 1) in ( dom f);

        thus thesis by A1;

      end;

    end

    theorem :: INTEGRA2:2

    for p be non-decreasing FinSequence of REAL , i, j st i in ( dom p) & j in ( dom p) & i <= j holds (p . i) <= (p . j)

    proof

      let p be non-decreasing FinSequence of REAL ;

      for n be Nat st n in ( dom p) & (n + 1) in ( dom p) holds (p . n) <= (p . (n + 1)) by Def1;

      hence thesis by LM;

    end;

    theorem :: INTEGRA2:3

    for p holds ex q be non-decreasing FinSequence of REAL st (p,q) are_fiberwise_equipotent

    proof

      let p;

      consider q be non-increasing FinSequence of REAL such that

       A1: (p,q) are_fiberwise_equipotent by RFINSEQ: 22;

      for n be Nat st n in ( dom ( Rev q)) & (n + 1) in ( dom ( Rev q)) holds (( Rev q) . n) <= (( Rev q) . (n + 1))

      proof

        let n;

        assume that

         A2: n in ( dom ( Rev q)) and

         A3: (n + 1) in ( dom ( Rev q));

        (( Rev q) . n) <= (( Rev q) . (n + 1))

        proof

          n in ( Seg ( len ( Rev q))) by A2, FINSEQ_1:def 3;

          then 1 <= n by FINSEQ_1: 1;

          then (n - 1) >= 0 by XREAL_1: 48;

          then (( len q) + 0 ) <= (( len q) + (n - 1)) by XREAL_1: 7;

          then

           A4: (( len q) - (n - 1)) <= ( len q) by XREAL_1: 20;

          n in ( Seg ( len ( Rev q))) by A2, FINSEQ_1:def 3;

          then n in ( Seg ( len q)) by FINSEQ_5:def 3;

          then n <= ( len q) by FINSEQ_1: 1;

          then

          consider m be Nat such that

           A5: ( len q) = (n + m) by NAT_1: 10;

          reconsider m as Nat;

          (m + 1) = ((( len q) - n) + 1) & 1 <= ((( len q) - n) + 1) by A5, NAT_1: 11;

          then ((( len q) - n) + 1) in ( Seg ( len q)) by A4, FINSEQ_1: 1;

          then

           A6: ((( len q) - n) + 1) in ( dom q) by FINSEQ_1:def 3;

          set x = (( Rev q) . n), y = (( Rev q) . (n + 1));

          

           A7: ((( len q) - (n + 1)) + 1) = (( len q) - n);

          ( len q) <= (( len q) + n) by NAT_1: 11;

          then

           A8: ((( len q) - (n + 1)) + 1) <= ( len q) by A7, XREAL_1: 20;

          (n + 1) in ( Seg ( len ( Rev q))) by A3, FINSEQ_1:def 3;

          then (n + 1) in ( Seg ( len q)) by FINSEQ_5:def 3;

          then (n + 1) <= ( len q) by FINSEQ_1: 1;

          then 1 <= ((( len q) - (n + 1)) + 1) by A7, XREAL_1: 19;

          then ((( len q) - (n + 1)) + 1) in ( Seg ( len q)) by A5, A8, FINSEQ_1: 1;

          then

           A9: ((( len q) - (n + 1)) + 1) in ( dom q) by FINSEQ_1:def 3;

          x = (q . ((( len q) - n) + 1)) & y = (q . ((( len q) - (n + 1)) + 1)) by A2, A3, FINSEQ_5:def 3;

          hence thesis by A6, A9, RFINSEQ:def 3;

        end;

        hence thesis;

      end;

      then

      reconsider r = ( Rev q) as non-decreasing FinSequence of REAL by Def1;

      take r;

      (p,( Rev q)) are_fiberwise_equipotent

      proof

        defpred P[ Nat] means for p be FinSequence of REAL , q be non-increasing FinSequence of REAL st ( len p) = $1 & (p,q) are_fiberwise_equipotent holds (p,( Rev q)) are_fiberwise_equipotent ;

        

         A10: for k st P[k] holds P[(k + 1)]

        proof

          let k;

          assume

           A11: P[k];

           P[(k + 1)]

          proof

            let p be FinSequence of REAL ;

            let q be non-increasing FinSequence of REAL ;

            consider q1 be non-increasing FinSequence of REAL such that

             A12: (p,q1) are_fiberwise_equipotent by RFINSEQ: 22;

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

            reconsider q1k = (q1 | kk) as non-increasing FinSequence of REAL by RFINSEQ: 20;

            

             A13: ((( Rev q1k) ^ <*(q1 . (k + 1))*>),( <*(q1 . (k + 1))*> ^ ( Rev q1k))) are_fiberwise_equipotent by RFINSEQ: 2;

            assume

             A14: ( len p) = (k + 1);

            then

             A15: ( len q1) = (k + 1) by A12, RFINSEQ: 3;

            ( len p) = ( len q1) by A12, RFINSEQ: 3;

            then ( len (q1 | k)) = k by A14, FINSEQ_1: 59, NAT_1: 11;

            then ((q1 | k),( Rev q1k)) are_fiberwise_equipotent by A11;

            then (((q1 | k) ^ <*(q1 . (k + 1))*>),(( Rev q1k) ^ <*(q1 . (k + 1))*>)) are_fiberwise_equipotent by RFINSEQ: 1;

            then (q1,(( Rev q1k) ^ <*(q1 . (k + 1))*>)) are_fiberwise_equipotent by A15, RFINSEQ: 7;

            then

             A16: (q1,( <*(q1 . (k + 1))*> ^ ( Rev q1k))) are_fiberwise_equipotent by A13, CLASSES1: 76;

            

             A17: ( <*(q1 . (k + 1))*> ^ ( Rev q1k)) = ( Rev ((q1 | k) ^ <*(q1 . (k + 1))*>)) by FINSEQ_5: 63

            .= ( Rev q1) by A15, RFINSEQ: 7;

            assume (p,q) are_fiberwise_equipotent ;

            then q = q1 by A12, CLASSES1: 76, RFINSEQ: 23;

            hence thesis by A12, A16, A17, CLASSES1: 76;

          end;

          hence thesis;

        end;

        

         A18: ( len p) = ( len p);

        

         A19: P[ 0 ]

        proof

          let p be FinSequence of REAL ;

          let q be non-increasing FinSequence of REAL ;

          assume

           A20: ( len p) = 0 ;

          assume (p,q) are_fiberwise_equipotent ;

          then ( len q) = 0 by A20, RFINSEQ: 3;

          then ( len ( Rev q)) = 0 by FINSEQ_5:def 3;

          then ( Rev q) = {} ;

          then

           A21: ( rng ( Rev q)) = {} ;

          p = {} by A20;

          then

           A22: ( rng p) = {} ;

          for x be object holds ( card ( Coim (p,x))) = ( card ( Coim (( Rev q),x)))

          proof

            let x be object;

            ( card (p " {x})) = 0 by A22, CARD_1: 27, FUNCT_1: 72;

            hence thesis by A21, CARD_1: 27, FUNCT_1: 72;

          end;

          hence thesis by CLASSES1:def 10;

        end;

        for k holds P[k] from NAT_1:sch 2( A19, A10);

        hence thesis by A1, A18;

      end;

      hence thesis;

    end;

    theorem :: INTEGRA2:4

    for D be non empty set, f be FinSequence of D, k1,k2,k3 be Nat st 1 <= k1 & k3 <= ( len f) & k1 <= k2 & k2 < k3 holds (( mid (f,k1,k2)) ^ ( mid (f,(k2 + 1),k3))) = ( mid (f,k1,k3))

    proof

      let D be non empty set;

      let f be FinSequence of D;

      let k1,k2,k3 be Nat;

      assume that

       A1: 1 <= k1 and

       A2: k3 <= ( len f) and

       A3: k1 <= k2 and

       A4: k2 < k3;

      

       A5: k2 <= ( len f) by A2, A4, XXREAL_0: 2;

      then

       A6: k1 <= ( len f) by A3, XXREAL_0: 2;

      1 <= k2 & k2 <= ( len f) by A1, A2, A3, A4, XXREAL_0: 2;

      

      then

       A7: ( len ( mid (f,k1,k2))) = ((k2 -' k1) + 1) by A1, A3, A6, FINSEQ_6: 118

      .= ((k2 - k1) + 1) by A3, XREAL_1: 233;

      

       A8: 1 <= k2 by A1, A3, XXREAL_0: 2;

      then

       A9: 1 <= k3 by A4, XXREAL_0: 2;

      

       A10: k1 < k3 by A3, A4, XXREAL_0: 2;

      

       A11: 1 <= (k2 + 1) by A8, NAT_1: 13;

      

       A12: (k2 + 1) <= k3 by A4, NAT_1: 13;

      then (k2 + 1) <= ( len f) by A2, XXREAL_0: 2;

      

      then

       A13: ( len ( mid (f,(k2 + 1),k3))) = ((k3 -' (k2 + 1)) + 1) by A2, A9, A12, A11, FINSEQ_6: 118

      .= ((k3 - (k2 + 1)) + 1) by A12, XREAL_1: 233

      .= (k3 - k2);

      

      then

       A14: ( len (( mid (f,k1,k2)) ^ ( mid (f,(k2 + 1),k3)))) = (((k2 - k1) + 1) + (k3 - k2)) by A7, FINSEQ_1: 22

      .= ((k3 - k1) + 1);

      

       A15: 1 <= (k2 + 1) by A8, NAT_1: 13;

      

       A16: for k be Nat st 1 <= k & k <= ( len (( mid (f,k1,k2)) ^ ( mid (f,(k2 + 1),k3)))) holds ((( mid (f,k1,k2)) ^ ( mid (f,(k2 + 1),k3))) . k) = (( mid (f,k1,k3)) . k)

      proof

        let k be Nat;

        assume

         A17: 1 <= k & k <= ( len (( mid (f,k1,k2)) ^ ( mid (f,(k2 + 1),k3))));

        then k in ( Seg ( len (( mid (f,k1,k2)) ^ ( mid (f,(k2 + 1),k3))))) by FINSEQ_1: 1;

        then

         A18: k in ( dom (( mid (f,k1,k2)) ^ ( mid (f,(k2 + 1),k3)))) by FINSEQ_1:def 3;

        now

          per cases by A18, FINSEQ_1: 25;

            suppose

             A19: k in ( dom ( mid (f,k1,k2)));

            then

             A20: k in ( Seg ( len ( mid (f,k1,k2)))) by FINSEQ_1:def 3;

            then

             A21: 1 <= k by FINSEQ_1: 1;

            

             A22: k <= ((k2 - k1) + 1) by A7, A20, FINSEQ_1: 1;

            (k2 - k1) <= (k3 - k1) by A4, XREAL_1: 9;

            then ((k2 - k1) + 1) <= ((k3 - k1) + 1) by XREAL_1: 6;

            then

             A23: k <= ((k3 - k1) + 1) by A22, XXREAL_0: 2;

            ((( mid (f,k1,k2)) ^ ( mid (f,(k2 + 1),k3))) . k) = (( mid (f,k1,k2)) . k) by A19, FINSEQ_1:def 7

            .= (f . ((k - 1) + k1)) by A1, A3, A5, A21, A22, FINSEQ_6: 122;

            hence thesis by A1, A2, A10, A21, A23, FINSEQ_6: 122;

          end;

            suppose ex n be Nat st n in ( dom ( mid (f,(k2 + 1),k3))) & k = (( len ( mid (f,k1,k2))) + n);

            then

            consider n be Nat such that

             A24: n in ( dom ( mid (f,(k2 + 1),k3))) and

             A25: k = (( len ( mid (f,k1,k2))) + n);

            

             A26: (( mid (f,k1,k3)) . k) = (f . ((((k2 - (k1 - 1)) + n) + k1) - 1)) by A1, A2, A10, A7, A14, A17, A25, FINSEQ_6: 122

            .= (f . (n + k2));

            n in ( Seg ( len ( mid (f,(k2 + 1),k3)))) by A24, FINSEQ_1:def 3;

            then

             A27: 1 <= n & n <= ((k3 - (k2 + 1)) + 1) by A13, FINSEQ_1: 1;

            ((( mid (f,k1,k2)) ^ ( mid (f,(k2 + 1),k3))) . k) = (( mid (f,(k2 + 1),k3)) . n) by A24, A25, FINSEQ_1:def 7

            .= (f . ((n + (k2 + 1)) - 1)) by A2, A15, A12, A27, FINSEQ_6: 122

            .= (f . ((n + k2) + 0 ));

            hence thesis by A26;

          end;

        end;

        hence thesis;

      end;

      ( len ( mid (f,k1,k3))) = ((k3 -' k1) + 1) by A1, A2, A6, A9, A10, FINSEQ_6: 118

      .= ((k3 - k1) + 1) by A3, A4, XREAL_1: 233, XXREAL_0: 2;

      hence thesis by A14, A16, FINSEQ_1: 14;

    end;

    begin

    definition

      let A be real-membered set;

      let x be Real;

      :: original: **

      redefine

      func x ** A -> Subset of REAL ;

      coherence by MEMBERED: 3;

    end

    theorem :: INTEGRA2:5

    for X,Y be non empty set, f be PartFunc of X, REAL st (f | X) is bounded_above & Y c= X holds ((f | Y) | Y) is bounded_above

    proof

      let X,Y be non empty set;

      let f be PartFunc of X, REAL ;

      assume (f | X) is bounded_above;

      then

      consider a be Real such that

       A1: for x be object st x in (X /\ ( dom f)) holds a >= (f . x) by RFUNCT_1: 70;

      assume

       A2: Y c= X;

      for x be object st x in (Y /\ ( dom (f | Y))) holds a >= ((f | Y) . x)

      proof

        let x be object;

        

         A3: (( dom f) /\ Y) c= (( dom f) /\ X) by A2, XBOOLE_1: 26;

        assume x in (Y /\ ( dom (f | Y)));

        then

         A4: x in ( dom (f | Y)) by XBOOLE_0:def 4;

        then x in (( dom f) /\ Y) by RELAT_1: 61;

        then a >= (f . x) by A1, A3;

        hence thesis by A4, FUNCT_1: 47;

      end;

      hence thesis by RFUNCT_1: 70;

    end;

    theorem :: INTEGRA2:6

    for X,Y be non empty set, f be PartFunc of X, REAL st (f | X) is bounded_below & Y c= X holds ((f | Y) | Y) is bounded_below

    proof

      let X,Y be non empty set;

      let f be PartFunc of X, REAL ;

      assume (f | X) is bounded_below;

      then

      consider a be Real such that

       A1: for x be object st x in (X /\ ( dom f)) holds (f . x) >= a by RFUNCT_1: 71;

      assume

       A2: Y c= X;

      for x be object st x in (Y /\ ( dom (f | Y))) holds ((f | Y) . x) >= a

      proof

        let x be object;

        

         A3: (( dom f) /\ Y) c= (( dom f) /\ X) by A2, XBOOLE_1: 26;

        assume x in (Y /\ ( dom (f | Y)));

        then

         A4: x in ( dom (f | Y)) by XBOOLE_0:def 4;

        then x in (( dom f) /\ Y) by RELAT_1: 61;

        then a <= (f . x) by A1, A3;

        hence thesis by A4, FUNCT_1: 47;

      end;

      hence thesis by RFUNCT_1: 71;

    end;

    theorem :: INTEGRA2:7

    for X be real-membered set, a be Real holds X is empty iff (a ** X) is empty;

    theorem :: INTEGRA2:8

    

     Th8: for X be Subset of REAL holds (r ** X) = { (r * x) : x in X }

    proof

      let X be Subset of REAL ;

      thus (r ** X) c= { (r * x) : x in X }

      proof

        let y be object;

        assume y in (r ** X);

        then

        consider z be Element of ExtREAL such that

         A1: y = (r * z) & z in X by MEMBER_1: 188;

        reconsider z1 = z as Element of REAL by A1;

        y = (r * z1) by A1, XXREAL_3:def 5;

        hence thesis by A1;

      end;

      let y be object;

      assume y in { (r * x) : x in X };

      then

      consider z be Real such that

       A2: y = (r * z) & z in X;

      thus thesis by A2, MEMBER_1: 193;

    end;

    theorem :: INTEGRA2:9

    for X be non empty Subset of REAL st X is bounded_above & 0 <= r holds (r ** X) is bounded_above

    proof

      let X be non empty Subset of REAL ;

      assume that

       A1: X is bounded_above and

       A2: 0 <= r;

      consider b be Real such that

       A3: b is UpperBound of X by A1;

      

       A4: for x be Real st x in X holds x <= b by A3, XXREAL_2:def 1;

      (r * b) is UpperBound of (r ** X)

      proof

        let y be ExtReal;

        assume y in (r ** X);

        then y in { (r * x) : x in X } by Th8;

        then

        consider x such that

         A5: y = (r * x) and

         A6: x in X;

        x <= b by A4, A6;

        hence thesis by A2, A5, XREAL_1: 64;

      end;

      hence thesis;

    end;

    theorem :: INTEGRA2:10

    for X be non empty Subset of REAL st X is bounded_above & r <= 0 holds (r ** X) is bounded_below

    proof

      let X be non empty Subset of REAL ;

      assume that

       A1: X is bounded_above and

       A2: r <= 0 ;

      consider b be Real such that

       A3: b is UpperBound of X by A1;

      

       A4: for x be Real st x in X holds x <= b by A3, XXREAL_2:def 1;

      (r * b) is LowerBound of (r ** X)

      proof

        let y be ExtReal;

        assume y in (r ** X);

        then y in { (r * x) : x in X } by Th8;

        then ex x st y = (r * x) & x in X;

        hence thesis by A2, A4, XREAL_1: 65;

      end;

      hence thesis;

    end;

    theorem :: INTEGRA2:11

    for X be non empty Subset of REAL st X is bounded_below & 0 <= r holds (r ** X) is bounded_below

    proof

      let X be non empty Subset of REAL ;

      assume that

       A1: X is bounded_below and

       A2: 0 <= r;

      consider b be Real such that

       A3: b is LowerBound of X by A1;

      

       A4: for x be Real st x in X holds b <= x by A3, XXREAL_2:def 2;

      (r * b) is LowerBound of (r ** X)

      proof

        let y be ExtReal;

        assume y in (r ** X);

        then y in { (r * x) : x in X } by Th8;

        then ex x st y = (r * x) & x in X;

        hence thesis by A2, A4, XREAL_1: 64;

      end;

      hence thesis;

    end;

    theorem :: INTEGRA2:12

    for X be non empty Subset of REAL st X is bounded_below & r <= 0 holds (r ** X) is bounded_above

    proof

      let X be non empty Subset of REAL ;

      assume that

       A1: X is bounded_below and

       A2: r <= 0 ;

      consider b be Real such that

       A3: b is LowerBound of X by A1;

      

       A4: for x be Real st x in X holds b <= x by A3, XXREAL_2:def 2;

      (r * b) is UpperBound of (r ** X)

      proof

        let y be ExtReal;

        assume y in (r ** X);

        then y in { (r * x) : x in X } by Th8;

        then

        consider x such that

         A5: y = (r * x) and

         A6: x in X;

        b <= x by A4, A6;

        hence thesis by A2, A5, XREAL_1: 65;

      end;

      hence thesis;

    end;

    theorem :: INTEGRA2:13

    

     Th13: for X be non empty Subset of REAL st X is bounded_above & 0 <= r holds ( upper_bound (r ** X)) = (r * ( upper_bound X))

    proof

      let X be non empty Subset of REAL ;

      assume that

       A1: X is bounded_above and

       A2: 0 <= r;

      

       A3: for a be Real st a in (r ** X) holds a <= (r * ( upper_bound X))

      proof

        let a be Real;

        assume a in (r ** X);

        then a in { (r * x) : x in X } by Th8;

        then

        consider x such that

         A4: a = (r * x) and

         A5: x in X;

        x <= ( upper_bound X) by A1, A5, SEQ_4:def 1;

        hence thesis by A2, A4, XREAL_1: 64;

      end;

      for b be Real st for a be Real st a in (r ** X) holds a <= b holds (r * ( upper_bound X)) <= b

      proof

        consider x be Element of REAL such that

         A6: x in X by SUBSET_1: 4;

        let b be Real;

        assume

         A7: for a be Real st a in (r ** X) holds a <= b;

        reconsider x as Real;

        (r * x) in { (r * y) : y in X } by A6;

        then

         A8: (r * x) in (r ** X) by Th8;

        now

          per cases by A2;

            suppose r = 0 ;

            hence thesis by A7, A8;

          end;

            suppose

             A9: r > 0 ;

            for z be Real st z in X holds z <= (b / r)

            proof

              let z be Real;

              assume z in X;

              then (r * z) in { (r * y) : y in X };

              then (r * z) in (r ** X) by Th8;

              hence thesis by A7, A9, XREAL_1: 77;

            end;

            then ( upper_bound X) <= (b / r) by SEQ_4: 45;

            then (r * ( upper_bound X)) <= ((b / r) * r) by A9, XREAL_1: 64;

            hence thesis by A9, XCMPLX_1: 87;

          end;

        end;

        hence thesis;

      end;

      hence thesis by A3, SEQ_4: 46;

    end;

    theorem :: INTEGRA2:14

    

     Th14: for X be non empty Subset of REAL st X is bounded_above & r <= 0 holds ( lower_bound (r ** X)) = (r * ( upper_bound X))

    proof

      let X be non empty Subset of REAL ;

      assume that

       A1: X is bounded_above and

       A2: r <= 0 ;

      

       A3: for a be Real st a in (r ** X) holds (r * ( upper_bound X)) <= a

      proof

        let a be Real;

        assume a in (r ** X);

        then a in { (r * x) : x in X } by Th8;

        then

        consider x such that

         A4: a = (r * x) and

         A5: x in X;

        x <= ( upper_bound X) by A1, A5, SEQ_4:def 1;

        hence thesis by A2, A4, XREAL_1: 65;

      end;

      for b be Real st for a be Real st a in (r ** X) holds a >= b holds (r * ( upper_bound X)) >= b

      proof

        consider x be Element of REAL such that

         A6: x in X by SUBSET_1: 4;

        let b be Real;

        assume

         A7: for a be Real st a in (r ** X) holds a >= b;

        reconsider x as Real;

        (r * x) in { (r * y) : y in X } by A6;

        then

         A8: (r * x) in (r ** X) by Th8;

        now

          per cases by A2;

            suppose r = 0 ;

            hence thesis by A7, A8;

          end;

            suppose

             A9: r < 0 ;

            for z be Real st z in X holds z <= (b / r)

            proof

              let z be Real;

              assume z in X;

              then (r * z) in { (r * y) : y in X };

              then (r * z) in (r ** X) by Th8;

              hence thesis by A7, A9, XREAL_1: 80;

            end;

            then ( upper_bound X) <= (b / r) by SEQ_4: 45;

            then (r * ( upper_bound X)) >= ((b / r) * r) by A9, XREAL_1: 65;

            hence thesis by A9, XCMPLX_1: 87;

          end;

        end;

        hence thesis;

      end;

      hence thesis by A3, SEQ_4: 44;

    end;

    theorem :: INTEGRA2:15

    

     Th15: for X be non empty Subset of REAL st X is bounded_below & 0 <= r holds ( lower_bound (r ** X)) = (r * ( lower_bound X))

    proof

      let X be non empty Subset of REAL ;

      assume that

       A1: X is bounded_below and

       A2: 0 <= r;

      

       A3: for a be Real st a in (r ** X) holds (r * ( lower_bound X)) <= a

      proof

        let a be Real;

        assume a in (r ** X);

        then a in { (r * x) : x in X } by Th8;

        then

        consider x such that

         A4: a = (r * x) and

         A5: x in X;

        ( lower_bound X) <= x by A1, A5, SEQ_4:def 2;

        hence thesis by A2, A4, XREAL_1: 64;

      end;

      for b be Real st for a be Real st a in (r ** X) holds a >= b holds (r * ( lower_bound X)) >= b

      proof

        consider x be Element of REAL such that

         A6: x in X by SUBSET_1: 4;

        let b be Real;

        assume

         A7: for a be Real st a in (r ** X) holds a >= b;

        reconsider x as Real;

        (r * x) in { (r * y) : y in X } by A6;

        then

         A8: (r * x) in (r ** X) by Th8;

        now

          per cases by A2;

            suppose r = 0 ;

            hence thesis by A7, A8;

          end;

            suppose

             A9: r > 0 ;

            for z be Real st z in X holds z >= (b / r)

            proof

              let z be Real;

              assume z in X;

              then (r * z) in { (r * y) : y in X };

              then (r * z) in (r ** X) by Th8;

              hence thesis by A7, A9, XREAL_1: 79;

            end;

            then ( lower_bound X) >= (b / r) by SEQ_4: 43;

            then (r * ( lower_bound X)) >= ((b / r) * r) by A9, XREAL_1: 64;

            hence thesis by A9, XCMPLX_1: 87;

          end;

        end;

        hence thesis;

      end;

      hence thesis by A3, SEQ_4: 44;

    end;

    theorem :: INTEGRA2:16

    

     Th16: for X be non empty Subset of REAL st X is bounded_below & r <= 0 holds ( upper_bound (r ** X)) = (r * ( lower_bound X))

    proof

      let X be non empty Subset of REAL ;

      assume that

       A1: X is bounded_below and

       A2: r <= 0 ;

      

       A3: for a be Real st a in (r ** X) holds (r * ( lower_bound X)) >= a

      proof

        let a be Real;

        assume a in (r ** X);

        then a in { (r * x) : x in X } by Th8;

        then

        consider x such that

         A4: a = (r * x) and

         A5: x in X;

        ( lower_bound X) <= x by A1, A5, SEQ_4:def 2;

        hence thesis by A2, A4, XREAL_1: 65;

      end;

      for b be Real st for a be Real st a in (r ** X) holds a <= b holds (r * ( lower_bound X)) <= b

      proof

        consider x be Element of REAL such that

         A6: x in X by SUBSET_1: 4;

        let b be Real;

        assume

         A7: for a be Real st a in (r ** X) holds a <= b;

        reconsider x as Real;

        (r * x) in { (r * y) : y in X } by A6;

        then

         A8: (r * x) in (r ** X) by Th8;

        now

          per cases by A2;

            suppose r = 0 ;

            hence thesis by A7, A8;

          end;

            suppose

             A9: r < 0 ;

            for z be Real st z in X holds z >= (b / r)

            proof

              let z be Real;

              assume z in X;

              then (r * z) in { (r * y) : y in X };

              then (r * z) in (r ** X) by Th8;

              hence thesis by A7, A9, XREAL_1: 78;

            end;

            then ( lower_bound X) >= (b / r) by SEQ_4: 43;

            then (r * ( lower_bound X)) <= ((b / r) * r) by A9, XREAL_1: 65;

            hence thesis by A9, XCMPLX_1: 87;

          end;

        end;

        hence thesis;

      end;

      hence thesis by A3, SEQ_4: 46;

    end;

    begin

    theorem :: INTEGRA2:17

    

     Th17: for X be non empty set, f be Function of X, REAL holds ( rng (r (#) f)) = (r ** ( rng f))

    proof

      let X be non empty set;

      let f be Function of X, REAL ;

      for y be Element of REAL holds y in (r ** ( rng f)) implies y in ( rng (r (#) f))

      proof

        let y be Element of REAL ;

        assume y in (r ** ( rng f));

        then y in { (r * b) : b in ( rng f) } by Th8;

        then

        consider b such that

         A1: y = (r * b) and

         A2: b in ( rng f);

        consider x be Element of X such that

         A3: x in ( dom f) and

         A4: b = (f . x) by A2, PARTFUN1: 3;

        x in ( dom (r (#) f)) by A3, VALUED_1:def 5;

        then ((r (#) f) . x) in ( rng (r (#) f)) by FUNCT_1:def 3;

        hence thesis by A1, A4, RFUNCT_1: 57;

      end;

      then

       A5: (r ** ( rng f)) c= ( rng (r (#) f));

      for y be Element of REAL holds y in ( rng (r (#) f)) implies y in (r ** ( rng f))

      proof

        let y be Element of REAL ;

        assume y in ( rng (r (#) f));

        then

        consider x be Element of X such that

         A6: x in ( dom (r (#) f)) and

         A7: y = ((r (#) f) . x) by PARTFUN1: 3;

        x in ( dom f) by A6, VALUED_1:def 5;

        then

         A8: (f . x) in ( rng f) by FUNCT_1:def 3;

        reconsider fx = (f . x) as Real;

        y = (r * fx) by A7, RFUNCT_1: 57;

        then y in { (r * b) : b in ( rng f) } by A8;

        hence thesis by Th8;

      end;

      then ( rng (r (#) f)) c= (r ** ( rng f));

      hence thesis by A5;

    end;

    theorem :: INTEGRA2:18

    

     Th18: for X,Z be non empty set, f be PartFunc of X, REAL holds ( rng (r (#) (f | Z))) = (r ** ( rng (f | Z)))

    proof

      let X,Z be non empty set;

      let f be PartFunc of X, REAL ;

      for y be Element of REAL holds y in (r ** ( rng (f | Z))) implies y in ( rng (r (#) (f | Z)))

      proof

        let y be Element of REAL ;

        assume y in (r ** ( rng (f | Z)));

        then y in { (r * b) : b in ( rng (f | Z)) } by Th8;

        then

        consider b such that

         A1: y = (r * b) and

         A2: b in ( rng (f | Z));

        consider x be Element of X such that

         A3: x in ( dom (f | Z)) and

         A4: b = ((f | Z) . x) by A2, PARTFUN1: 3;

        

         A5: x in ( dom (r (#) (f | Z))) by A3, VALUED_1:def 5;

        then y = ((r (#) (f | Z)) . x) by A1, A4, VALUED_1:def 5;

        hence thesis by A5, FUNCT_1:def 3;

      end;

      then

       A6: (r ** ( rng (f | Z))) c= ( rng (r (#) (f | Z)));

      for y be Element of REAL holds y in ( rng (r (#) (f | Z))) implies y in (r ** ( rng (f | Z)))

      proof

        let y be Element of REAL ;

        assume y in ( rng (r (#) (f | Z)));

        then

        consider x be Element of X such that

         A7: x in ( dom (r (#) (f | Z))) and

         A8: y = ((r (#) (f | Z)) . x) by PARTFUN1: 3;

        x in ( dom (f | Z)) by A7, VALUED_1:def 5;

        then

         A9: ((f | Z) . x) in ( rng (f | Z)) by FUNCT_1:def 3;

        reconsider fx = ((f | Z) . x) as Real;

        y = (r * fx) by A7, A8, VALUED_1:def 5;

        then y in { (r * b) : b in ( rng (f | Z)) } by A9;

        hence thesis by Th8;

      end;

      then ( rng (r (#) (f | Z))) c= (r ** ( rng (f | Z)));

      hence thesis by A6;

    end;

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

    reserve f,g for Function of A, REAL ;

    reserve D,D1,D2 for Division of A;

    theorem :: INTEGRA2:19

    

     Th19: (f | A) is bounded & r >= 0 implies (( upper_sum_set (r (#) f)) . D) >= ((r * ( lower_bound ( rng f))) * ( vol A))

    proof

      assume that

       A1: (f | A) is bounded and

       A2: r >= 0 ;

      

       A3: ( rng f) is bounded_below by A1, INTEGRA1: 11;

      

       A4: ((r (#) f) | A) is bounded by A1, RFUNCT_1: 80;

      then

       A5: ( lower_sum ((r (#) f),D)) >= (( lower_bound ( rng (r (#) f))) * ( vol A)) by INTEGRA1: 25;

      (( upper_sum_set (r (#) f)) . D) = ( upper_sum ((r (#) f),D)) by INTEGRA1:def 10;

      then

       A6: (( upper_sum_set (r (#) f)) . D) >= ( lower_sum ((r (#) f),D)) by A4, INTEGRA1: 28;

      ( lower_bound ( rng (r (#) f))) = ( lower_bound (r ** ( rng f))) by Th17

      .= (r * ( lower_bound ( rng f))) by A2, A3, Th15;

      hence thesis by A6, A5, XXREAL_0: 2;

    end;

    theorem :: INTEGRA2:20

    

     Th20: (f | A) is bounded & r <= 0 implies (( upper_sum_set (r (#) f)) . D) >= ((r * ( upper_bound ( rng f))) * ( vol A))

    proof

      assume that

       A1: (f | A) is bounded and

       A2: r <= 0 ;

      

       A3: ( rng f) is bounded_above by A1, INTEGRA1: 13;

      

       A4: ((r (#) f) | A) is bounded by A1, RFUNCT_1: 80;

      then

       A5: ( lower_sum ((r (#) f),D)) >= (( lower_bound ( rng (r (#) f))) * ( vol A)) by INTEGRA1: 25;

      (( upper_sum_set (r (#) f)) . D) = ( upper_sum ((r (#) f),D)) by INTEGRA1:def 10;

      then

       A6: (( upper_sum_set (r (#) f)) . D) >= ( lower_sum ((r (#) f),D)) by A4, INTEGRA1: 28;

      ( lower_bound ( rng (r (#) f))) = ( lower_bound (r ** ( rng f))) by Th17

      .= (r * ( upper_bound ( rng f))) by A2, A3, Th14;

      hence thesis by A6, A5, XXREAL_0: 2;

    end;

    theorem :: INTEGRA2:21

    

     Th21: (f | A) is bounded & r >= 0 implies (( lower_sum_set (r (#) f)) . D) <= ((r * ( upper_bound ( rng f))) * ( vol A))

    proof

      assume that

       A1: (f | A) is bounded and

       A2: r >= 0 ;

      

       A3: ( rng f) is bounded_above by A1, INTEGRA1: 13;

      

       A4: ((r (#) f) | A) is bounded by A1, RFUNCT_1: 80;

      then

       A5: ( upper_sum ((r (#) f),D)) <= (( upper_bound ( rng (r (#) f))) * ( vol A)) by INTEGRA1: 27;

      (( lower_sum_set (r (#) f)) . D) = ( lower_sum ((r (#) f),D)) by INTEGRA1:def 11;

      then

       A6: (( lower_sum_set (r (#) f)) . D) <= ( upper_sum ((r (#) f),D)) by A4, INTEGRA1: 28;

      ( upper_bound ( rng (r (#) f))) = ( upper_bound (r ** ( rng f))) by Th17

      .= (r * ( upper_bound ( rng f))) by A2, A3, Th13;

      hence thesis by A6, A5, XXREAL_0: 2;

    end;

    theorem :: INTEGRA2:22

    

     Th22: (f | A) is bounded & r <= 0 implies (( lower_sum_set (r (#) f)) . D) <= ((r * ( lower_bound ( rng f))) * ( vol A))

    proof

      assume that

       A1: (f | A) is bounded and

       A2: r <= 0 ;

      

       A3: ( rng f) is bounded_below by A1, INTEGRA1: 11;

      

       A4: ((r (#) f) | A) is bounded by A1, RFUNCT_1: 80;

      then

       A5: ( upper_sum ((r (#) f),D)) <= (( upper_bound ( rng (r (#) f))) * ( vol A)) by INTEGRA1: 27;

      (( lower_sum_set (r (#) f)) . D) = ( lower_sum ((r (#) f),D)) by INTEGRA1:def 11;

      then

       A6: (( lower_sum_set (r (#) f)) . D) <= ( upper_sum ((r (#) f),D)) by A4, INTEGRA1: 28;

      ( upper_bound ( rng (r (#) f))) = ( upper_bound (r ** ( rng f))) by Th17

      .= (r * ( lower_bound ( rng f))) by A2, A3, Th16;

      hence thesis by A6, A5, XXREAL_0: 2;

    end;

    theorem :: INTEGRA2:23

    

     Th23: i in ( dom D) & (f | A) is bounded_above & r >= 0 implies (( upper_volume ((r (#) f),D)) . i) = (r * (( upper_volume (f,D)) . i))

    proof

      assume that

       A1: i in ( dom D) and

       A2: (f | A) is bounded_above and

       A3: r >= 0 ;

      ( dom (f | ( divset (D,i)))) = (( dom f) /\ ( divset (D,i))) by RELAT_1: 61

      .= (A /\ ( divset (D,i))) by FUNCT_2:def 1

      .= ( divset (D,i)) by A1, INTEGRA1: 8, XBOOLE_1: 28;

      then

       A4: ( rng (f | ( divset (D,i)))) is non empty by RELAT_1: 42;

      ( rng f) is bounded_above by A2, INTEGRA1: 13;

      then

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

      (( upper_volume ((r (#) f),D)) . i) = (( upper_bound ( rng ((r (#) f) | ( divset (D,i))))) * ( vol ( divset (D,i)))) by A1, INTEGRA1:def 6

      .= (( upper_bound ( rng (r (#) (f | ( divset (D,i)))))) * ( vol ( divset (D,i)))) by RFUNCT_1: 49

      .= (( upper_bound (r ** ( rng (f | ( divset (D,i)))))) * ( vol ( divset (D,i)))) by Th18

      .= ((r * ( upper_bound ( rng (f | ( divset (D,i)))))) * ( vol ( divset (D,i)))) by A3, A4, A5, Th13

      .= (r * (( upper_bound ( rng (f | ( divset (D,i))))) * ( vol ( divset (D,i)))))

      .= (r * (( upper_volume (f,D)) . i)) by A1, INTEGRA1:def 6;

      hence thesis;

    end;

    theorem :: INTEGRA2:24

    

     Th24: i in ( dom D) & (f | A) is bounded_above & r <= 0 implies (( lower_volume ((r (#) f),D)) . i) = (r * (( upper_volume (f,D)) . i))

    proof

      assume that

       A1: i in ( dom D) and

       A2: (f | A) is bounded_above and

       A3: r <= 0 ;

      ( dom (f | ( divset (D,i)))) = (( dom f) /\ ( divset (D,i))) by RELAT_1: 61

      .= (A /\ ( divset (D,i))) by FUNCT_2:def 1

      .= ( divset (D,i)) by A1, INTEGRA1: 8, XBOOLE_1: 28;

      then

       A4: ( rng (f | ( divset (D,i)))) is non empty by RELAT_1: 42;

      ( rng f) is bounded_above by A2, INTEGRA1: 13;

      then

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

      (( lower_volume ((r (#) f),D)) . i) = (( lower_bound ( rng ((r (#) f) | ( divset (D,i))))) * ( vol ( divset (D,i)))) by A1, INTEGRA1:def 7

      .= (( lower_bound ( rng (r (#) (f | ( divset (D,i)))))) * ( vol ( divset (D,i)))) by RFUNCT_1: 49

      .= (( lower_bound (r ** ( rng (f | ( divset (D,i)))))) * ( vol ( divset (D,i)))) by Th18

      .= ((r * ( upper_bound ( rng (f | ( divset (D,i)))))) * ( vol ( divset (D,i)))) by A3, A4, A5, Th14

      .= (r * (( upper_bound ( rng (f | ( divset (D,i))))) * ( vol ( divset (D,i)))))

      .= (r * (( upper_volume (f,D)) . i)) by A1, INTEGRA1:def 6;

      hence thesis;

    end;

    theorem :: INTEGRA2:25

    

     Th25: i in ( dom D) & (f | A) is bounded_below & r >= 0 implies (( lower_volume ((r (#) f),D)) . i) = (r * (( lower_volume (f,D)) . i))

    proof

      assume that

       A1: i in ( dom D) and

       A2: (f | A) is bounded_below and

       A3: r >= 0 ;

      ( dom (f | ( divset (D,i)))) = (( dom f) /\ ( divset (D,i))) by RELAT_1: 61

      .= (A /\ ( divset (D,i))) by FUNCT_2:def 1

      .= ( divset (D,i)) by A1, INTEGRA1: 8, XBOOLE_1: 28;

      then

       A4: ( rng (f | ( divset (D,i)))) is non empty by RELAT_1: 42;

      ( rng f) is bounded_below by A2, INTEGRA1: 11;

      then

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

      (( lower_volume ((r (#) f),D)) . i) = (( lower_bound ( rng ((r (#) f) | ( divset (D,i))))) * ( vol ( divset (D,i)))) by A1, INTEGRA1:def 7

      .= (( lower_bound ( rng (r (#) (f | ( divset (D,i)))))) * ( vol ( divset (D,i)))) by RFUNCT_1: 49

      .= (( lower_bound (r ** ( rng (f | ( divset (D,i)))))) * ( vol ( divset (D,i)))) by Th18

      .= ((r * ( lower_bound ( rng (f | ( divset (D,i)))))) * ( vol ( divset (D,i)))) by A3, A4, A5, Th15

      .= (r * (( lower_bound ( rng (f | ( divset (D,i))))) * ( vol ( divset (D,i)))))

      .= (r * (( lower_volume (f,D)) . i)) by A1, INTEGRA1:def 7;

      hence thesis;

    end;

    theorem :: INTEGRA2:26

    

     Th26: i in ( dom D) & (f | A) is bounded_below & r <= 0 implies (( upper_volume ((r (#) f),D)) . i) = (r * (( lower_volume (f,D)) . i))

    proof

      assume that

       A1: i in ( dom D) and

       A2: (f | A) is bounded_below and

       A3: r <= 0 ;

      ( dom (f | ( divset (D,i)))) = (( dom f) /\ ( divset (D,i))) by RELAT_1: 61

      .= (A /\ ( divset (D,i))) by FUNCT_2:def 1

      .= ( divset (D,i)) by A1, INTEGRA1: 8, XBOOLE_1: 28;

      then

       A4: ( rng (f | ( divset (D,i)))) is non empty by RELAT_1: 42;

      ( rng f) is bounded_below by A2, INTEGRA1: 11;

      then

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

      (( upper_volume ((r (#) f),D)) . i) = (( upper_bound ( rng ((r (#) f) | ( divset (D,i))))) * ( vol ( divset (D,i)))) by A1, INTEGRA1:def 6

      .= (( upper_bound ( rng (r (#) (f | ( divset (D,i)))))) * ( vol ( divset (D,i)))) by RFUNCT_1: 49

      .= (( upper_bound (r ** ( rng (f | ( divset (D,i)))))) * ( vol ( divset (D,i)))) by Th18

      .= ((r * ( lower_bound ( rng (f | ( divset (D,i)))))) * ( vol ( divset (D,i)))) by A3, A4, A5, Th16

      .= (r * (( lower_bound ( rng (f | ( divset (D,i))))) * ( vol ( divset (D,i)))))

      .= (r * (( lower_volume (f,D)) . i)) by A1, INTEGRA1:def 7;

      hence thesis;

    end;

    theorem :: INTEGRA2:27

    

     Th27: (f | A) is bounded_above & r >= 0 implies ( upper_sum ((r (#) f),D)) = (r * ( upper_sum (f,D)))

    proof

      assume

       A1: (f | A) is bounded_above & r >= 0 ;

      

       A2: for i be Nat st 1 <= i & i <= ( len ( upper_volume ((r (#) f),D))) holds (( upper_volume ((r (#) f),D)) . i) = ((r * ( upper_volume (f,D))) . i)

      proof

        let i be Nat;

        assume

         A3: 1 <= i & i <= ( len ( upper_volume ((r (#) f),D)));

        ( len D) = ( len ( upper_volume ((r (#) f),D))) by INTEGRA1:def 6;

        then i in ( dom D) by A3, FINSEQ_3: 25;

        

        then (( upper_volume ((r (#) f),D)) . i) = (r * (( upper_volume (f,D)) . i)) by A1, Th23

        .= ((r * ( upper_volume (f,D))) . i) by RVSUM_1: 44;

        hence thesis;

      end;

      ( len ( upper_volume ((r (#) f),D))) = ( len D) by INTEGRA1:def 6

      .= ( len ( upper_volume (f,D))) by INTEGRA1:def 6

      .= ( len (r * ( upper_volume (f,D)))) by NEWTON: 2;

      then ( upper_volume ((r (#) f),D)) = (r * ( upper_volume (f,D))) by A2, FINSEQ_1: 14;

      

      then ( upper_sum ((r (#) f),D)) = ( Sum (r * ( upper_volume (f,D)))) by INTEGRA1:def 8

      .= (r * ( Sum ( upper_volume (f,D)))) by RVSUM_1: 87

      .= (r * ( upper_sum (f,D))) by INTEGRA1:def 8;

      hence thesis;

    end;

    theorem :: INTEGRA2:28

    

     Th28: (f | A) is bounded_above & r <= 0 implies ( lower_sum ((r (#) f),D)) = (r * ( upper_sum (f,D)))

    proof

      assume

       A1: (f | A) is bounded_above & r <= 0 ;

      

       A2: for i be Nat st 1 <= i & i <= ( len ( lower_volume ((r (#) f),D))) holds (( lower_volume ((r (#) f),D)) . i) = ((r * ( upper_volume (f,D))) . i)

      proof

        let i be Nat;

        assume

         A3: 1 <= i & i <= ( len ( lower_volume ((r (#) f),D)));

        ( len D) = ( len ( lower_volume ((r (#) f),D))) by INTEGRA1:def 7;

        then i in ( dom D) by A3, FINSEQ_3: 25;

        

        then (( lower_volume ((r (#) f),D)) . i) = (r * (( upper_volume (f,D)) . i)) by A1, Th24

        .= ((r * ( upper_volume (f,D))) . i) by RVSUM_1: 44;

        hence thesis;

      end;

      ( len ( lower_volume ((r (#) f),D))) = ( len D) by INTEGRA1:def 7

      .= ( len ( upper_volume (f,D))) by INTEGRA1:def 6

      .= ( len (r * ( upper_volume (f,D)))) by NEWTON: 2;

      then ( lower_volume ((r (#) f),D)) = (r * ( upper_volume (f,D))) by A2, FINSEQ_1: 14;

      

      then ( lower_sum ((r (#) f),D)) = ( Sum (r * ( upper_volume (f,D)))) by INTEGRA1:def 9

      .= (r * ( Sum ( upper_volume (f,D)))) by RVSUM_1: 87

      .= (r * ( upper_sum (f,D))) by INTEGRA1:def 8;

      hence thesis;

    end;

    theorem :: INTEGRA2:29

    

     Th29: (f | A) is bounded_below & r >= 0 implies ( lower_sum ((r (#) f),D)) = (r * ( lower_sum (f,D)))

    proof

      assume

       A1: (f | A) is bounded_below & r >= 0 ;

      

       A2: for i be Nat st 1 <= i & i <= ( len ( lower_volume ((r (#) f),D))) holds (( lower_volume ((r (#) f),D)) . i) = ((r * ( lower_volume (f,D))) . i)

      proof

        let i be Nat;

        assume

         A3: 1 <= i & i <= ( len ( lower_volume ((r (#) f),D)));

        ( len D) = ( len ( lower_volume ((r (#) f),D))) by INTEGRA1:def 7;

        then i in ( dom D) by A3, FINSEQ_3: 25;

        

        then (( lower_volume ((r (#) f),D)) . i) = (r * (( lower_volume (f,D)) . i)) by A1, Th25

        .= ((r * ( lower_volume (f,D))) . i) by RVSUM_1: 44;

        hence thesis;

      end;

      ( len ( lower_volume ((r (#) f),D))) = ( len D) by INTEGRA1:def 7

      .= ( len ( lower_volume (f,D))) by INTEGRA1:def 7

      .= ( len (r * ( lower_volume (f,D)))) by NEWTON: 2;

      then ( lower_volume ((r (#) f),D)) = (r * ( lower_volume (f,D))) by A2, FINSEQ_1: 14;

      

      then ( lower_sum ((r (#) f),D)) = ( Sum (r * ( lower_volume (f,D)))) by INTEGRA1:def 9

      .= (r * ( Sum ( lower_volume (f,D)))) by RVSUM_1: 87

      .= (r * ( lower_sum (f,D))) by INTEGRA1:def 9;

      hence thesis;

    end;

    theorem :: INTEGRA2:30

    

     Th30: (f | A) is bounded_below & r <= 0 implies ( upper_sum ((r (#) f),D)) = (r * ( lower_sum (f,D)))

    proof

      assume

       A1: (f | A) is bounded_below & r <= 0 ;

      

       A2: for i be Nat st 1 <= i & i <= ( len ( upper_volume ((r (#) f),D))) holds (( upper_volume ((r (#) f),D)) . i) = ((r * ( lower_volume (f,D))) . i)

      proof

        let i be Nat;

        assume

         A3: 1 <= i & i <= ( len ( upper_volume ((r (#) f),D)));

        ( len D) = ( len ( upper_volume ((r (#) f),D))) by INTEGRA1:def 6;

        then i in ( dom D) by A3, FINSEQ_3: 25;

        

        then (( upper_volume ((r (#) f),D)) . i) = (r * (( lower_volume (f,D)) . i)) by A1, Th26

        .= ((r * ( lower_volume (f,D))) . i) by RVSUM_1: 44;

        hence thesis;

      end;

      ( len ( upper_volume ((r (#) f),D))) = ( len D) by INTEGRA1:def 6

      .= ( len ( lower_volume (f,D))) by INTEGRA1:def 7

      .= ( len (r * ( lower_volume (f,D)))) by NEWTON: 2;

      then ( upper_volume ((r (#) f),D)) = (r * ( lower_volume (f,D))) by A2, FINSEQ_1: 14;

      

      then ( upper_sum ((r (#) f),D)) = ( Sum (r * ( lower_volume (f,D)))) by INTEGRA1:def 8

      .= (r * ( Sum ( lower_volume (f,D)))) by RVSUM_1: 87

      .= (r * ( lower_sum (f,D))) by INTEGRA1:def 9;

      hence thesis;

    end;

    theorem :: INTEGRA2:31

    

     Th31: (f | A) is bounded & f is integrable implies (r (#) f) is integrable & ( integral (r (#) f)) = (r * ( integral f))

    proof

      assume that

       A1: (f | A) is bounded and

       A2: f is integrable;

      f is upper_integrable by A2, INTEGRA1:def 16;

      then

       A3: ( rng ( upper_sum_set f)) is bounded_below by INTEGRA1:def 12;

      f is lower_integrable by A2, INTEGRA1:def 16;

      then

       A4: ( rng ( lower_sum_set f)) is bounded_above by INTEGRA1:def 13;

       A5:

      now

        per cases ;

          suppose

           A6: r >= 0 ;

          

           A7: for D be object st D in ( divs A) holds (( upper_sum_set (r (#) f)) . D) = ((r (#) ( upper_sum_set f)) . D)

          proof

            let D be object;

            assume

             A8: D in ( divs A);

            then

            reconsider D as Division of A by INTEGRA1:def 3;

            (( upper_sum_set (r (#) f)) . D) = ( upper_sum ((r (#) f),D)) by INTEGRA1:def 10

            .= (r * ( upper_sum (f,D))) by A1, A6, Th27

            .= (r * (( upper_sum_set f) . D)) by INTEGRA1:def 10

            .= ((r (#) ( upper_sum_set f)) . D) by A8, RFUNCT_1: 57;

            hence thesis;

          end;

          

           A9: ( divs A) = ( dom ( upper_sum_set f)) by FUNCT_2:def 1

          .= ( dom (r (#) ( upper_sum_set f))) by VALUED_1:def 5;

          ( divs A) = ( dom ( upper_sum_set (r (#) f))) by FUNCT_2:def 1;

          then ( upper_sum_set (r (#) f)) = (r (#) ( upper_sum_set f)) by A9, A7, FUNCT_1: 2;

          

          then

           A10: ( upper_integral (r (#) f)) = ( lower_bound ( rng (r (#) ( upper_sum_set f)))) by INTEGRA1:def 14

          .= ( lower_bound (r ** ( rng ( upper_sum_set f)))) by Th17

          .= (r * ( lower_bound ( rng ( upper_sum_set f)))) by A3, A6, Th15

          .= (r * ( upper_integral f)) by INTEGRA1:def 14;

          

           A11: for D be object st D in ( divs A) holds (( lower_sum_set (r (#) f)) . D) = ((r (#) ( lower_sum_set f)) . D)

          proof

            let D be object;

            assume

             A12: D in ( divs A);

            then

            reconsider D as Division of A by INTEGRA1:def 3;

            (( lower_sum_set (r (#) f)) . D) = ( lower_sum ((r (#) f),D)) by INTEGRA1:def 11

            .= (r * ( lower_sum (f,D))) by A1, A6, Th29

            .= (r * (( lower_sum_set f) . D)) by INTEGRA1:def 11

            .= ((r (#) ( lower_sum_set f)) . D) by A12, RFUNCT_1: 57;

            hence thesis;

          end;

          

           A13: ( divs A) = ( dom ( lower_sum_set f)) by FUNCT_2:def 1

          .= ( dom (r (#) ( lower_sum_set f))) by VALUED_1:def 5;

          ( divs A) = ( dom ( lower_sum_set (r (#) f))) by FUNCT_2:def 1;

          then ( lower_sum_set (r (#) f)) = (r (#) ( lower_sum_set f)) by A13, A11, FUNCT_1: 2;

          

          then ( lower_integral (r (#) f)) = ( upper_bound ( rng (r (#) ( lower_sum_set f)))) by INTEGRA1:def 15

          .= ( upper_bound (r ** ( rng ( lower_sum_set f)))) by Th17

          .= (r * ( upper_bound ( rng ( lower_sum_set f)))) by A4, A6, Th13

          .= (r * ( lower_integral f)) by INTEGRA1:def 15

          .= (r * ( upper_integral f)) by A2, INTEGRA1:def 16;

          hence ( upper_integral (r (#) f)) = ( lower_integral (r (#) f)) by A10;

          thus ( upper_integral (r (#) f)) = (r * ( integral f)) by A10, INTEGRA1:def 17;

        end;

          suppose

           A14: r < 0 ;

          

           A15: for D be object st D in ( divs A) holds (( upper_sum_set (r (#) f)) . D) = ((r (#) ( lower_sum_set f)) . D)

          proof

            let D be object;

            assume

             A16: D in ( divs A);

            then

            reconsider D as Division of A by INTEGRA1:def 3;

            (( upper_sum_set (r (#) f)) . D) = ( upper_sum ((r (#) f),D)) by INTEGRA1:def 10

            .= (r * ( lower_sum (f,D))) by A1, A14, Th30

            .= (r * (( lower_sum_set f) . D)) by INTEGRA1:def 11

            .= ((r (#) ( lower_sum_set f)) . D) by A16, RFUNCT_1: 57;

            hence thesis;

          end;

          

           A17: ( divs A) = ( dom ( lower_sum_set f)) by FUNCT_2:def 1

          .= ( dom (r (#) ( lower_sum_set f))) by VALUED_1:def 5;

          ( divs A) = ( dom ( upper_sum_set (r (#) f))) by FUNCT_2:def 1;

          then ( upper_sum_set (r (#) f)) = (r (#) ( lower_sum_set f)) by A17, A15, FUNCT_1: 2;

          

          then

           A18: ( upper_integral (r (#) f)) = ( lower_bound ( rng (r (#) ( lower_sum_set f)))) by INTEGRA1:def 14

          .= ( lower_bound (r ** ( rng ( lower_sum_set f)))) by Th17

          .= (r * ( upper_bound ( rng ( lower_sum_set f)))) by A4, A14, Th14

          .= (r * ( lower_integral f)) by INTEGRA1:def 15;

          

           A19: for D be object st D in ( divs A) holds (( lower_sum_set (r (#) f)) . D) = ((r (#) ( upper_sum_set f)) . D)

          proof

            let D be object;

            assume

             A20: D in ( divs A);

            then

            reconsider D as Division of A by INTEGRA1:def 3;

            (( lower_sum_set (r (#) f)) . D) = ( lower_sum ((r (#) f),D)) by INTEGRA1:def 11

            .= (r * ( upper_sum (f,D))) by A1, A14, Th28

            .= (r * (( upper_sum_set f) . D)) by INTEGRA1:def 10

            .= ((r (#) ( upper_sum_set f)) . D) by A20, RFUNCT_1: 57;

            hence thesis;

          end;

          

           A21: ( divs A) = ( dom ( upper_sum_set f)) by FUNCT_2:def 1

          .= ( dom (r (#) ( upper_sum_set f))) by VALUED_1:def 5;

          ( divs A) = ( dom ( lower_sum_set (r (#) f))) by FUNCT_2:def 1;

          then ( lower_sum_set (r (#) f)) = (r (#) ( upper_sum_set f)) by A21, A19, FUNCT_1: 2;

          

          then ( lower_integral (r (#) f)) = ( upper_bound ( rng (r (#) ( upper_sum_set f)))) by INTEGRA1:def 15

          .= ( upper_bound (r ** ( rng ( upper_sum_set f)))) by Th17

          .= (r * ( lower_bound ( rng ( upper_sum_set f)))) by A3, A14, Th16

          .= (r * ( upper_integral f)) by INTEGRA1:def 14

          .= (r * ( lower_integral f)) by A2, INTEGRA1:def 16;

          hence ( upper_integral (r (#) f)) = ( lower_integral (r (#) f)) by A18;

          ( upper_integral (r (#) f)) = (r * ( upper_integral f)) by A2, A18, INTEGRA1:def 16

          .= (r * ( integral f)) by INTEGRA1:def 17;

          hence ( upper_integral (r (#) f)) = (r * ( integral f));

        end;

      end;

      ex a st for D be object st D in (( divs A) /\ ( dom ( lower_sum_set (r (#) f)))) holds a >= (( lower_sum_set (r (#) f)) . D)

      proof

        now

          per cases ;

            suppose

             A22: r >= 0 ;

            for D be object st D in (( divs A) /\ ( dom ( lower_sum_set (r (#) f)))) holds ((r * ( upper_bound ( rng f))) * ( vol A)) >= (( lower_sum_set (r (#) f)) . D)

            proof

              let D be object;

              assume D in (( divs A) /\ ( dom ( lower_sum_set (r (#) f))));

              then D is Division of A by INTEGRA1:def 3;

              hence thesis by A1, A22, Th21;

            end;

            hence thesis;

          end;

            suppose

             A23: r < 0 ;

            for D be object st D in (( divs A) /\ ( dom ( lower_sum_set (r (#) f)))) holds ((r * ( lower_bound ( rng f))) * ( vol A)) >= (( lower_sum_set (r (#) f)) . D)

            proof

              let D be object;

              assume D in (( divs A) /\ ( dom ( lower_sum_set (r (#) f))));

              then D is Division of A by INTEGRA1:def 3;

              hence thesis by A1, A23, Th22;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      then (( lower_sum_set (r (#) f)) | ( divs A)) is bounded_above by RFUNCT_1: 70;

      then ( rng ( lower_sum_set (r (#) f))) is bounded_above by INTEGRA1: 13;

      then

       A24: (r (#) f) is lower_integrable by INTEGRA1:def 13;

      ex a st for D be object st D in (( divs A) /\ ( dom ( upper_sum_set (r (#) f)))) holds a <= (( upper_sum_set (r (#) f)) . D)

      proof

        now

          per cases ;

            suppose

             A25: r >= 0 ;

            for D be object st D in (( divs A) /\ ( dom ( upper_sum_set (r (#) f)))) holds ((r * ( lower_bound ( rng f))) * ( vol A)) <= (( upper_sum_set (r (#) f)) . D)

            proof

              let D be object;

              assume D in (( divs A) /\ ( dom ( upper_sum_set (r (#) f))));

              then D is Division of A by INTEGRA1:def 3;

              hence thesis by A1, A25, Th19;

            end;

            hence thesis;

          end;

            suppose

             A26: r < 0 ;

            for D be object st D in (( divs A) /\ ( dom ( upper_sum_set (r (#) f)))) holds ((r * ( upper_bound ( rng f))) * ( vol A)) <= (( upper_sum_set (r (#) f)) . D)

            proof

              let D be object;

              assume D in (( divs A) /\ ( dom ( upper_sum_set (r (#) f))));

              then D is Division of A by INTEGRA1:def 3;

              hence thesis by A1, A26, Th20;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      then (( upper_sum_set (r (#) f)) | ( divs A)) is bounded_below by RFUNCT_1: 71;

      then ( rng ( upper_sum_set (r (#) f))) is bounded_below by INTEGRA1: 11;

      then (r (#) f) is upper_integrable by INTEGRA1:def 12;

      hence thesis by A24, A5, INTEGRA1:def 16, INTEGRA1:def 17;

    end;

    begin

    theorem :: INTEGRA2:32

    

     Th32: (f | A) is bounded & (for x st x in A holds (f . x) >= 0 ) implies ( integral f) >= 0

    proof

      assume that

       A1: (f | A) is bounded and

       A2: for x st x in A holds (f . x) >= 0 ;

      

       A3: for a be Real st a in ( rng ( upper_sum_set f)) holds a >= 0

      proof

        let a be Real;

        assume a in ( rng ( upper_sum_set f));

        then

        consider D be Element of ( divs A) such that

         A4: D in ( dom ( upper_sum_set f)) & a = (( upper_sum_set f) . D) by PARTFUN1: 3;

        reconsider D as Division of A by INTEGRA1:def 3;

        

         A5: for i be Nat st i in ( dom ( upper_volume (f,D))) holds 0 <= (( upper_volume (f,D)) . i)

        proof

          let i be Nat;

          set r = (( upper_volume (f,D)) . i);

          assume

           A6: i in ( dom ( upper_volume (f,D)));

          ( len D) = ( len ( upper_volume (f,D))) by INTEGRA1:def 6;

          then

           A7: i in ( dom D) by A6, FINSEQ_3: 29;

          

           A8: ( upper_bound ( rng (f | ( divset (D,i))))) >= 0

          proof

            ( rng f) is bounded_above by A1, INTEGRA1: 13;

            then

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

            ( dom (f | ( divset (D,i)))) = (( dom f) /\ ( divset (D,i))) & ( dom f) = A by FUNCT_2:def 1, RELAT_1: 61;

            then ( dom (f | ( divset (D,i)))) is non empty Subset of REAL by A7, INTEGRA1: 8, XBOOLE_1: 28;

            then

            consider x be Element of REAL such that

             A10: x in ( dom (f | ( divset (D,i)))) by SUBSET_1: 4;

            (f . x) >= 0 by A2, A10;

            then

             A11: ((f | ( divset (D,i))) . x) >= 0 by A10, FUNCT_1: 47;

            ((f | ( divset (D,i))) . x) in ( rng (f | ( divset (D,i)))) by A10, FUNCT_1:def 3;

            hence thesis by A9, A11, SEQ_4:def 1;

          end;

          

           A12: ( vol ( divset (D,i))) >= 0 by INTEGRA1: 9;

          r = (( upper_bound ( rng (f | ( divset (D,i))))) * ( vol ( divset (D,i)))) by A7, INTEGRA1:def 6;

          hence thesis by A12, A8;

        end;

        a = ( upper_sum (f,D)) by A4, INTEGRA1:def 10

        .= ( Sum ( upper_volume (f,D))) by INTEGRA1:def 8;

        hence thesis by A5, RVSUM_1: 84;

      end;

      ( upper_integral f) = ( lower_bound ( rng ( upper_sum_set f))) & ( rng ( upper_sum_set f)) is non empty by INTEGRA1:def 14;

      then ( upper_integral f) >= 0 by A3, SEQ_4: 43;

      hence thesis by INTEGRA1:def 17;

    end;

    theorem :: INTEGRA2:33

    

     Th33: (f | A) is bounded & f is integrable & (g | A) is bounded & g is integrable implies (f - g) is integrable & ( integral (f - g)) = (( integral f) - ( integral g))

    proof

      assume that

       A1: (f | A) is bounded & f is integrable and

       A2: (g | A) is bounded and

       A3: g is integrable;

      

       A4: ( - g) is integrable by A2, A3, Th31;

      

       A5: (( - g) | A) is bounded by A2, RFUNCT_1: 82;

      hence (f - g) is integrable by A1, A4, INTEGRA1: 57;

      ( integral ( - g)) = (( - 1) * ( integral g)) by A2, A3, Th31;

      then ( integral (f - g)) = (( integral f) + ( - ( integral g))) by A1, A5, A4, INTEGRA1: 57;

      hence thesis;

    end;

    theorem :: INTEGRA2:34

    (f | A) is bounded & f is integrable & (g | A) is bounded & g is integrable & (for x st x in A holds (f . x) >= (g . x)) implies ( integral f) >= ( integral g)

    proof

      assume that

       A1: (f | A) is bounded & f is integrable & (g | A) is bounded & g is integrable and

       A2: for x st x in A holds (f . x) >= (g . x);

      

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

      

       A4: for x st x in A holds ((f - g) . x) >= 0

      proof

        let x;

        assume

         A5: x in A;

        then ((f - g) . x) = ((f . x) - (g . x)) by A3, VALUED_1: 13;

        hence thesis by A2, A5, XREAL_1: 48;

      end;

      ( integral (f - g)) = (( integral f) - ( integral g)) & ((f - g) | (A /\ A)) is bounded by A1, Th33, RFUNCT_1: 84;

      hence thesis by A4, Th32, XREAL_1: 49;

    end;

    begin

    theorem :: INTEGRA2:35

    (f | A) is bounded implies ( rng ( upper_sum_set f)) is bounded_below

    proof

      set D1 = the Division of A;

      assume

       A1: (f | A) is bounded;

      take ( lower_sum (f,D1));

      let a be ExtReal;

      assume a in ( rng ( upper_sum_set f));

      then

      consider D be Element of ( divs A) such that

       A2: D in ( dom ( upper_sum_set f)) & a = (( upper_sum_set f) . D) by PARTFUN1: 3;

      reconsider D as Division of A by INTEGRA1:def 3;

      a = ( upper_sum (f,D)) by A2, INTEGRA1:def 10;

      hence thesis by A1, INTEGRA1: 48;

    end;

    theorem :: INTEGRA2:36

    (f | A) is bounded implies ( rng ( lower_sum_set f)) is bounded_above

    proof

      set D1 = the Division of A;

      assume

       A1: (f | A) is bounded;

      take ( upper_sum (f,D1));

      let a be ExtReal;

      assume a in ( rng ( lower_sum_set f));

      then

      consider D be Element of ( divs A) such that

       A2: D in ( dom ( lower_sum_set f)) & a = (( lower_sum_set f) . D) by PARTFUN1: 3;

      reconsider D as Division of A by INTEGRA1:def 3;

      a = ( lower_sum (f,D)) by A2, INTEGRA1:def 11;

      hence thesis by A1, INTEGRA1: 48;

    end;

    definition

      let A be non empty closed_interval Subset of REAL ;

      mode DivSequence of A is sequence of ( divs A);

    end

    definition

      let A;

      let T be DivSequence of A;

      let i;

      :: original: .

      redefine

      func T . i -> Division of A ;

      coherence

      proof

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

        (T . i) is Element of ( divs A);

        hence thesis by INTEGRA1:def 3;

      end;

    end

    definition

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

      :: INTEGRA2:def2

      func upper_sum (f,T) -> Real_Sequence means for i holds (it . i) = ( upper_sum (f,(T . i)));

      existence

      proof

        deffunc F( Nat) = ( upper_sum (f,(T . ( In ($1, NAT )))));

        consider IT be Real_Sequence such that

         A1: for i be Nat holds (IT . i) = F(i) from SEQ_1:sch 1;

        take IT;

        let i;

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

        hence thesis;

      end;

      uniqueness

      proof

        let F1,F2 be Real_Sequence such that

         A2: for i holds (F1 . i) = ( upper_sum (f,(T . i))) and

         A3: for i holds (F2 . i) = ( upper_sum (f,(T . i)));

        for i be Element of NAT holds (F1 . i) = (F2 . i)

        proof

          let i be Element of NAT ;

          (F1 . i) = ( upper_sum (f,(T . i))) by A2

          .= (F2 . i) by A3;

          hence thesis;

        end;

        hence thesis by FUNCT_2: 63;

      end;

      :: INTEGRA2:def3

      func lower_sum (f,T) -> Real_Sequence means for i holds (it . i) = ( lower_sum (f,(T . i)));

      existence

      proof

        deffunc F( Nat) = ( lower_sum (f,(T . ( In ($1, NAT )))));

        consider IT be Real_Sequence such that

         A4: for i be Nat holds (IT . i) = F(i) from SEQ_1:sch 1;

        take IT;

        let i;

        (IT . i) = F(i) by A4;

        hence thesis;

      end;

      uniqueness

      proof

        let F1,F2 be Real_Sequence such that

         A5: for i holds (F1 . i) = ( lower_sum (f,(T . i))) and

         A6: for i holds (F2 . i) = ( lower_sum (f,(T . i)));

        for i be Element of NAT holds (F1 . i) = (F2 . i)

        proof

          let i be Element of NAT ;

          (F1 . i) = ( lower_sum (f,(T . i))) by A5

          .= (F2 . i) by A6;

          hence thesis;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    theorem :: INTEGRA2:37

    D1 <= D2 implies for j st j in ( dom D2) holds ex i st i in ( dom D1) & ( divset (D2,j)) c= ( divset (D1,i))

    proof

      assume

       A1: D1 <= D2;

      let j;

      defpred P[ set] means (D2 . $1) in ( rng D1) & (D2 . $1) >= (D2 . j);

      consider X be Subset of ( dom D2) such that

       A2: for x1 holds x1 in X iff x1 in ( dom D2) & P[x1] from SUBSET_1:sch 1;

      reconsider X as Subset of NAT by XBOOLE_1: 1;

      assume

       A3: j in ( dom D2);

      ex n st n in ( dom D2) & (D2 . n) in ( rng D1) & (D2 . n) >= (D2 . j)

      proof

        take ( len D2);

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

        then

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

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

        then

         A5: ( len D1) in ( dom D1) by FINSEQ_1:def 3;

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

        then

         A6: (D1 . ( len D1)) = (D2 . ( len D2)) by INTEGRA1:def 2;

        j in ( Seg ( len D2)) by A3, FINSEQ_1:def 3;

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

        hence thesis by A3, A5, A6, A4, FUNCT_1:def 3, SEQ_4: 137;

      end;

      then

      reconsider X as non empty Subset of NAT by A2;

      

       A7: ( min X) in X by XXREAL_2:def 7;

      then

       A8: (D2 . ( min X)) >= (D2 . j) by A2;

      (D2 . ( min X)) in ( rng D1) by A2, A7;

      then

      consider i be Element of NAT such that

       A9: i in ( dom D1) and

       A10: (D2 . ( min X)) = (D1 . i) by PARTFUN1: 3;

      take i;

      

       A11: (D1 . i) >= (D2 . j) by A2, A7, A10;

      ( divset (D2,j)) c= ( divset (D1,i))

      proof

        now

          per cases ;

            suppose i = 1;

            then ( lower_bound ( divset (D1,i))) = ( lower_bound A) & ( upper_bound ( divset (D1,i))) = (D1 . i) by A9, INTEGRA1:def 4;

            then

             A12: ( divset (D1,i)) = [.( lower_bound A), (D1 . i).] by INTEGRA1: 4;

            now

              per cases ;

                suppose

                 A13: j = 1;

                (D1 . i) in ( rng D1) & ( rng D1) c= A by A9, FUNCT_1:def 3, INTEGRA1:def 2;

                then

                 A14: (D1 . i) in A;

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

                then (D1 . i) in { r : ( lower_bound A) <= r & r <= ( upper_bound A) } by A14, RCOMP_1:def 1;

                then ex x st x = (D1 . i) & ( lower_bound A) <= x & x <= ( upper_bound A);

                then ( lower_bound A) in { r : ( lower_bound A) <= r & r <= (D1 . i) };

                then

                 A15: ( lower_bound A) in [.( lower_bound A), (D1 . i).] by RCOMP_1:def 1;

                (D2 . j) in ( rng D2) & ( rng D2) c= A by A3, FUNCT_1:def 3, INTEGRA1:def 2;

                then

                 A16: (D2 . j) in A;

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

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

                then ex x st x = (D2 . j) & ( lower_bound A) <= x & x <= ( upper_bound A);

                then (D2 . j) in { r : ( lower_bound A) <= r & r <= (D1 . i) } by A8, A10;

                then

                 A17: (D2 . j) in [.( lower_bound A), (D1 . i).] by RCOMP_1:def 1;

                ( lower_bound ( divset (D2,j))) = ( lower_bound A) & ( upper_bound ( divset (D2,j))) = (D2 . j) by A3, A13, INTEGRA1:def 4;

                then ( divset (D2,j)) = [.( lower_bound A), (D2 . j).] by INTEGRA1: 4;

                hence thesis by A12, A15, A17, XXREAL_2:def 12;

              end;

                suppose

                 A18: j <> 1;

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

                then

                 A19: A = { r : ( lower_bound A) <= r & r <= ( upper_bound A) } by RCOMP_1:def 1;

                (D2 . j) in ( rng D2) & ( rng D2) c= A by A3, FUNCT_1:def 3, INTEGRA1:def 2;

                then (D2 . j) in { r : ( lower_bound A) <= r & r <= ( upper_bound A) } by A19;

                then ex x st x = (D2 . j) & ( lower_bound A) <= x & x <= ( upper_bound A);

                then (D2 . j) in { r : ( lower_bound A) <= r & r <= (D1 . i) } by A8, A10;

                then

                 A20: (D2 . j) in [.( lower_bound A), (D1 . i).] by RCOMP_1:def 1;

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

                then

                 A21: A = { r : ( lower_bound A) <= r & r <= ( upper_bound A) } by RCOMP_1:def 1;

                

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

                

                 A23: (j - 1) in ( dom D2) by A3, A18, INTEGRA1: 7;

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

                then (D2 . (j - 1)) in { r : ( lower_bound A) <= r & r <= ( upper_bound A) } by A21, A22;

                then

                 A24: ex x st x = (D2 . (j - 1)) & ( lower_bound A) <= x & x <= ( upper_bound A);

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

                then (j - 1) <= j by XREAL_1: 20;

                then (D2 . (j - 1)) <= (D2 . j) by A3, A23, SEQ_4: 137;

                then (D2 . (j - 1)) <= (D1 . i) by A8, A10, XXREAL_0: 2;

                then (D2 . (j - 1)) in { r : ( lower_bound A) <= r & r <= (D1 . i) } by A24;

                then

                 A25: (D2 . (j - 1)) in [.( lower_bound A), (D1 . i).] by RCOMP_1:def 1;

                ( lower_bound ( divset (D2,j))) = (D2 . (j - 1)) & ( upper_bound ( divset (D2,j))) = (D2 . j) by A3, A18, INTEGRA1:def 4;

                then ( divset (D2,j)) = [.(D2 . (j - 1)), (D2 . j).] by INTEGRA1: 4;

                hence thesis by A12, A25, A20, XXREAL_2:def 12;

              end;

            end;

            hence thesis;

          end;

            suppose

             A26: i <> 1;

            

             A27: j <> 1

            proof

              assume

               A28: j = 1;

              

               A29: i in ( Seg ( len D1)) by A9, FINSEQ_1:def 3;

              then

               A30: 1 <= i by FINSEQ_1: 1;

              i <= ( len D1) by A29, FINSEQ_1: 1;

              then 1 <= ( len D1) by A30, XXREAL_0: 2;

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

              then

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

              then

               A32: (D1 . 1) in ( rng D1) by FUNCT_1:def 3;

              ( rng D1) c= ( rng D2) by A1, INTEGRA1:def 18;

              then

              consider n be Element of NAT such that

               A33: n in ( dom D2) and

               A34: (D1 . 1) = (D2 . n) by A32, PARTFUN1: 3;

              

               A35: n in ( Seg ( len D2)) by A33, FINSEQ_1:def 3;

              then

               A36: 1 <= n by FINSEQ_1: 1;

              n <= ( 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 1 in ( dom D2) by FINSEQ_1:def 3;

              then (D2 . j) <= (D2 . n) by A28, A33, A36, SEQ_4: 137;

              then n in X by A2, A32, A33, A34;

              then n >= ( min X) by XXREAL_2:def 7;

              then

               A37: (D1 . 1) >= (D1 . i) by A7, A10, A33, A34, SEQ_4: 137;

              i > 1 by A26, A30, XXREAL_0: 1;

              hence contradiction by A9, A31, A37, SEQM_3:def 1;

            end;

            then

             A38: (j - 1) in ( dom D2) by A3, INTEGRA1: 7;

            

             A39: (D1 . (i - 1)) <= (D2 . (j - 1))

            proof

              

               A40: (i - 1) in ( dom D1) by A9, A26, INTEGRA1: 7;

              then

               A41: (D1 . (i - 1)) in ( rng D1) by FUNCT_1:def 3;

              ( rng D1) c= ( rng D2) by A1, INTEGRA1:def 18;

              then

              consider n be Element of NAT such that

               A42: n in ( dom D2) & (D1 . (i - 1)) = (D2 . n) by A41, PARTFUN1: 3;

              assume (D1 . (i - 1)) > (D2 . (j - 1));

              then n > (j - 1) by A38, A42, SEQ_4: 137;

              then (n + 1) > j by XREAL_1: 19;

              then n >= j by NAT_1: 13;

              then (D1 . (i - 1)) >= (D2 . j) by A3, A42, SEQ_4: 137;

              then n in X by A2, A41, A42;

              then n >= ( min X) by XXREAL_2:def 7;

              then (D1 . (i - 1)) >= (D1 . i) by A7, A10, A42, SEQ_4: 137;

              then (i - 1) >= i by A9, A40, SEQM_3:def 1;

              then

               A43: i >= (i + 1) by XREAL_1: 19;

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

              then i = (i + 1) by A43, XXREAL_0: 1;

              hence contradiction;

            end;

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

            then (j - 1) <= j by XREAL_1: 20;

            then

             A44: (D2 . (j - 1)) <= (D2 . j) by A3, A38, SEQ_4: 137;

            then

             A45: (D1 . (i - 1)) <= (D2 . j) by A39, XXREAL_0: 2;

            (D2 . (j - 1)) <= (D1 . i) by A11, A44, XXREAL_0: 2;

            then (D2 . (j - 1)) in { r : (D1 . (i - 1)) <= r & r <= (D1 . i) } by A39;

            then

             A46: (D2 . (j - 1)) in [.(D1 . (i - 1)), (D1 . i).] by RCOMP_1:def 1;

            (D2 . j) <= (D1 . i) by A2, A7, A10;

            then (D2 . j) in { r : (D1 . (i - 1)) <= r & r <= (D1 . i) } by A45;

            then

             A47: (D2 . j) in [.(D1 . (i - 1)), (D1 . i).] by RCOMP_1:def 1;

            ( lower_bound ( divset (D2,j))) = (D2 . (j - 1)) & ( upper_bound ( divset (D2,j))) = (D2 . j) by A3, A27, INTEGRA1:def 4;

            then

             A48: ( divset (D2,j)) = [.(D2 . (j - 1)), (D2 . j).] by INTEGRA1: 4;

            ( lower_bound ( divset (D1,i))) = (D1 . (i - 1)) & ( upper_bound ( divset (D1,i))) = (D1 . i) by A9, A26, INTEGRA1:def 4;

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

            hence thesis by A48, A46, A47, XXREAL_2:def 12;

          end;

        end;

        hence thesis;

      end;

      hence thesis by A9;

    end;

    theorem :: INTEGRA2:38

    A c= B implies ( vol A) <= ( vol B)

    proof

      assume

       A1: A c= B;

      ( vol A) = (( upper_bound A) - ( lower_bound A)) by INTEGRA1:def 5;

      then ( upper_bound B) >= (( vol A) + ( lower_bound A)) by A1, SEQ_4: 48;

      then

       A2: (( upper_bound B) - ( vol A)) >= ( lower_bound A) by XREAL_1: 19;

      ( lower_bound A) >= ( lower_bound B) by A1, SEQ_4: 47;

      then (( upper_bound B) - ( vol A)) >= ( lower_bound B) by A2, XXREAL_0: 2;

      then (( upper_bound B) - ( lower_bound B)) >= ( vol A) by XREAL_1: 11;

      hence thesis by INTEGRA1:def 5;

    end;

    theorem :: INTEGRA2:39

    for A be Subset of REAL , a,x be Real st x in (a ** A) holds ex b be Real st b in A & x = (a * b)

    proof

      let A be Subset of REAL , a,x be Real;

      assume x in (a ** A);

      then x in { (a * b) where b be Element of ExtREAL : b in A } by MEMBER_1: 187;

      then

      consider b be Element of ExtREAL such that

       A1: x = (a * b) & b in A;

      reconsider b as Real by A1;

      take b;

      x = (a * b) by A1, XXREAL_3:def 5;

      hence thesis by A1;

    end;

    begin

    theorem :: INTEGRA2:40

    for A be non empty ext-real-membered set holds ( 0 ** A) = { 0 }

    proof

      let A be non empty ext-real-membered set;

      for e be object holds e in ( 0 ** A) iff e = 0

      proof

        let e be object;

        consider r be ExtReal such that

         A1: r in A by MEMBERED: 8;

        hereby

          assume e in ( 0 ** A);

          then ex z be Element of ExtREAL st e = ( 0 * z) & z in A by MEMBER_1: 188;

          hence e = 0 ;

        end;

        assume e = 0 ;

        then e = ( 0 * r);

        hence thesis by A1, MEMBER_1: 186;

      end;

      hence thesis by TARSKI:def 1;

    end;