measure7.miz



    begin

    theorem :: MEASURE7:1

    

     Th1: for F be sequence of ExtREAL st for n be Element of NAT holds (F . n) = 0. holds ( SUM F) = 0.

    proof

      let F be sequence of ExtREAL ;

      defpred P[ Nat] means (( Ser F) . $1) = 0. ;

      assume

       A1: for n be Element of NAT holds (F . n) = 0. ;

      

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

      proof

        let t be Nat;

        assume (( Ser F) . t) = 0. ;

        

        hence (( Ser F) . (t + 1)) = ( 0. + (F . (t + 1))) by SUPINF_2:def 11

        .= (F . (t + 1)) by XXREAL_3: 4

        .= 0. by A1;

      end;

      

       A3: (( Ser F) . 0 ) = (F . 0 ) by SUPINF_2:def 11

      .= 0. by A1;

      then

       A4: P[ 0 ];

      

       A5: for s be Nat holds P[s] from NAT_1:sch 2( A4, A2);

      

       A6: ( rng ( Ser F)) = { 0. }

      proof

        thus ( rng ( Ser F)) c= { 0. }

        proof

          let x be object;

          assume x in ( rng ( Ser F));

          then

          consider s be object such that

           A7: s in ( dom ( Ser F)) and

           A8: x = (( Ser F) . s) by FUNCT_1:def 3;

          reconsider s as Element of NAT by A7;

          (( Ser F) . s) = 0. by A5;

          hence thesis by A8, TARSKI:def 1;

        end;

        let x be object;

        assume x in { 0. };

        then ( dom ( Ser F)) = NAT & x = 0. by FUNCT_2:def 1, TARSKI:def 1;

        hence thesis by A3, FUNCT_1:def 3;

      end;

      ( sup { 0. }) = 0. by XXREAL_2: 11;

      hence thesis by A6;

    end;

    theorem :: MEASURE7:2

    

     Th2: for F be sequence of ExtREAL st F is nonnegative holds for n be Nat holds (F . n) <= (( Ser F) . n)

    proof

      let F be sequence of ExtREAL ;

      assume

       A1: F is nonnegative;

      let n be Nat;

      per cases ;

        suppose n = 0 ;

        hence thesis by SUPINF_2:def 11;

      end;

        suppose n <> 0 ;

        then

        consider k be Nat such that

         A2: n = (k + 1) by NAT_1: 6;

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

        

         A3: 0. <= (( Ser F) . k) by A1, SUPINF_2: 40;

        (( Ser F) . n) = ((( Ser F) . k) + (F . n)) by A2, SUPINF_2:def 11;

        then ( 0. + (F . n)) <= (( Ser F) . n) by A3, XXREAL_3: 36;

        hence thesis by XXREAL_3: 4;

      end;

    end;

    theorem :: MEASURE7:3

    

     Th3: for F,G,H be sequence of ExtREAL st G is nonnegative & H is nonnegative holds (for n be Element of NAT holds (F . n) = ((G . n) + (H . n))) implies for n be Nat holds (( Ser F) . n) = ((( Ser G) . n) + (( Ser H) . n))

    proof

      let F,G,H be sequence of ExtREAL ;

      assume that

       A1: G is nonnegative and

       A2: H is nonnegative;

      defpred P[ Nat] means (( Ser F) . $1) = ((( Ser G) . $1) + (( Ser H) . $1));

      assume

       A3: for n be Element of NAT holds (F . n) = ((G . n) + (H . n));

      

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

      proof

        let k be Nat;

        assume

         A5: (( Ser F) . k) = ((( Ser G) . k) + (( Ser H) . k));

        set n = (k + 1);

        

         A6: (( Ser G) . (k + 1)) = ((( Ser G) . k) + (G . (k + 1))) & (( Ser H) . (k + 1)) = ((( Ser H) . k) + (H . (k + 1))) by SUPINF_2:def 11;

        

         A7: 0. <= (H . (k + 1)) by A2, SUPINF_2: 39;

        

         A8: (F . (k + 1)) = ((G . (k + 1)) + (H . (k + 1))) & 0. <= (G . (k + 1)) by A1, A3, SUPINF_2: 39;

        

         A9: 0. <= (( Ser G) . k) by A1, SUPINF_2: 40;

        

         A10: 0. <= (( Ser G) . (k + 1)) by A1, SUPINF_2: 40;

        

         A11: 0. <= (( Ser H) . k) by A2, SUPINF_2: 40;

         0. <= (G . n) & 0. <= (H . n) by A1, A2, SUPINF_2: 39;

        then ( 0. + 0. ) <= ((G . n) + (H . n)) by XXREAL_3: 36;

        then 0. <= (F . (k + 1)) by A3;

        

        then (((( Ser G) . k) + (( Ser H) . k)) + (F . (k + 1))) = (((( Ser G) . k) + (F . (k + 1))) + (( Ser H) . k)) by A9, A11, XXREAL_3: 44

        .= ((((( Ser G) . k) + (G . (k + 1))) + (H . (k + 1))) + (( Ser H) . k)) by A9, A7, A8, XXREAL_3: 44

        .= ((( Ser G) . (k + 1)) + (( Ser H) . (k + 1))) by A6, A11, A10, A7, XXREAL_3: 44;

        hence thesis by A5, SUPINF_2:def 11;

      end;

      

       A12: (( Ser H) . 0 ) = (H . 0 ) by SUPINF_2:def 11;

      (( Ser F) . 0 ) = (F . 0 ) & (( Ser G) . 0 ) = (G . 0 ) by SUPINF_2:def 11;

      then

       A13: P[ 0 ] by A3, A12;

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

    end;

    theorem :: MEASURE7:4

    

     Th4: for F,G,H be sequence of ExtREAL st for n be Element of NAT holds (F . n) = ((G . n) + (H . n)) holds G is nonnegative & H is nonnegative implies ( SUM F) <= (( SUM G) + ( SUM H))

    proof

      let F,G,H be sequence of ExtREAL ;

      assume

       A1: for n be Element of NAT holds (F . n) = ((G . n) + (H . n));

      defpred P[ Nat] means (( Ser F) . $1) = ((( Ser G) . $1) + (( Ser H) . $1));

      assume that

       A2: G is nonnegative and

       A3: H is nonnegative;

      

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

      proof

        let k be Nat;

        

         A5: (( Ser G) . (k + 1)) = ((( Ser G) . k) + (G . (k + 1))) & (( Ser H) . (k + 1)) = ((( Ser H) . k) + (H . (k + 1))) by SUPINF_2:def 11;

        

         A6: 0. <= (( Ser G) . k) by A2, SUPINF_2: 40;

        

         A7: 0. <= (( Ser H) . (k + 1)) by A3, SUPINF_2: 40;

        

         A8: 0. <= (H . (k + 1)) by A3, SUPINF_2: 39;

        

         A9: 0. <= (( Ser H) . k) by A3, SUPINF_2: 40;

         0. <= (G . (k + 1)) & 0. <= (H . (k + 1)) by A2, A3, SUPINF_2: 39;

        then ( 0. + 0. ) <= ((G . (k + 1)) + (H . (k + 1))) by XXREAL_3: 36;

        then

         A10: (( Ser F) . (k + 1)) = ((( Ser F) . k) + (F . (k + 1))) & 0. <= (F . (k + 1)) by A1, SUPINF_2:def 11;

        

         A11: 0. <= (G . (k + 1)) by A2, SUPINF_2: 39;

        assume (( Ser F) . k) = ((( Ser G) . k) + (( Ser H) . k));

        

        hence (( Ser F) . (k + 1)) = ((( Ser G) . k) + ((( Ser H) . k) + (F . (k + 1)))) by A10, A6, A9, XXREAL_3: 44

        .= ((( Ser G) . k) + ((( Ser H) . k) + ((G . (k + 1)) + (H . (k + 1))))) by A1

        .= ((( Ser G) . k) + (((( Ser H) . k) + (H . (k + 1))) + (G . (k + 1)))) by A11, A9, A8, XXREAL_3: 44

        .= ((( Ser G) . (k + 1)) + (( Ser H) . (k + 1))) by A5, A6, A11, A7, XXREAL_3: 44;

      end;

      

       A12: (( Ser H) . 0 ) = (H . 0 ) by SUPINF_2:def 11;

      (( Ser F) . 0 ) = (F . 0 ) & (( Ser G) . 0 ) = (G . 0 ) by SUPINF_2:def 11;

      then

       A13: P[ 0 ] by A1, A12;

      

       A14: for n be Nat holds P[n] from NAT_1:sch 2( A13, A4);

      (( SUM G) + ( SUM H)) is UpperBound of ( rng ( Ser F))

      proof

        let x be ExtReal;

        

         A15: ( dom ( Ser F)) = NAT by FUNCT_2:def 1;

        assume x in ( rng ( Ser F));

        then

        consider n be object such that

         A16: n in NAT and

         A17: x = (( Ser F) . n) by A15, FUNCT_1:def 3;

        reconsider n as Element of NAT by A16;

        (( Ser H) . n) <= ( sup ( rng ( Ser H))) by FUNCT_2: 4, XXREAL_2: 4;

        then

         A18: (( Ser H) . n) <= ( SUM H);

        (( Ser G) . n) <= ( sup ( rng ( Ser G))) by FUNCT_2: 4, XXREAL_2: 4;

        then (( Ser G) . n) <= ( SUM G);

        then ((( Ser G) . n) + (( Ser H) . n)) <= (( SUM G) + ( SUM H)) by A18, XXREAL_3: 36;

        hence thesis by A14, A17;

      end;

      then ( sup ( rng ( Ser F))) <= (( SUM G) + ( SUM H)) by XXREAL_2:def 3;

      hence thesis;

    end;

    theorem :: MEASURE7:5

    

     Th5: for F,G be sequence of ExtREAL holds (for n be Element of NAT holds (F . n) <= (G . n)) implies for n be Element of NAT holds (( Ser F) . n) <= ( SUM G)

    proof

      let F,G be sequence of ExtREAL ;

      assume

       A1: for n be Element of NAT holds (F . n) <= (G . n);

      let n be Element of NAT ;

      set y = (( Ser G) . n);

      ( dom ( Ser G)) = NAT by FUNCT_2:def 1;

      then ( SUM G) = ( sup ( rng ( Ser G))) & y in ( rng ( Ser G)) by FUNCT_1:def 3;

      hence thesis by A1, SUPINF_2: 42, XXREAL_2: 61;

    end;

    theorem :: MEASURE7:6

    

     Th6: for F be sequence of ExtREAL holds F is nonnegative implies for n be Element of NAT holds (( Ser F) . n) <= ( SUM F)

    proof

      let F be sequence of ExtREAL ;

      for n be Element of NAT holds (F . n) <= (F . n);

      hence thesis by Th5;

    end;

    definition

      let S be non empty set;

      let H be Function of S, ExtREAL ;

      :: MEASURE7:def1

      func On H -> sequence of ExtREAL means

      : Def1: for n be Element of NAT holds (n in S implies (it . n) = (H . n)) & ( not n in S implies (it . n) = 0. );

      existence

      proof

        defpred P[ Element of NAT , Element of ExtREAL ] means ($1 in S implies $2 = (H . $1)) & ( not $1 in S implies $2 = 0. );

        

         A1: for n be Element of NAT holds ex y be Element of ExtREAL st P[n, y]

        proof

          let n be Element of NAT ;

          per cases ;

            suppose n in S;

            then

            reconsider n as Element of S;

            take (H . n);

            thus thesis;

          end;

            suppose

             A2: not n in S;

            take 0. ;

            thus thesis by A2;

          end;

        end;

        consider GG be sequence of ExtREAL such that

         A3: for n be Element of NAT holds P[n, (GG . n)] from FUNCT_2:sch 3( A1);

        take GG;

        thus thesis by A3;

      end;

      uniqueness

      proof

        let G1,G2 be sequence of ExtREAL such that

         A4: for n be Element of NAT holds (n in S implies (G1 . n) = (H . n)) & (( not n in S) implies (G1 . n) = 0. ) and

         A5: for n be Element of NAT holds (n in S implies (G2 . n) = (H . n)) & (( not n in S) implies (G2 . n) = 0. );

        for n be object st n in NAT holds (G1 . n) = (G2 . n)

        proof

          let n be object;

          assume n in NAT ;

          then

          reconsider n as Element of NAT ;

          per cases ;

            suppose

             A6: n in S;

            then (G1 . n) = (H . n) by A4;

            hence thesis by A5, A6;

          end;

            suppose

             A7: not n in S;

            then (G1 . n) = 0. by A4;

            hence thesis by A5, A7;

          end;

        end;

        hence thesis by FUNCT_2: 12;

      end;

    end

    theorem :: MEASURE7:7

    

     Th7: for X be non empty set holds for G be Function of X, ExtREAL st G is nonnegative holds ( On G) is nonnegative

    proof

      let X be non empty set;

      let G be Function of X, ExtREAL ;

      assume

       A1: G is nonnegative;

      for n be Element of NAT holds 0. <= (( On G) . n)

      proof

        let n be Element of NAT ;

        per cases ;

          suppose

           A2: n in X;

          then (( On G) . n) = (G . n) by Def1;

          hence thesis by A1, A2, SUPINF_2: 39;

        end;

          suppose not n in X;

          hence thesis by Def1;

        end;

      end;

      hence thesis by SUPINF_2: 39;

    end;

    theorem :: MEASURE7:8

    

     Th8: for F be sequence of ExtREAL st F is nonnegative holds for n,k be Nat st n <= k holds (( Ser F) . n) <= (( Ser F) . k)

    proof

      let F be sequence of ExtREAL ;

      assume

       A1: F is nonnegative;

      let n,k be Nat;

      defpred P[ Nat] means (( Ser F) . n) <= (( Ser F) . (n + $1));

      

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

      proof

        let k be Nat;

        assume

         A3: (( Ser F) . n) <= (( Ser F) . (n + k));

        (( Ser F) . (n + k)) <= (( Ser F) . ((n + k) + 1)) by A1, SUPINF_2: 40;

        hence thesis by A3, XXREAL_0: 2;

      end;

      assume n <= k;

      then

      consider s be Nat such that

       A4: k = (n qua Complex + s) by NAT_1: 10;

      

       A5: k = (n + s) by A4;

      

       A6: P[ 0 ];

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

      hence thesis by A5;

    end;

    theorem :: MEASURE7:9

    

     Th9: for k be Nat holds for F be sequence of ExtREAL holds ((for n be Element of NAT st n <> k holds (F . n) = 0. ) implies (for n be Element of NAT st n < k holds (( Ser F) . n) = 0. ) & for n be Element of NAT st k <= n holds (( Ser F) . n) = (F . k))

    proof

      let k be Nat;

      let F be sequence of ExtREAL ;

      defpred P[ Nat] means $1 < k implies (( Ser F) . $1) = 0. ;

      assume

       A1: for n be Element of NAT st n <> k holds (F . n) = 0. ;

      

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

      proof

        let n be Nat;

        assume

         A3: n < k implies (( Ser F) . n) = 0. ;

        assume

         A4: (n + 1) < k;

        then

         A5: n <= (n + 1) & (F . (n + 1)) = 0. by A1, NAT_1: 11;

        (( Ser F) . (n + 1)) = ((( Ser F) . n) + (F . (n + 1))) by SUPINF_2:def 11

        .= 0. by A3, A4, A5, XXREAL_0: 2;

        hence thesis;

      end;

      

       A6: P[ 0 ]

      proof

        assume 0 < k;

        then (F . 0 ) = 0. by A1;

        hence thesis by SUPINF_2:def 11;

      end;

      

       A7: for n be Nat holds P[n] from NAT_1:sch 2( A6, A2);

      defpred P[ Nat] means k <= $1 implies (( Ser F) . $1) = (F . k);

      

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

      proof

        let n be Nat;

        assume

         A9: k <= n implies (( Ser F) . n) = (F . k);

        assume

         A10: k <= (n + 1);

        per cases by A10, NAT_1: 8;

          suppose

           A11: k <= n;

          then k <> (n + 1) by NAT_1: 13;

          then

           A12: (F . (n + 1)) = 0. by A1;

          (( Ser F) . (n + 1)) = ((( Ser F) . n) + (F . (n + 1))) by SUPINF_2:def 11

          .= (F . k) by A9, A11, A12, XXREAL_3: 4;

          hence thesis;

        end;

          suppose

           A13: k = (n + 1);

          then n < k by NAT_1: 13;

          then

           A14: (( Ser F) . n) = 0. by A7;

          (( Ser F) . (n + 1)) = ((( Ser F) . n) + (F . (n + 1))) by SUPINF_2:def 11

          .= (F . k) by A13, A14, XXREAL_3: 4;

          hence thesis;

        end;

      end;

      

       A15: P[ 0 ]

      proof

        

         A16: 0 <= k by NAT_1: 2;

        assume k <= 0 ;

        then (F . 0 ) = (F . k) by A16, XXREAL_0: 1;

        hence thesis by SUPINF_2:def 11;

      end;

      for n be Nat holds P[n] from NAT_1:sch 2( A15, A8);

      hence thesis by A7;

    end;

    theorem :: MEASURE7:10

    

     Th10: for G be sequence of ExtREAL st G is nonnegative holds for S be non empty Subset of NAT holds for H be Function of S, NAT st H is one-to-one holds ( SUM ( On (G * H))) <= ( SUM G)

    proof

      let G be sequence of ExtREAL ;

      assume

       A1: G is nonnegative;

      let S be non empty Subset of NAT ;

      let H be Function of S, NAT ;

      defpred P[ Nat] means ex m be Element of NAT st for F be sequence of ExtREAL st F is nonnegative holds (( Ser ( On (F * H))) . $1) <= (( Ser F) . m);

      assume

       A2: H is one-to-one;

      

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

      proof

        let k be Nat;

        given m0 be Element of NAT such that

         A4: for F be sequence of ExtREAL st F is nonnegative holds (( Ser ( On (F * H))) . k) <= (( Ser F) . m0);

        per cases ;

          suppose

           A5: (k + 1) in S;

          reconsider m1 = (H . (k + 1)) as Element of NAT ;

          set m = (m0 + m1);

          take m;

          let F be sequence of ExtREAL ;

          defpred QQ0[ Element of NAT , Element of ExtREAL ] means (($1 = (H . (k + 1)) implies $2 = (F . $1)) & ($1 <> (H . (k + 1)) implies $2 = 0. ));

          

           A6: for n be Element of NAT holds ex y be Element of ExtREAL st QQ0[n, y]

          proof

            let n be Element of NAT ;

            per cases ;

              suppose

               A7: n = (H . (k + 1));

              take (F . n);

              thus thesis by A7;

            end;

              suppose

               A8: n <> (H . (k + 1));

              take 0. ;

              thus thesis by A8;

            end;

          end;

          consider G0 be sequence of ExtREAL such that

           A9: for n be Element of NAT holds QQ0[n, (G0 . n)] from FUNCT_2:sch 3( A6);

          reconsider GG0 = ( On (G0 * H)) as sequence of ExtREAL ;

          

           A10: for n be Element of NAT holds n <> (k + 1) implies (GG0 . n) = 0.

          proof

            let n be Element of NAT ;

            assume

             A11: n <> (k + 1);

            per cases ;

              suppose

               A12: n in S;

              

              then

               A13: (GG0 . n) = ((G0 * H) . n) by Def1

              .= (G0 . (H . n)) by A12, FUNCT_2: 15;

              reconsider n as Element of S by A12;

               not (H . n) = (H . (k + 1)) by A2, A5, A11, FUNCT_2: 19;

              hence thesis by A9, A13;

            end;

              suppose not n in S;

              hence thesis by Def1;

            end;

          end;

          assume

           A14: F is nonnegative;

          for n be Element of NAT holds 0. <= (G0 . n)

          proof

            let n be Element of NAT ;

            per cases ;

              suppose n = (H . (k + 1));

              then (G0 . n) = (F . n) by A9;

              hence thesis by A14, SUPINF_2: 39;

            end;

              suppose not n = (H . (k + 1));

              hence thesis by A9;

            end;

          end;

          then

           A15: G0 is nonnegative by SUPINF_2: 39;

          reconsider n = (k + 1) as Element of S by A5;

          defpred QQ1[ Element of NAT , Element of ExtREAL ] means (($1 <> (H . (k + 1)) implies $2 = (F . $1)) & ($1 = (H . (k + 1)) implies $2 = 0. ));

          

           A16: for n be Element of NAT holds ex y be Element of ExtREAL st QQ1[n, y]

          proof

            let n be Element of NAT ;

            per cases ;

              suppose

               A17: n <> (H . (k + 1));

              take (F . n);

              thus thesis by A17;

            end;

              suppose

               A18: n = (H . (k + 1));

              take 0. ;

              thus thesis by A18;

            end;

          end;

          consider G1 be sequence of ExtREAL such that

           A19: for n be Element of NAT holds QQ1[n, (G1 . n)] from FUNCT_2:sch 3( A16);

          set GG1 = ( On (G1 * H));

          

           A20: (GG1 . (k + 1)) = ((G1 * H) . n) by Def1

          .= (G1 . (H . n)) by FUNCT_2: 15

          .= 0. by A19;

          

           A21: (GG0 . n) = ((G0 * H) . n) by Def1

          .= (G0 . (H . n)) by FUNCT_2: 15

          .= (F . (H . n)) by A9;

          then

           A22: (( Ser GG0) . (k + 1)) = (F . (H . (k + 1))) by A10, Th9;

          

           A23: for n be Element of NAT holds n <> (k + 1) & n in S implies (GG1 . n) = (F . (H . n))

          proof

            let n be Element of NAT ;

            assume that

             A24: n <> (k + 1) and

             A25: n in S;

            

             A26: (GG1 . n) = ((G1 * H) . n) by A25, Def1

            .= (G1 . (H . n)) by A25, FUNCT_2: 15;

            reconsider n as Element of S by A25;

             not (H . n) = (H . (k + 1)) by A2, A5, A24, FUNCT_2: 19;

            hence thesis by A19, A26;

          end;

          

           A27: for n be Element of NAT holds (( On (F * H)) . n) = ((GG0 . n) + (GG1 . n))

          proof

            let n be Element of NAT ;

            per cases ;

              suppose

               A28: n = (k + 1);

              

              then (( On (F * H)) . n) = ((F * H) . n) by A5, Def1

              .= (F . (H . n)) by A5, A28, FUNCT_2: 15

              .= ((GG0 . n) + (GG1 . n)) by A21, A20, A28, XXREAL_3: 4;

              hence thesis;

            end;

              suppose

               A29: n <> (k + 1);

              now

                per cases ;

                  suppose

                   A30: n in S;

                  then

                   A31: (GG1 . n) = (F . (H . n)) by A23, A29;

                  

                   A32: (GG0 . n) = 0. by A10, A29;

                  (( On (F * H)) . n) = ((F * H) . n) by A30, Def1

                  .= (F . (H . n)) by A30, FUNCT_2: 15

                  .= ((GG0 . n) + (GG1 . n)) by A32, A31, XXREAL_3: 4;

                  hence thesis;

                end;

                  suppose

                   A33: not n in S;

                  then

                   A34: (GG1 . n) = 0. by Def1;

                  

                   A35: (GG0 . n) = 0. by A10, A29;

                  (( On (F * H)) . n) = 0. by A33, Def1

                  .= ((GG0 . n) + (GG1 . n)) by A35, A34;

                  hence thesis;

                end;

              end;

              hence thesis;

            end;

          end;

          m1 <= m by NAT_1: 11;

          then

           A36: (( Ser G0) . m) = (G0 . (H . (k + 1))) by A9, Th9;

          set v = (H . n);

          

           A37: (( Ser GG1) . (k + 1)) = ((( Ser GG1) . k) + (GG1 . (k + 1))) by SUPINF_2:def 11

          .= (( Ser ( On (G1 * H))) . k) by A20, XXREAL_3: 4;

          

           A38: (G0 . v) = (F . v) by A9;

          for n be Element of NAT holds 0. <= (G1 . n)

          proof

            let n be Element of NAT ;

            per cases ;

              suppose n <> (H . (k + 1));

              then (G1 . n) = (F . n) by A19;

              hence thesis by A14, SUPINF_2: 39;

            end;

              suppose n = (H . (k + 1));

              hence thesis by A19;

            end;

          end;

          then

           A39: G1 is nonnegative by SUPINF_2: 39;

          then (G1 * H) is nonnegative by MEASURE1: 25;

          then

           A40: GG1 is nonnegative by Th7;

          (G0 * H) is nonnegative by A15, MEASURE1: 25;

          then GG0 is nonnegative by Th7;

          then

           A41: (( Ser ( On (F * H))) . (k + 1)) = ((( Ser GG0) . (k + 1)) + (( Ser GG1) . (k + 1))) by A40, A27, Th3;

          (( Ser ( On (G1 * H))) . k) <= (( Ser G1) . m0) & (( Ser G1) . m0) <= (( Ser G1) . m) by A4, A39, Th8, NAT_1: 11;

          then

           A42: (( Ser GG1) . (k + 1)) <= (( Ser G1) . m) by A37, XXREAL_0: 2;

          for m be Element of NAT holds (F . m) = ((G0 . m) + (G1 . m))

          proof

            let m be Element of NAT ;

            per cases ;

              suppose m = (H . (k + 1));

              then (G0 . m) = (F . m) & (G1 . m) = 0. by A9, A19;

              hence thesis by XXREAL_3: 4;

            end;

              suppose m <> (H . (k + 1));

              then (G0 . m) = 0. & (G1 . m) = (F . m) by A9, A19;

              hence thesis by XXREAL_3: 4;

            end;

          end;

          then (( Ser F) . m) = ((( Ser G0) . m) + (( Ser G1) . m)) by A15, A39, Th3;

          hence thesis by A22, A36, A38, A42, A41, XXREAL_3: 36;

        end;

          suppose

           A43: not (k + 1) in S;

          take m0;

          let F be sequence of ExtREAL ;

          

           A44: (( On (F * H)) . (k + 1)) = 0. by A43, Def1;

          assume

           A45: F is nonnegative;

          (( Ser ( On (F * H))) . (k + 1)) = ((( Ser ( On (F * H))) . k) + (( On (F * H)) . (k + 1))) by SUPINF_2:def 11

          .= (( Ser ( On (F * H))) . k) by A44, XXREAL_3: 4;

          hence thesis by A4, A45;

        end;

      end;

      

       A46: P[ 0 ]

      proof

        per cases ;

          suppose

           A47: 0 in S;

          reconsider m = (H . 0 ) as Element of NAT ;

          take m;

          let F be sequence of ExtREAL ;

          (( Ser ( On (F * H))) . 0 ) = (( On (F * H)) . 0 ) by SUPINF_2:def 11;

          

          then

           A48: (( Ser ( On (F * H))) . 0 ) = ((F * H) . 0 ) by A47, Def1

          .= (F . (H . 0 )) by A47, FUNCT_2: 15;

          assume F is nonnegative;

          hence thesis by A48, Th2;

        end;

          suppose

           A49: not 0 in S;

          take m = 0 ;

          let F be sequence of ExtREAL ;

          assume F is nonnegative;

          then

           A50: 0. <= (F . 0 ) & (F . 0 ) <= (( Ser F) . m) by Th2, SUPINF_2: 39;

          (( Ser ( On (F * H))) . 0 ) = (( On (F * H)) . 0 ) by SUPINF_2:def 11;

          then (( Ser ( On (F * H))) . 0 ) = 0. by A49, Def1;

          hence thesis by A50, XXREAL_0: 2;

        end;

      end;

      

       A51: for k be Nat holds P[k] from NAT_1:sch 2( A46, A3);

      for x be ExtReal st x in ( rng ( Ser ( On (G * H)))) holds ex y be ExtReal st y in ( rng ( Ser G)) & x <= y

      proof

        let x be ExtReal;

        assume

         A52: x in ( rng ( Ser ( On (G * H))));

        ex y be ExtReal st y in ( rng ( Ser G)) & x <= y

        proof

          consider n be object such that

           A53: n in ( dom ( Ser ( On (G * H)))) and

           A54: x = (( Ser ( On (G * H))) . n) by A52, FUNCT_1:def 3;

          reconsider n as Element of NAT by A53;

          consider m be Element of NAT such that

           A55: for F be sequence of ExtREAL st F is nonnegative holds (( Ser ( On (F * H))) . n) <= (( Ser F) . m) by A51;

          take (( Ser G) . m);

          ( dom ( Ser G)) = NAT by FUNCT_2:def 1;

          hence thesis by A1, A54, A55, FUNCT_1:def 3;

        end;

        hence thesis;

      end;

      then ( sup ( rng ( Ser ( On (G * H))))) <= ( sup ( rng ( Ser G))) by XXREAL_2: 63;

      hence thesis;

    end;

    theorem :: MEASURE7:11

    

     Th11: for F,G be sequence of ExtREAL st G is nonnegative holds for S be non empty Subset of NAT holds for H be Function of S, NAT st H is one-to-one holds (for k be Element of NAT holds ((k in S implies (F . k) = ((G * H) . k)) & (( not k in S) implies (F . k) = 0. ))) implies ( SUM F) <= ( SUM G)

    proof

      let F,G be sequence of ExtREAL ;

      assume

       A1: G is nonnegative;

      let S be non empty Subset of NAT ;

      let H be Function of S, NAT ;

      assume

       A2: H is one-to-one;

      assume for k be Element of NAT holds (k in S implies (F . k) = ((G * H) . k)) & (( not k in S) implies (F . k) = 0. );

      then F = ( On (G * H)) by Def1;

      hence thesis by A1, A2, Th10;

    end;

     REAL in ( bool REAL ) by ZFMISC_1:def 1;

    then

    reconsider G0 = ( NAT --> REAL ) as sequence of ( bool REAL ) by FUNCOP_1: 45;

    

     Lm1: ( rng G0) = { REAL } by FUNCOP_1: 8;

    then

     Lm2: REAL c= ( union ( rng G0)) by ZFMISC_1: 25;

    

     Lm3: for n be Element of NAT holds (G0 . n) is Interval

    proof

      let n be Element of NAT ;

      (G0 . n) in { REAL } by Lm1, FUNCT_2: 4;

      hence thesis by TARSKI:def 1;

    end;

    definition

      let A be Subset of REAL ;

      :: MEASURE7:def2

      mode Interval_Covering of A -> sequence of ( bool REAL ) means

      : Def2: A c= ( union ( rng it )) & for n be Element of NAT holds (it . n) is Interval;

      existence by Lm2, Lm3, XBOOLE_1: 1;

    end

    definition

      let A be Subset of REAL ;

      let F be Interval_Covering of A;

      let n be Element of NAT ;

      :: original: .

      redefine

      func F . n -> Interval ;

      correctness by Def2;

    end

    definition

      let F be sequence of ( bool REAL );

      :: MEASURE7:def3

      mode Interval_Covering of F -> sequence of ( Funcs ( NAT ,( bool REAL ))) means

      : Def3: for n be Element of NAT holds (it . n) is Interval_Covering of (F . n);

      existence

      proof

        reconsider G = G0 as Element of ( Funcs ( NAT ,( bool REAL ))) by FUNCT_2: 8;

        reconsider H = ( NAT --> G) as sequence of ( Funcs ( NAT ,( bool REAL )));

        take H;

        

         A1: for n be Element of NAT holds G0 is Interval_Covering of (F . n) by Lm2, XBOOLE_1: 1, Def2, Lm3;

        for n be Element of NAT holds (H . n) is Interval_Covering of (F . n)

        proof

          let n be Element of NAT ;

          (H . n) = G by FUNCOP_1: 7;

          hence thesis by A1;

        end;

        hence thesis;

      end;

    end

    definition

      let A be Subset of REAL ;

      let F be Interval_Covering of A;

      deffunc F( Element of NAT ) = ( diameter (F . $1));

      :: MEASURE7:def4

      func F vol -> sequence of ExtREAL means

      : Def4: for n be Element of NAT holds (it . n) = ( diameter (F . n));

      existence

      proof

        thus ex G be sequence of ExtREAL st for n be Element of NAT holds (G . n) = F(n) from FUNCT_2:sch 4;

      end;

      uniqueness

      proof

        thus for G1,G2 be sequence of ExtREAL st (for n be Element of NAT holds (G1 . n) = F(n)) & (for n be Element of NAT holds (G2 . n) = F(n)) holds G1 = G2 from BINOP_2:sch 1;

      end;

    end

    theorem :: MEASURE7:12

    

     Th12: for A be Subset of REAL holds for F be Interval_Covering of A holds (F vol ) is nonnegative

    proof

      let A be Subset of REAL ;

      let F be Interval_Covering of A;

      for n be Element of NAT holds 0. <= ((F vol ) . n)

      proof

        let n be Element of NAT ;

        ((F vol ) . n) = ( diameter (F . n)) by Def4;

        hence thesis by MEASURE5: 13;

      end;

      hence thesis by SUPINF_2: 39;

    end;

    definition

      let F be sequence of ( bool REAL );

      let H be Interval_Covering of F;

      let n be Element of NAT ;

      :: original: .

      redefine

      func H . n -> Interval_Covering of (F . n) ;

      correctness by Def3;

    end

    definition

      let F be sequence of ( bool REAL );

      let G be Interval_Covering of F;

      :: MEASURE7:def5

      func G vol -> sequence of ( Funcs ( NAT , ExtREAL )) means for n be Element of NAT holds (it . n) = ((G . n) vol );

      existence

      proof

        defpred P[ Element of NAT , set] means $2 = ((G . $1) vol );

        

         A1: for n be Element of NAT holds ex y be Element of ( Funcs ( NAT , ExtREAL )) st P[n, y]

        proof

          let n be Element of NAT ;

          ((G . n) vol ) is Element of ( Funcs ( NAT , ExtREAL )) by FUNCT_2: 8;

          hence thesis;

        end;

        ex G0 be sequence of ( Funcs ( NAT , ExtREAL )) st for n be Element of NAT holds P[n, (G0 . n)] from FUNCT_2:sch 3( A1);

        hence thesis;

      end;

      uniqueness

      proof

        deffunc F( Element of NAT ) = ((G . $1) vol );

        thus for F1,F2 be sequence of ( Funcs ( NAT , ExtREAL )) st (for n be Element of NAT holds (F1 . n) = F(n)) & (for n be Element of NAT holds (F2 . n) = F(n)) holds F1 = F2 from BINOP_2:sch 1;

      end;

    end

    definition

      let A be Subset of REAL ;

      let F be Interval_Covering of A;

      :: MEASURE7:def6

      func vol F -> R_eal equals ( SUM (F vol ));

      correctness ;

    end

    definition

      let F be sequence of ( bool REAL );

      let G be Interval_Covering of F;

      :: MEASURE7:def7

      func vol (G) -> sequence of ExtREAL means

      : Def7: for n be Element of NAT holds (it . n) = ( vol (G . n));

      existence

      proof

        defpred P[ Element of NAT , Element of ExtREAL ] means $2 = ( vol (G . $1));

        

         A1: for n be Element of NAT holds ex y be Element of ExtREAL st P[n, y];

        consider G0 be sequence of ExtREAL such that

         A2: for n be Element of NAT holds P[n, (G0 . n)] from FUNCT_2:sch 3( A1);

        take G0;

        thus thesis by A2;

      end;

      uniqueness

      proof

        deffunc F( Element of NAT ) = ( vol (G . $1));

        thus for F1,F2 be sequence of ExtREAL st (for n be Element of NAT holds (F1 . n) = F(n)) & (for n be Element of NAT holds (F2 . n) = F(n)) holds F1 = F2 from BINOP_2:sch 1;

      end;

    end

    theorem :: MEASURE7:13

    

     Th13: for F be sequence of ( bool REAL ) holds for G be Interval_Covering of F holds for n be Element of NAT holds 0. <= (( vol G) . n)

    proof

      let F be sequence of ( bool REAL );

      let G be Interval_Covering of F;

      let n be Element of NAT ;

      for k be Element of NAT holds 0. <= (((G . n) vol ) . k)

      proof

        let k be Element of NAT ;

         0. <= ( diameter ((G . n) . k)) by MEASURE5: 13;

        hence thesis by Def4;

      end;

      then

       A1: ((G . n) vol ) is nonnegative by SUPINF_2: 39;

      (( vol G) . n) = ( vol (G . n)) by Def7;

      hence thesis by A1, MEASURE6: 2;

    end;

    definition

      let A be Subset of REAL ;

      defpred P[ object] means ex F be Interval_Covering of A st $1 = ( vol F);

      :: MEASURE7:def8

      func Svc (A) -> Subset of ExtREAL means

      : Def8: for x be R_eal holds x in it iff ex F be Interval_Covering of A st x = ( vol F);

      existence

      proof

        consider D be set such that

         A1: for x be object holds x in D iff x in ExtREAL & P[x] from XBOOLE_0:sch 1;

        for z be object holds z in D implies z in ExtREAL by A1;

        then

        reconsider D as Subset of ExtREAL by TARSKI:def 3;

        take D;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let D1,D2 be Subset of ExtREAL such that

         A2: for x be R_eal holds x in D1 iff P[x] and

         A3: for x be R_eal holds x in D2 iff P[x];

        thus D1 = D2 from SUBSET_1:sch 2( A2, A3);

      end;

    end

    registration

      let A be Subset of REAL ;

      cluster ( Svc A) -> non empty;

      coherence

      proof

         REAL c= REAL ;

        then

        consider F0 be sequence of ( bool REAL ) such that

         A1: ( rng F0) = { REAL , ( {} REAL )} and

         A2: (F0 . 0 ) = REAL & for n be Nat st 0 < n holds (F0 . n) = ( {} REAL ) by MEASURE1: 19;

        ( union { REAL , {} }) = ( REAL \/ {} ) & for n be Element of NAT holds (F0 . n) is Interval by A2, NAT_1: 3, ZFMISC_1: 75;

        then

        reconsider F0 as Interval_Covering of A by A1, Def2;

        defpred P[ set] means ex F be Interval_Covering of A st $1 = ( vol F);

        consider D be set such that

         A3: for x be set holds x in D iff x in ExtREAL & P[x] from XFAMILY:sch 1;

        ( vol F0) in D by A3;

        hence thesis by Def8;

      end;

    end

    definition

      let A be Subset of REAL ;

      :: MEASURE7:def9

      func COMPLEX (A) -> Element of ExtREAL equals ( inf ( Svc A));

      correctness ;

    end

    definition

      :: MEASURE7:def10

      func OS_Meas -> Function of ( bool REAL ), ExtREAL means

      : Def10: for A be Subset of REAL holds (it . A) = ( inf ( Svc A));

      existence

      proof

        consider G be Function of ( bool REAL ), ExtREAL such that

         A1: for A be Subset of REAL holds (G . A) = ( COMPLEX A) from FUNCT_2:sch 4;

        take G;

        for A be Subset of REAL holds (G . A) = ( inf ( Svc A))

        proof

          let A be Subset of REAL ;

          (G . A) = ( COMPLEX A) by A1;

          hence thesis;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        deffunc F( Subset of REAL ) = ( inf ( Svc $1));

        thus for F1,F2 be Function of ( bool REAL ), ExtREAL st (for A be Subset of REAL holds (F1 . A) = F(A)) & (for A be Subset of REAL holds (F2 . A) = F(A)) holds F1 = F2 from BINOP_2:sch 1;

      end;

    end

    definition

      let F be sequence of ( bool REAL );

      let G be Interval_Covering of F;

      let H be sequence of [: NAT , NAT :];

      :: MEASURE7:def11

      func On (G,H) -> Interval_Covering of ( union ( rng F)) means

      : Def11: for n be Element of NAT holds (it . n) = ((G . (( pr1 H) . n)) . (( pr2 H) . n));

      existence

      proof

        defpred P[ Element of NAT , Subset of REAL ] means $2 = ((G . (( pr1 H) . $1)) . (( pr2 H) . $1));

        

         A2: for n be Element of NAT holds ex y be Subset of REAL st P[n, y];

        consider GG be sequence of ( bool REAL ) such that

         A3: for n be Element of NAT holds P[n, (GG . n)] from FUNCT_2:sch 3( A2);

        

         A4: ( union ( rng F)) c= ( union ( rng GG))

        proof

          let x be object;

          assume x in ( union ( rng F));

          then

          consider A be set such that

           A5: x in A and

           A6: A in ( rng F) by TARSKI:def 4;

          consider n1 be object such that

           A7: n1 in ( dom F) and

           A8: A = (F . n1) by A6, FUNCT_1:def 3;

          reconsider n1 as Element of NAT by A7;

          (F . n1) c= ( union ( rng (G . n1))) by Def2;

          then

          consider AA be set such that

           A9: x in AA and

           A10: AA in ( rng (G . n1)) by A5, A8, TARSKI:def 4;

          consider n2 be object such that

           A11: n2 in ( dom (G . n1)) and

           A12: AA = ((G . n1) . n2) by A10, FUNCT_1:def 3;

          reconsider n2 as Element of NAT by A11;

          consider n be object such that

           A13: n in ( dom H) and

           A14: [n1, n2] = (H . n) by A1, FUNCT_1:def 3;

          reconsider n as Element of NAT by A13;

           [(( pr1 H) . n), (( pr2 H) . n)] = [n1, n2] by A14, FUNCT_2: 119;

          then (( pr1 H) . n) = n1 & (( pr2 H) . n) = n2 by XTUPLE_0: 1;

          then

           A15: x in (GG . n) by A3, A9, A12;

          (GG . n) in ( rng GG) by FUNCT_2: 4;

          hence thesis by A15, TARSKI:def 4;

        end;

        for n be Element of NAT holds (GG . n) is Interval

        proof

          let n be Element of NAT ;

          (GG . n) = ((G . (( pr1 H) . n)) . (( pr2 H) . n)) by A3;

          hence thesis;

        end;

        then

        reconsider GG as Interval_Covering of ( union ( rng F)) by A4, Def2;

        take GG;

        thus thesis by A3;

      end;

      uniqueness

      proof

        let G1,G2 be Interval_Covering of ( union ( rng F)) such that

         A16: for n be Element of NAT holds (G1 . n) = ((G . (( pr1 H) . n)) . (( pr2 H) . n)) and

         A17: for n be Element of NAT holds (G2 . n) = ((G . (( pr1 H) . n)) . (( pr2 H) . n));

        for n be object st n in NAT holds (G1 . n) = (G2 . n)

        proof

          let n be object;

          assume n in NAT ;

          then

          reconsider n as Element of NAT ;

          (G1 . n) = ((G . (( pr1 H) . n)) . (( pr2 H) . n)) by A16;

          hence thesis by A17;

        end;

        hence thesis by FUNCT_2: 12;

      end;

    end

    reconsider D = ( NAT --> ( {} REAL )) as sequence of ( bool REAL );

    theorem :: MEASURE7:14

    

     Th14: for H be sequence of [: NAT , NAT :] st H is one-to-one & ( rng H) = [: NAT , NAT :] holds for k be Nat holds ex m be Element of NAT st for F be sequence of ( bool REAL ) holds for G be Interval_Covering of F holds (( Ser (( On (G,H)) vol )) . k) <= (( Ser ( vol G)) . m)

    proof

      reconsider y = D as Element of ( Funcs ( NAT ,( bool REAL ))) by FUNCT_2: 8;

      let H be sequence of [: NAT , NAT :];

      assume that

       A1: H is one-to-one and

       A2: ( rng H) = [: NAT , NAT :];

      defpred P[ Nat] means ex m be Element of NAT st for F be sequence of ( bool REAL ) holds for G be Interval_Covering of F holds (( Ser (( On (G,H)) vol )) . $1) <= (( Ser ( vol G)) . m);

      

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

      proof

        let k be Nat;

        set N0 = { s where s be Element of NAT : (( pr1 H) . (k + 1)) = (( pr1 H) . s) };

        

         A4: N0 c= NAT

        proof

          let s1 be object;

          assume s1 in N0;

          then ex s be Element of NAT st s = s1 & (( pr1 H) . (k + 1)) = (( pr1 H) . s);

          hence thesis;

        end;

        (k + 1) in N0;

        then

        reconsider N0 as non empty Subset of NAT by A4;

        given m0 be Element of NAT such that

         A5: for F be sequence of ( bool REAL ) holds for G be Interval_Covering of F holds (( Ser (( On (G,H)) vol )) . k) <= (( Ser ( vol G)) . m0);

        take m = (m0 + (( pr1 H) . (k + 1)));

        let F be sequence of ( bool REAL );

        let G be Interval_Covering of F;

        defpred QQ1[ Element of NAT , Function] means (($1 <> (( pr1 H) . (k + 1)) implies for m be Element of NAT holds ($2 . m) = ((G . $1) . m)) & ($1 = (( pr1 H) . (k + 1)) implies for m be Element of NAT holds ($2 . m) = {} ));

        

         A6: for n be Element of NAT holds ex y be Element of ( Funcs ( NAT ,( bool REAL ))) st QQ1[n, y]

        proof

          let n be Element of NAT ;

          per cases ;

            suppose

             A7: n <> (( pr1 H) . (k + 1));

            reconsider y = (G . n) as Element of ( Funcs ( NAT ,( bool REAL ))) by FUNCT_2: 8;

            take y;

            thus thesis by A7;

          end;

            suppose

             A8: n = (( pr1 H) . (k + 1));

            take y;

            thus thesis by A8, FUNCOP_1: 7;

          end;

        end;

        consider G1 be sequence of ( Funcs ( NAT ,( bool REAL ))) such that

         A9: for n be Element of NAT holds QQ1[n, (G1 . n)] from FUNCT_2:sch 3( A6);

        

         A10: for n be Element of NAT holds (G1 . n) is Interval_Covering of (D . n)

        proof

          let n be Element of NAT ;

          consider f0 be Function such that

           A11: (G1 . n) = f0 and

           A12: ( dom f0) = NAT & ( rng f0) c= ( bool REAL ) by FUNCT_2:def 2;

          reconsider f0 as sequence of ( bool REAL ) by A12, FUNCT_2: 2;

          

           A13: for s be Element of NAT holds (f0 . s) is Interval

          proof

            let s be Element of NAT ;

            per cases ;

              suppose n <> (( pr1 H) . (k + 1));

              then (f0 . s) = ((G . n) . s) by A9, A11;

              hence thesis;

            end;

              suppose n = (( pr1 H) . (k + 1));

              hence thesis by A9, A11;

            end;

          end;

          (D . n) = {} by FUNCOP_1: 7;

          then (D . n) c= ( union ( rng f0));

          then

          reconsider f0 as Interval_Covering of (D . n) by A13, Def2;

          (G1 . n) = f0 by A11;

          hence thesis;

        end;

        defpred SSS[ Element of N0, Element of NAT ] means $2 = (( pr2 H) . $1);

        defpred QQ0[ Element of NAT , Function] means (($1 = (( pr1 H) . (k + 1)) implies for m be Element of NAT holds ($2 . m) = ((G . $1) . m)) & ($1 <> (( pr1 H) . (k + 1)) implies for m be Element of NAT holds ($2 . m) = {} ));

        

         A14: for n be Element of NAT holds ex y be Element of ( Funcs ( NAT ,( bool REAL ))) st QQ0[n, y]

        proof

          let n be Element of NAT ;

          per cases ;

            suppose

             A15: n = (( pr1 H) . (k + 1));

            reconsider y = (G . n) as Element of ( Funcs ( NAT ,( bool REAL ))) by FUNCT_2: 8;

            take y;

            thus thesis by A15;

          end;

            suppose

             A16: n <> (( pr1 H) . (k + 1));

            take y;

            thus thesis by A16, FUNCOP_1: 7;

          end;

        end;

        consider G0 be sequence of ( Funcs ( NAT ,( bool REAL ))) such that

         A17: for n be Element of NAT holds QQ0[n, (G0 . n)] from FUNCT_2:sch 3( A14);

        for n be Element of NAT holds (G0 . n) is Interval_Covering of (D . n)

        proof

          let n be Element of NAT ;

          consider f0 be Function such that

           A18: (G0 . n) = f0 and

           A19: ( dom f0) = NAT & ( rng f0) c= ( bool REAL ) by FUNCT_2:def 2;

          reconsider f0 as sequence of ( bool REAL ) by A19, FUNCT_2: 2;

          

           A20: for s be Element of NAT holds (f0 . s) is Interval

          proof

            let s be Element of NAT ;

            per cases ;

              suppose n = (( pr1 H) . (k + 1));

              then (f0 . s) = ((G . n) . s) by A17, A18;

              hence thesis;

            end;

              suppose n <> (( pr1 H) . (k + 1));

              hence thesis by A17, A18;

            end;

          end;

          (D . n) = {} by FUNCOP_1: 7;

          then (D . n) c= ( union ( rng f0));

          then

          reconsider f0 as Interval_Covering of (D . n) by A20, Def2;

          (G0 . n) = f0 by A18;

          hence thesis;

        end;

        then

        reconsider G0 as Interval_Covering of D by Def3;

        set GG0 = ( On (G0,H));

        reconsider G1 as Interval_Covering of D by A10, Def3;

        set GG1 = ( On (G1,H));

        

         A21: (( Ser (GG0 vol )) . (k + 1)) <= ( SUM (GG0 vol )) by Th6, Th12;

        (GG1 . (k + 1)) = ((G1 . (( pr1 H) . (k + 1))) . (( pr2 H) . (k + 1))) by A2, Def11

        .= {} by A9;

        then

         A22: ((GG1 vol ) . (k + 1)) = 0. by Def4, MEASURE5: 10;

        (( Ser (GG1 vol )) . (k + 1)) = ((( Ser (GG1 vol )) . k) + ((GG1 vol ) . (k + 1))) by SUPINF_2:def 11;

        then

         A23: (( Ser (GG1 vol )) . (k + 1)) = (( Ser (GG1 vol )) . k) by A22, XXREAL_3: 4;

        for s be Element of NAT holds 0. <= (( vol G1) . s) by Th13;

        then ( vol G1) is nonnegative by SUPINF_2: 39;

        then

         A24: (( Ser ( vol G1)) . m0) <= (( Ser ( vol G1)) . m) by SUPINF_2: 41;

        

         A25: for n be Element of NAT holds ((( On (G,H)) vol ) . n) = (((GG0 vol ) . n) + ((GG1 vol ) . n))

        proof

          let n be Element of NAT ;

          

           A26: ((GG0 vol ) . n) = ( diameter (GG0 . n)) & ((GG1 vol ) . n) = ( diameter (GG1 . n)) by Def4;

          ((( On (G,H)) vol ) . n) = ( diameter (( On (G,H)) . n)) by Def4;

          then

           A27: ((( On (G,H)) vol ) . n) = ( diameter ((G . (( pr1 H) . n)) . (( pr2 H) . n))) by A2, Def11;

          per cases ;

            suppose

             A28: (( pr1 H) . n) = (( pr1 H) . (k + 1));

            

             A29: (GG1 . n) = ((G1 . (( pr1 H) . n)) . (( pr2 H) . n)) by A2, Def11

            .= {} by A9, A28;

            (GG0 . n) = ((G0 . (( pr1 H) . n)) . (( pr2 H) . n)) by A2, Def11

            .= ((G . (( pr1 H) . n)) . (( pr2 H) . n)) by A17, A28;

            hence thesis by A26, A27, A29, MEASURE5: 10, XXREAL_3: 4;

          end;

            suppose

             A30: (( pr1 H) . n) <> (( pr1 H) . (k + 1));

            

             A31: (GG0 . n) = ((G0 . (( pr1 H) . n)) . (( pr2 H) . n)) by A2, Def11

            .= {} by A17, A30;

            (GG1 . n) = ((G1 . (( pr1 H) . n)) . (( pr2 H) . n)) by A2, Def11

            .= ((G . (( pr1 H) . n)) . (( pr2 H) . n)) by A9, A30;

            hence thesis by A26, A27, A31, MEASURE5: 10, XXREAL_3: 4;

          end;

        end;

        (GG0 vol ) is nonnegative & (GG1 vol ) is nonnegative by Th12;

        then

         A32: (( Ser (( On (G,H)) vol )) . (k + 1)) = ((( Ser (GG0 vol )) . (k + 1)) + (( Ser (GG1 vol )) . (k + 1))) by A25, Th3;

        for s be Element of NAT holds 0. <= (( vol G1) . s) by Th13;

        then

         A33: ( vol G1) is nonnegative by SUPINF_2: 39;

        (( Ser (GG1 vol )) . k) <= (( Ser ( vol G1)) . m0) by A5;

        then

         A34: (( Ser (GG1 vol )) . (k + 1)) <= (( Ser ( vol G1)) . m) by A23, A24, XXREAL_0: 2;

        

         A35: for s be Element of N0 holds ex y be Element of NAT st SSS[s, y];

        consider SOS be Function of N0, NAT such that

         A36: for s be Element of N0 holds SSS[s, (SOS . s)] from FUNCT_2:sch 3( A35);

        

         A37: for n be Element of NAT holds (( vol G) . n) = ((( vol G0) . n) + (( vol G1) . n))

        proof

          let n be Element of NAT ;

          

           A38: ( vol (G . n)) = (( vol (G0 . n)) + ( vol (G1 . n)))

          proof

            per cases ;

              suppose

               A39: n = (( pr1 H) . (k + 1));

              for s be Element of NAT holds (((G . n) vol ) . s) <= (((G0 . n) vol ) . s)

              proof

                let s be Element of NAT ;

                (((G0 . n) vol ) . s) = ( diameter ((G0 . n) . s)) by Def4

                .= ( diameter ((G . n) . s)) by A17, A39

                .= (((G . n) vol ) . s) by Def4;

                hence thesis;

              end;

              then

               A40: ( SUM ((G . n) vol )) <= ( SUM ((G0 . n) vol )) by SUPINF_2: 43;

              for s be Element of NAT holds (((G1 . n) vol ) . s) = 0.

              proof

                let s be Element of NAT ;

                ( diameter ((G1 . n) . s)) = 0. by A9, A39, MEASURE5: 10;

                hence thesis by Def4;

              end;

              then

               A41: ( SUM ((G1 . n) vol )) = 0. by Th1;

              for s be Element of NAT holds (((G0 . n) vol ) . s) <= (((G . n) vol ) . s)

              proof

                let s be Element of NAT ;

                (((G0 . n) vol ) . s) = ( diameter ((G0 . n) . s)) by Def4

                .= ( diameter ((G . n) . s)) by A17, A39

                .= (((G . n) vol ) . s) by Def4;

                hence thesis;

              end;

              then ( SUM ((G0 . n) vol )) <= ( SUM ((G . n) vol )) by SUPINF_2: 43;

              then ( SUM ((G . n) vol )) = ( SUM ((G0 . n) vol )) by A40, XXREAL_0: 1;

              hence thesis by A41, XXREAL_3: 4;

            end;

              suppose

               A42: n <> (( pr1 H) . (k + 1));

              

               A43: for s be Element of NAT holds (((G1 . n) vol ) . s) = (((G . n) vol ) . s)

              proof

                let s be Element of NAT ;

                (((G1 . n) vol ) . s) = ( diameter ((G1 . n) . s)) & (((G . n) vol ) . s) = ( diameter ((G . n) . s)) by Def4;

                hence thesis by A9, A42;

              end;

              then for s be Element of NAT holds (((G . n) vol ) . s) <= (((G1 . n) vol ) . s);

              then

               A44: ( SUM ((G . n) vol )) <= ( SUM ((G1 . n) vol )) by SUPINF_2: 43;

              for s be Element of NAT holds (((G0 . n) vol ) . s) = 0.

              proof

                let s be Element of NAT ;

                ( diameter ((G0 . n) . s)) = 0. by A17, A42, MEASURE5: 10;

                hence thesis by Def4;

              end;

              then

               A45: ( SUM ((G0 . n) vol )) = 0. by Th1;

              for s be Element of NAT holds (((G1 . n) vol ) . s) <= (((G . n) vol ) . s) by A43;

              then ( SUM ((G1 . n) vol )) <= ( SUM ((G . n) vol )) by SUPINF_2: 43;

              then ( SUM ((G . n) vol )) = ( SUM ((G1 . n) vol )) by A44, XXREAL_0: 1;

              hence thesis by A45, XXREAL_3: 4;

            end;

          end;

          (( vol G) . n) = ( vol (G . n)) & (( vol G0) . n) = ( vol (G0 . n)) by Def7;

          hence thesis by A38, Def7;

        end;

        for s be Element of NAT holds 0. <= (( vol G0) . s) by Th13;

        then ( vol G0) is nonnegative by SUPINF_2: 39;

        then

         A46: (( vol G0) . (( pr1 H) . (k + 1))) <= (( Ser ( vol G0)) . (( pr1 H) . (k + 1))) & (( Ser ( vol G0)) . (( pr1 H) . (k + 1))) <= (( Ser ( vol G0)) . m) by Th2, SUPINF_2: 41;

        

         A47: for s be Element of NAT holds (s in N0 implies ((GG0 vol ) . s) = ((((G0 . (( pr1 H) . (k + 1))) vol ) * SOS) . s)) & ( not s in N0 implies ((GG0 vol ) . s) = 0. )

        proof

          let s be Element of NAT ;

          thus s in N0 implies ((GG0 vol ) . s) = ((((G0 . (( pr1 H) . (k + 1))) vol ) * SOS) . s)

          proof

            assume

             A48: s in N0;

            then

             A49: ex s1 be Element of NAT st s1 = s & (( pr1 H) . (k + 1)) = (( pr1 H) . s1);

            

             A50: (( pr2 H) . s) = (SOS . s) by A36, A48;

            ((GG0 vol ) . s) = ( diameter (GG0 . s)) by Def4

            .= ( diameter ((G0 . (( pr1 H) . (k + 1))) . (( pr2 H) . s))) by A2, A49, Def11

            .= (((G0 . (( pr1 H) . (k + 1))) vol ) . (SOS . s)) by A50, Def4

            .= ((((G0 . (( pr1 H) . (k + 1))) vol ) * SOS) . s) by A48, FUNCT_2: 15;

            hence thesis;

          end;

          assume not s in N0;

          then

           A51: not (( pr1 H) . (k + 1)) = (( pr1 H) . s);

          ((GG0 vol ) . s) = ( diameter (GG0 . s)) by Def4

          .= ( diameter ((G0 . (( pr1 H) . s)) . (( pr2 H) . s))) by A2, Def11

          .= 0. by A17, A51, MEASURE5: 10;

          hence thesis;

        end;

        for s1,s2 be object st s1 in N0 & s2 in N0 & (SOS . s1) = (SOS . s2) holds s1 = s2

        proof

          let s1,s2 be object;

          assume that

           A52: s1 in N0 & s2 in N0 and

           A53: (SOS . s1) = (SOS . s2);

          reconsider s1, s2 as Element of NAT by A52;

          

           A54: (ex s11 be Element of NAT st s11 = s1 & (( pr1 H) . (k + 1)) = (( pr1 H) . s11)) & ex s22 be Element of NAT st s22 = s2 & (( pr1 H) . (k + 1)) = (( pr1 H) . s22) by A52;

          

           A55: (H . s1) = [(( pr1 H) . s1), (( pr2 H) . s1)] & (H . s2) = [(( pr1 H) . s2), (( pr2 H) . s2)] by FUNCT_2: 119;

          (SOS . s1) = (( pr2 H) . s1) & (SOS . s2) = (( pr2 H) . s2) by A36, A52;

          hence thesis by A1, A53, A54, A55, FUNCT_2: 19;

        end;

        then

         A56: SOS is one-to-one by FUNCT_2: 19;

        ((G0 . (( pr1 H) . (k + 1))) vol ) is nonnegative by Th12;

        then ( SUM (GG0 vol )) <= ( SUM ((G0 . (( pr1 H) . (k + 1))) vol )) by A56, A47, Th11;

        then

         A57: (( Ser (GG0 vol )) . (k + 1)) <= ( SUM ((G0 . (( pr1 H) . (k + 1))) vol )) by A21, XXREAL_0: 2;

        ( SUM ((G0 . (( pr1 H) . (k + 1))) vol )) = ( vol (G0 . (( pr1 H) . (k + 1))))

        .= (( vol G0) . (( pr1 H) . (k + 1))) by Def7;

        then ( SUM ((G0 . (( pr1 H) . (k + 1))) vol )) <= (( Ser ( vol G0)) . m) by A46, XXREAL_0: 2;

        then

         A58: (( Ser (GG0 vol )) . (k + 1)) <= (( Ser ( vol G0)) . m) by A57, XXREAL_0: 2;

        for s be Element of NAT holds 0. <= (( vol G0) . s) by Th13;

        then ( vol G0) is nonnegative by SUPINF_2: 39;

        then (( Ser ( vol G)) . m) = ((( Ser ( vol G0)) . m) + (( Ser ( vol G1)) . m)) by A37, A33, Th3;

        hence thesis by A58, A34, A32, XXREAL_3: 36;

      end;

      

       A59: P[ 0 ]

      proof

        take m = (( pr1 H) . 0 );

        let F be sequence of ( bool REAL );

        let G be Interval_Covering of F;

        reconsider GG = ( On (G,H)) as Interval_Covering of ( union ( rng F));

        ((GG vol ) . 0 ) = ( diameter (GG . 0 )) & (((G . (( pr1 H) . 0 )) vol ) . (( pr2 H) . 0 )) = ( diameter ((G . (( pr1 H) . 0 )) . (( pr2 H) . 0 ))) by Def4;

        then ((GG vol ) . 0 ) <= (((G . (( pr1 H) . 0 )) vol ) . (( pr2 H) . 0 )) by A2, Def11;

        then ((GG vol ) . 0 ) <= ( vol (G . (( pr1 H) . 0 ))) by Th12, MEASURE6: 3;

        then

         A60: (( Ser (GG vol )) . 0 ) = ((GG vol ) . 0 ) & ((GG vol ) . 0 ) <= (( vol G) . (( pr1 H) . 0 )) by Def7, SUPINF_2:def 11;

        for n be Element of NAT holds 0. <= (( vol G) . n) by Th13;

        then ( vol G) is nonnegative by SUPINF_2: 39;

        then (( vol G) . m) <= (( Ser ( vol G)) . m) by Th2;

        hence thesis by A60, XXREAL_0: 2;

      end;

      thus for k be Nat holds P[k] from NAT_1:sch 2( A59, A3);

    end;

    theorem :: MEASURE7:15

    

     Th15: for F be sequence of ( bool REAL ) holds for G be Interval_Covering of F holds ( inf ( Svc ( union ( rng F)))) <= ( SUM ( vol G))

    proof

      let F be sequence of ( bool REAL );

      let G be Interval_Covering of F;

      consider H be sequence of [: NAT , NAT :] such that

       A1: H is one-to-one and ( dom H) = NAT and

       A2: ( rng H) = [: NAT , NAT :] by MEASURE6: 1;

      set GG = ( On (G,H));

      

       A3: for x be ExtReal st x in ( rng ( Ser (GG vol ))) holds ex y be ExtReal st y in ( rng ( Ser ( vol G))) & x <= y

      proof

        let x be ExtReal;

        assume x in ( rng ( Ser (GG vol )));

        then

        consider n be object such that

         A4: n in ( dom ( Ser (GG vol ))) and

         A5: x = (( Ser (GG vol )) . n) by FUNCT_1:def 3;

        reconsider n as Element of NAT by A4;

        consider m be Element of NAT such that

         A6: for F be sequence of ( bool REAL ) holds for G be Interval_Covering of F holds (( Ser (( On (G,H)) vol )) . n) <= (( Ser ( vol G)) . m) by A1, A2, Th14;

        take (( Ser ( vol G)) . m);

        ( dom ( Ser ( vol G))) = NAT by FUNCT_2:def 1;

        hence thesis by A5, A6, FUNCT_1:def 3;

      end;

      set Q = ( vol GG);

      Q in ( Svc ( union ( rng F))) by Def8;

      then

       A7: ( inf ( Svc ( union ( rng F)))) <= Q by XXREAL_2: 3;

      ( vol GG) <= ( SUM ( vol G)) by A3, XXREAL_2: 63;

      hence thesis by A7, XXREAL_0: 2;

    end;

    theorem :: MEASURE7:16

    

     Th16: OS_Meas is C_Measure of REAL

    proof

      set G = D;

       {} c= ( union ( rng G)) & for n be Element of NAT holds (G . n) is Interval by FUNCOP_1: 7;

      then

      reconsider G as Interval_Covering of ( {} REAL ) by Def2;

      

       A1: for A be Subset of REAL holds for F be Interval_Covering of A holds (F vol ) is nonnegative

      proof

        let A be Subset of REAL ;

        let F be Interval_Covering of A;

        for n be Element of NAT holds 0. <= ((F vol ) . n)

        proof

          let n be Element of NAT ;

          ((F vol ) . n) = ( diameter (F . n)) by Def4;

          hence thesis by MEASURE5: 13;

        end;

        hence thesis by SUPINF_2: 39;

      end;

      

       A2: for A be Subset of REAL holds 0. <= ( OS_Meas . A)

      proof

        let A be Subset of REAL ;

        

         A3: 0. is LowerBound of ( Svc A)

        proof

          let x be ExtReal;

          assume x in ( Svc A);

          then

          consider F be Interval_Covering of A such that

           A4: x = ( vol F) by Def8;

          set y = (( Ser (F vol )) . 0 );

          (F vol ) is nonnegative by A1;

          then

           A5: 0. <= y by SUPINF_2: 40;

          ( SUM (F vol )) = ( sup ( rng ( Ser (F vol )))) & y <= ( sup ( rng ( Ser (F vol )))) by FUNCT_2: 4, XXREAL_2: 4;

          hence thesis by A4, A5, XXREAL_0: 2;

        end;

        ( OS_Meas . A) = ( inf ( Svc A)) by Def10;

        hence thesis by A3, XXREAL_2:def 4;

      end;

      hence OS_Meas is nonnegative by MEASURE1:def 2;

      

       A6: for r be Element of NAT holds 0 <= r implies ((G vol ) . r) = 0.

      proof

        let n be Element of NAT ;

        ( diameter (G . n)) = ( diameter {} ) by FUNCOP_1: 7;

        hence thesis by Def4, MEASURE5: 10;

      end;

      

      then ( vol G) = (( Ser (G vol )) . 0 ) by A1, SUPINF_2: 48

      .= ((G vol ) . 0 ) by SUPINF_2:def 11

      .= 0. by A6;

      then

       A7: 0. in ( Svc ( {} REAL )) by Def8;

       0. is LowerBound of ( Svc ( {} REAL ))

      proof

        let x be ExtReal;

        assume x in ( Svc ( {} REAL ));

        then

         A8: ( inf ( Svc ( {} REAL ))) <= x by XXREAL_2: 3;

         0. <= ( OS_Meas . ( {} REAL )) by A2;

        then 0. <= ( inf ( Svc ( {} REAL ))) by Def10;

        hence thesis by A8, XXREAL_0: 2;

      end;

      then ( inf ( Svc ( {} REAL ))) = 0. by A7, XXREAL_2: 56;

      hence ( OS_Meas . {} ) = 0 by Def10;

      let A,B be Subset of REAL ;

      assume

       A9: A c= B;

      

       A10: ( Svc B) c= ( Svc A)

      proof

        let x be object;

        assume

         A11: x in ( Svc B);

        then

        reconsider x as R_eal;

        consider F be Interval_Covering of B such that

         A12: x = ( vol F) by A11, Def8;

        B c= ( union ( rng F)) by Def2;

        then (for n be Element of NAT holds (F . n) is Interval) & A c= ( union ( rng F)) by A9;

        then

        reconsider G = F as Interval_Covering of A by Def2;

        for n be Element of NAT holds ((F vol ) . n) <= ((G vol ) . n)

        proof

          let n be Element of NAT ;

          ((G vol ) . n) = ( diameter (G . n)) by Def4

          .= ((F vol ) . n) by Def4;

          hence thesis;

        end;

        then

         A13: ( SUM (F vol )) <= ( SUM (G vol )) by SUPINF_2: 43;

        for n be Element of NAT holds ((G vol ) . n) <= ((F vol ) . n)

        proof

          let n be Element of NAT ;

          ((G vol ) . n) = ( diameter (G . n)) by Def4

          .= ((F vol ) . n) by Def4;

          hence thesis;

        end;

        then ( SUM (G vol )) <= ( SUM (F vol )) by SUPINF_2: 43;

        then x = ( vol G) by A12, A13, XXREAL_0: 1;

        hence thesis by Def8;

      end;

      ( OS_Meas . A) = ( inf ( Svc A)) & ( OS_Meas . B) = ( inf ( Svc B)) by Def10;

      hence ( OS_Meas . A) <= ( OS_Meas . B) by A10, XXREAL_2: 60;

      let F be sequence of ( bool REAL );

      per cases ;

        suppose

         A14: for n be Element of NAT holds ( Svc (F . n)) <> { +infty };

        

         A16: for n be Element of NAT holds 0. <= (( OS_Meas * F) . n)

        proof

          let n be Element of NAT ;

          (( OS_Meas * F) . n) = ( OS_Meas . (F . n)) by FUNCT_2: 15;

          hence thesis by A2;

        end;

        then

         A17: ( OS_Meas * F) is nonnegative by SUPINF_2: 39;

        ( inf ( Svc ( union ( rng F)))) <= ( sup ( rng ( Ser ( OS_Meas * F))))

        proof

          set y = ( inf ( Svc ( union ( rng F)))), x = ( sup ( rng ( Ser ( OS_Meas * F))));

          assume

           A18: not ( inf ( Svc ( union ( rng F)))) <= ( sup ( rng ( Ser ( OS_Meas * F))));

           0. <= (( OS_Meas * F) . 0 ) by A16;

          then

           A19: 0. <= (( Ser ( OS_Meas * F)) . 0 ) by SUPINF_2:def 11;

          (( Ser ( OS_Meas * F)) . 0 ) <= x by FUNCT_2: 4, XXREAL_2: 4;

          then 0. <= x by A19, XXREAL_0: 2;

          then

          consider eps be Real such that

           A20: 0. < eps and

           A21: (x + eps) < y by A18, XXREAL_3: 49;

          reconsider eps as Element of ExtREAL by XXREAL_0:def 1;

          consider E be sequence of ExtREAL such that

           A22: for n be Nat holds 0. < (E . n) and

           A23: ( SUM E) < eps by A20, MEASURE6: 4;

          

           A24: (( SUM ( OS_Meas * F)) + ( SUM E)) <= (( SUM ( OS_Meas * F)) + eps) by A23, XXREAL_3: 36;

          defpred P[ Element of NAT , set] means ex F0 be Interval_Covering of (F . $1) st ($2 = F0 & (( vol F0) < (( inf ( Svc (F . $1))) + (E . $1))));

          

           A25: for n be Element of NAT holds ex F0 be Element of ( Funcs ( NAT ,( bool REAL ))) st P[n, F0]

          proof

            let n be Element of NAT ;

            

             A26: ( OS_Meas . (F . n)) = ( inf ( Svc (F . n))) & ( In ( 0 , REAL )) is Real by Def10;

            ( Svc (F . n)) <> { +infty } by A14;

            then not ( Svc (F . n)) c= { +infty } by ZFMISC_1: 33;

            then (( Svc (F . n)) \ { +infty }) <> {} by XBOOLE_1: 37;

            then

            consider x be object such that

             A27: x in (( Svc (F . n)) \ { +infty }) by XBOOLE_0:def 1;

            reconsider x as R_eal by A27;

             not x in { +infty } by A27, XBOOLE_0:def 5;

            then

             A28: x <> +infty by TARSKI:def 1;

            x in ( Svc (F . n)) by A27, XBOOLE_0:def 5;

            then ( inf ( Svc (F . n))) <= x by XXREAL_2: 3;

            then ( inf ( Svc (F . n))) < +infty by A28, XXREAL_0: 2, XXREAL_0: 4;

            then ( inf ( Svc (F . n))) is Element of REAL by A2, A26, XXREAL_0: 46;

            then

            consider S be ExtReal such that

             A29: S in ( Svc (F . n)) and

             A30: S < (( inf ( Svc (F . n))) + (E . n)) by A22, MEASURE6: 5;

            consider FS be Interval_Covering of (F . n) such that

             A31: S = ( vol FS) by A29, Def8;

            reconsider FS as Element of ( Funcs ( NAT ,( bool REAL ))) by FUNCT_2: 8;

            take FS;

            thus thesis by A30, A31;

          end;

          consider FF be sequence of ( Funcs ( NAT ,( bool REAL ))) such that

           A32: for n be Element of NAT holds P[n, (FF . n)] from FUNCT_2:sch 3( A25);

          for n be Element of NAT holds (FF . n) is Interval_Covering of (F . n)

          proof

            let n be Element of NAT ;

            ex F0 be Interval_Covering of (F . n) st F0 = (FF . n) & ( vol F0) < (( inf ( Svc (F . n))) + (E . n)) by A32;

            hence thesis;

          end;

          then

          reconsider FF as Interval_Covering of F by Def3;

          

           A33: y <= ( SUM ( vol FF)) by Th15;

          defpred P1[ Element of NAT , Element of ExtREAL ] means $2 = ((( OS_Meas * F) . $1) + (E . $1));

          

           A34: for n be Element of NAT holds ex y be Element of ExtREAL st P1[n, y];

          consider G0 be sequence of ExtREAL such that

           A35: for n be Element of NAT holds P1[n, (G0 . n)] from FUNCT_2:sch 3( A34);

          for n be Element of NAT holds (( vol FF) . n) <= (G0 . n)

          proof

            let n be Element of NAT ;

            (ex F0 be Interval_Covering of (F . n) st F0 = (FF . n) & ( vol F0) < (( inf ( Svc (F . n))) + (E . n))) & (( OS_Meas * F) . n) = ( OS_Meas . (F . n)) by A32, FUNCT_2: 15;

            then ( vol (FF . n)) < ((( OS_Meas * F) . n) + (E . n)) by Def10;

            then (( vol FF) . n) < ((( OS_Meas * F) . n) + (E . n)) by Def7;

            hence thesis by A35;

          end;

          then

           A36: ( SUM ( vol FF)) <= ( SUM G0) by SUPINF_2: 43;

          for n be Element of NAT holds 0. <= (E . n) by A22;

          then E is nonnegative by SUPINF_2: 39;

          then ( SUM G0) <= (( SUM ( OS_Meas * F)) + ( SUM E)) by A17, A35, Th4;

          then ( SUM G0) <= (( SUM ( OS_Meas * F)) + eps) by A24, XXREAL_0: 2;

          then ( SUM ( vol FF)) <= (( SUM ( OS_Meas * F)) + eps) by A36, XXREAL_0: 2;

          hence thesis by A21, A33, XXREAL_0: 2;

        end;

        hence thesis by Def10;

      end;

        suppose ex n be Element of NAT st ( Svc (F . n)) = { +infty };

        then

        consider n be Element of NAT such that

         A37: ( Svc (F . n)) = { +infty };

        for n be Element of NAT holds 0. <= (( OS_Meas * F) . n)

        proof

          let n be Element of NAT ;

          (( OS_Meas * F) . n) = ( OS_Meas . (F . n)) by FUNCT_2: 15;

          hence thesis by A2;

        end;

        then

         A38: ( OS_Meas * F) is nonnegative by SUPINF_2: 39;

        ( inf { +infty }) = +infty by XXREAL_2: 13;

        then ( OS_Meas . (F . n)) = +infty by A37, Def10;

        then (( OS_Meas * F) . n) = +infty by FUNCT_2: 15;

        then ( SUM ( OS_Meas * F)) = +infty by A38, SUPINF_2: 45;

        hence thesis by XXREAL_0: 4;

      end;

    end;

    definition

      :: original: OS_Meas

      redefine

      func OS_Meas -> C_Measure of REAL ;

      correctness by Th16;

    end

    definition

      :: MEASURE7:def12

      func Lmi_sigmaFIELD -> SigmaField of REAL equals ( sigma_Field OS_Meas );

      coherence ;

    end

    definition

      :: MEASURE7:def13

      func L_mi -> sigma_Measure of Lmi_sigmaFIELD equals ( sigma_Meas OS_Meas );

      correctness ;

    end