measure3.miz



    begin

    reserve X for set;

    theorem :: MEASURE3:1

    

     Th1: for F1,F2 be sequence of ExtREAL st (for n be Element of NAT holds (( Ser F1) . n) <= (( Ser F2) . n)) holds ( SUM F1) <= ( SUM F2)

    proof

      let F1,F2 be sequence of ExtREAL ;

      assume

       A1: for n be Element of NAT holds (( Ser F1) . n) <= (( Ser F2) . n);

      

       A2: for x be ExtReal st x in ( rng ( Ser F1)) holds ex y be ExtReal st y in ( rng ( Ser F2)) & x <= y

      proof

        let x be ExtReal;

        

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

        assume x in ( rng ( Ser F1));

        then

        consider n be object such that

         A4: n in NAT and

         A5: x = (( Ser F1) . n) by A3, FUNCT_1:def 3;

        reconsider n as Element of NAT by A4;

        reconsider y = (( Ser F2) . n) as R_eal;

        take y;

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

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

      end;

      ( SUM F1) = ( sup ( rng ( Ser F1))) & ( SUM F2) = ( sup ( rng ( Ser F2))) by SUPINF_2:def 13;

      hence thesis by A2, XXREAL_2: 63;

    end;

    theorem :: MEASURE3:2

    for F1,F2 be sequence of ExtREAL st (for n be Element of NAT holds (( Ser F1) . n) = (( Ser F2) . n)) holds ( SUM F1) = ( SUM F2)

    proof

      let F1,F2 be sequence of ExtREAL ;

      assume

       A1: for n be Element of NAT holds (( Ser F1) . n) = (( Ser F2) . n);

      then for n be Element of NAT holds (( Ser F2) . n) <= (( Ser F1) . n);

      then

       A2: ( SUM F2) <= ( SUM F1) by Th1;

      for n be Element of NAT holds (( Ser F1) . n) <= (( Ser F2) . n) by A1;

      then ( SUM F1) <= ( SUM F2) by Th1;

      hence thesis by A2, XXREAL_0: 1;

    end;

    definition

      let X be set;

      let S be SigmaField of X;

      let F be sequence of S;

      :: original: rng

      redefine

      func rng F -> N_Measure_fam of S ;

      coherence

      proof

        ( rng F) is N_Sub_set_fam of X & ( rng F) c= S by MEASURE1: 23, RELAT_1:def 19;

        hence thesis by MEASURE2:def 1;

      end;

    end

    theorem :: MEASURE3:3

    for S be SigmaField of X, M be sigma_Measure of S, F be sequence of S, A be Element of S st ( meet ( rng F)) c= A & (for n be Element of NAT holds A c= (F . n)) holds (M . A) = (M . ( meet ( rng F)))

    proof

      let S be SigmaField of X;

      let M be sigma_Measure of S;

      let F be sequence of S;

      let A be Element of S;

      assume that

       A1: ( meet ( rng F)) c= A and

       A2: for n be Element of NAT holds A c= (F . n);

      A c= ( meet ( rng F))

      proof

        let x be object;

        assume

         A3: x in A;

        for Y be set st Y in ( rng F) holds x in Y

        proof

          let Y be set;

          

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

          assume Y in ( rng F);

          then ex n be object st n in NAT & Y = (F . n) by A4, FUNCT_1:def 3;

          then A c= Y by A2;

          hence thesis by A3;

        end;

        hence thesis by SETFAM_1:def 1;

      end;

      then

       A5: (M . A) <= (M . ( meet ( rng F))) by MEASURE1: 31;

      (M . ( meet ( rng F))) <= (M . A) by A1, MEASURE1: 31;

      hence thesis by A5, XXREAL_0: 1;

    end;

    theorem :: MEASURE3:4

    

     Th4: for S be SigmaField of X, G,F be sequence of S st ((G . 0 ) = {} & for n be Nat holds (G . (n + 1)) = ((F . 0 ) \ (F . n)) & (F . (n + 1)) c= (F . n)) holds ( union ( rng G)) = ((F . 0 ) \ ( meet ( rng F)))

    proof

      let S be SigmaField of X;

      let G,F be sequence of S;

      assume that

       A1: (G . 0 ) = {} and

       A2: for n be Nat holds (G . (n + 1)) = ((F . 0 ) \ (F . n)) & (F . (n + 1)) c= (F . n);

      

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

      thus ( union ( rng G)) c= ((F . 0 ) \ ( meet ( rng F)))

      proof

        let A be object;

        assume A in ( union ( rng G));

        then

        consider Z be set such that

         A4: A in Z and

         A5: Z in ( rng G) by TARSKI:def 4;

        consider n be object such that

         A6: n in NAT and

         A7: Z = (G . n) by A3, A5, FUNCT_1:def 3;

        reconsider n as Element of NAT by A6;

        consider k be Nat such that

         A8: n = (k + 1) by A1, A4, A7, NAT_1: 6;

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

        set Y = (F . k);

        

         A9: A in ((F . 0 ) \ (F . k)) by A2, A4, A7, A8;

        then Y in ( rng F) & not A in Y by FUNCT_2: 4, XBOOLE_0:def 5;

        then

         A10: not A in ( meet ( rng F)) by SETFAM_1:def 1;

        A in (F . 0 ) by A9, XBOOLE_0:def 5;

        hence thesis by A10, XBOOLE_0:def 5;

      end;

      let A be object;

      assume

       A11: A in ((F . 0 ) \ ( meet ( rng F)));

      then not A in ( meet ( rng F)) by XBOOLE_0:def 5;

      then

       A12: ex Y be set st Y in ( rng F) & not A in Y by SETFAM_1:def 1;

      A in (F . 0 ) by A11, XBOOLE_0:def 5;

      then

      consider Y be set such that

       A13: A in (F . 0 ) and

       A14: Y in ( rng F) and

       A15: not A in Y by A12;

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

      then

      consider n be object such that

       A16: n in NAT and

       A17: Y = (F . n) by A14, FUNCT_1:def 3;

      reconsider n as Element of NAT by A16;

      A in ((F . 0 ) \ (F . n)) by A13, A15, A17, XBOOLE_0:def 5;

      then

       A18: A in (G . (n + 1)) by A2;

      (G . (n + 1)) in ( rng G) by FUNCT_2: 4;

      hence thesis by A18, TARSKI:def 4;

    end;

    theorem :: MEASURE3:5

    

     Th5: for S be SigmaField of X, G,F be sequence of S st ((G . 0 ) = {} & for n be Nat holds (G . (n + 1)) = ((F . 0 ) \ (F . n)) & (F . (n + 1)) c= (F . n)) holds ( meet ( rng F)) = ((F . 0 ) \ ( union ( rng G)))

    proof

      let S be SigmaField of X;

      let G,F be sequence of S;

      assume that

       A1: (G . 0 ) = {} and

       A2: for n be Nat holds (G . (n + 1)) = ((F . 0 ) \ (F . n)) & (F . (n + 1)) c= (F . n);

      

       A3: for n be Nat holds (F . n) c= (F . 0 )

      proof

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

        

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

        proof

          let k be Nat;

          assume

           A5: (F . k) c= (F . 0 );

          (F . (k + 1)) c= (F . k) by A2;

          hence thesis by A5, XBOOLE_1: 1;

        end;

        

         A6: P[ 0 ];

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

      end;

      

       A7: ( meet ( rng F)) c= (F . 0 )

      proof

        set X = the Element of ( rng F);

        let A be object;

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

        then ex n be object st n in NAT & (F . n) = X by FUNCT_1:def 3;

        then

         A8: X c= (F . 0 ) by A3;

        assume A in ( meet ( rng F));

        then A in X by SETFAM_1:def 1;

        hence thesis by A8;

      end;

      

       A9: ((F . 0 ) /\ ( meet ( rng F))) = ((F . 0 ) \ ((F . 0 ) \ ( meet ( rng F)))) by XBOOLE_1: 48;

      ( union ( rng G)) = ((F . 0 ) \ ( meet ( rng F))) by A1, A2, Th4;

      hence thesis by A7, A9, XBOOLE_1: 28;

    end;

    theorem :: MEASURE3:6

    

     Th6: for S be SigmaField of X, M be sigma_Measure of S, G,F be sequence of S st ((M . (F . 0 )) < +infty & (G . 0 ) = {} & for n be Nat holds (G . (n + 1)) = ((F . 0 ) \ (F . n)) & (F . (n + 1)) c= (F . n)) holds (M . ( meet ( rng F))) = ((M . (F . 0 )) - (M . ( union ( rng G))))

    proof

      let S be SigmaField of X, M be sigma_Measure of S, G,F be sequence of S;

      assume that

       A1: (M . (F . 0 )) < +infty and

       A2: (G . 0 ) = {} & for n be Nat holds (G . (n + 1)) = ((F . 0 ) \ (F . n)) & (F . (n + 1)) c= (F . n);

      

       A3: ( union ( rng G)) = ((F . 0 ) \ ( meet ( rng F))) by A2, Th4;

      

       A4: (M . ((F . 0 ) \ ( union ( rng G)))) = (M . ( meet ( rng F))) by A2, Th5;

      (M . ((F . 0 ) \ ( meet ( rng F)))) <> +infty by A1, MEASURE1: 31, XBOOLE_1: 36;

      then (M . ( union ( rng G))) < +infty by A3, XXREAL_0: 4;

      hence thesis by A3, A4, MEASURE1: 32, XBOOLE_1: 36;

    end;

    theorem :: MEASURE3:7

    

     Th7: for S be SigmaField of X, M be sigma_Measure of S, G,F be sequence of S st ((M . (F . 0 )) < +infty & (G . 0 ) = {} & for n be Nat holds (G . (n + 1)) = ((F . 0 ) \ (F . n)) & (F . (n + 1)) c= (F . n)) holds (M . ( union ( rng G))) = ((M . (F . 0 )) - (M . ( meet ( rng F))))

    proof

      let S be SigmaField of X, M be sigma_Measure of S, G,F be sequence of S;

      assume that

       A1: (M . (F . 0 )) < +infty and

       A2: (G . 0 ) = {} & for n be Nat holds (G . (n + 1)) = ((F . 0 ) \ (F . n)) & (F . (n + 1)) c= (F . n);

      

       A3: ( meet ( rng F)) = ((F . 0 ) \ ( union ( rng G))) by A2, Th5;

      

       A4: (M . ((F . 0 ) \ ( meet ( rng F)))) = (M . ( union ( rng G))) by A2, Th4;

      (M . ((F . 0 ) \ ( union ( rng G)))) <> +infty by A1, MEASURE1: 31, XBOOLE_1: 36;

      then (M . ( meet ( rng F))) < +infty by A3, XXREAL_0: 4;

      hence thesis by A3, A4, MEASURE1: 32, XBOOLE_1: 36;

    end;

    theorem :: MEASURE3:8

    for S be SigmaField of X, M be sigma_Measure of S, G,F be sequence of S st ((M . (F . 0 )) < +infty & (G . 0 ) = {} & for n be Nat holds (G . (n + 1)) = ((F . 0 ) \ (F . n)) & (F . (n + 1)) c= (F . n)) holds (M . ( meet ( rng F))) = ((M . (F . 0 )) - ( sup ( rng (M * G))))

    proof

      let S be SigmaField of X, M be sigma_Measure of S, G,F be sequence of S;

      assume that

       A1: (M . (F . 0 )) < +infty and

       A2: (G . 0 ) = {} & for n be Nat holds (G . (n + 1)) = ((F . 0 ) \ (F . n)) & (F . (n + 1)) c= (F . n);

      for n be Nat holds (G . n) c= (G . (n + 1)) by A2, MEASURE2: 13;

      then (M . ( union ( rng G))) = ( sup ( rng (M * G))) by MEASURE2: 23;

      hence thesis by A1, A2, Th6;

    end;

    theorem :: MEASURE3:9

    

     Th9: for S be SigmaField of X, M be sigma_Measure of S, G,F be sequence of S st ((M . (F . 0 )) < +infty & (G . 0 ) = {} & for n be Nat holds (G . (n + 1)) = ((F . 0 ) \ (F . n)) & (F . (n + 1)) c= (F . n)) holds (M . (F . 0 )) in REAL & ( inf ( rng (M * F))) in REAL & ( sup ( rng (M * G))) in REAL

    proof

      let S be SigmaField of X, M be sigma_Measure of S, G,F be sequence of S;

      assume that

       A1: (M . (F . 0 )) < +infty and

       A2: (G . 0 ) = {} and

       A3: for n be Nat holds (G . (n + 1)) = ((F . 0 ) \ (F . n)) & (F . (n + 1)) c= (F . n);

      reconsider P = {} as Element of S by PROB_1: 4;

      

       A4: 0 in REAL by XREAL_0:def 1;

      (M . P) <= (M . (F . 0 )) by MEASURE1: 31, XBOOLE_1: 2;

      then 0. <= (M . (F . 0 )) by VALUED_0:def 19;

      hence

       A5: (M . (F . 0 )) in REAL by A1, XXREAL_0: 46, A4;

      for x be ExtReal st x in ( rng (M * G)) holds x <= (M . (F . 0 ))

      proof

        let x be ExtReal;

        

         A6: ( dom (M * G)) = NAT by FUNCT_2:def 1;

        assume x in ( rng (M * G));

        then

        consider n be object such that

         A7: n in NAT and

         A8: ((M * G) . n) = x by A6, FUNCT_1:def 3;

        reconsider n as Element of NAT by A7;

        

         A9: x = (M . (G . n)) by A6, A8, FUNCT_1: 12;

        

         A10: (ex k be Nat st n = (k + 1)) implies x <= (M . (F . 0 ))

        proof

          given k be Nat such that

           A11: n = (k + 1);

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

          (G . n) = ((F . 0 ) \ (F . k)) by A3, A11;

          hence thesis by A9, MEASURE1: 31, XBOOLE_1: 36;

        end;

        n = 0 implies x <= (M . (F . 0 )) by A2, A9, MEASURE1: 31, XBOOLE_1: 2;

        hence thesis by A10, NAT_1: 6;

      end;

      then (M . (F . 0 )) is UpperBound of ( rng (M * G)) by XXREAL_2:def 1;

      then

       A12: ( sup ( rng (M * G))) <= (M . (F . 0 )) by XXREAL_2:def 3;

      for x be ExtReal st x in ( rng (M * F)) holds 0. <= x

      proof

        let x be ExtReal;

        

         A13: ( dom (M * F)) = NAT by FUNCT_2:def 1;

        

         A14: (M * F) is nonnegative by MEASURE2: 1;

        assume x in ( rng (M * F));

        then ex n be object st n in NAT & ((M * F) . n) = x by A13, FUNCT_1:def 3;

        hence thesis by A14, SUPINF_2: 39;

      end;

      then 0. is LowerBound of ( rng (M * F)) by XXREAL_2:def 2;

      then

       A15: ( inf ( rng (M * F))) >= ( In ( 0 , REAL )) by XXREAL_2:def 4;

      ex x be R_eal st x in ( rng (M * F)) & x = (M . (F . 0 ))

      proof

        take ((M * F) . 0 );

        ( dom (M * F)) = NAT by FUNCT_2:def 1;

        hence thesis by FUNCT_1: 12, FUNCT_2: 4;

      end;

      then ( inf ( rng (M * F))) <= (M . (F . 0 )) by XXREAL_2: 3;

      hence ( inf ( rng (M * F))) in REAL by A5, A15, XXREAL_0: 45;

      ( In ( 0 , REAL )) <= ( sup ( rng (M * G)))

      proof

        set x = ((M * G) . 0 );

        for x be R_eal st x in ( rng (M * G)) holds 0. <= x

        proof

          let x be R_eal;

          

           A16: ( dom (M * G)) = NAT by FUNCT_2:def 1;

          

           A17: (M * G) is nonnegative by MEASURE2: 1;

          assume x in ( rng (M * G));

          then ex n be object st n in NAT & ((M * G) . n) = x by A16, FUNCT_1:def 3;

          hence thesis by A17, SUPINF_2: 39;

        end;

        then

         A18: 0. <= x by FUNCT_2: 4;

        x <= ( sup ( rng (M * G))) by FUNCT_2: 4, XXREAL_2: 4;

        hence thesis by A18, XXREAL_0: 2;

      end;

      hence thesis by A5, A12, XXREAL_0: 45;

    end;

    theorem :: MEASURE3:10

    

     Th10: for S be SigmaField of X, M be sigma_Measure of S, G,F be sequence of S st ((M . (F . 0 )) < +infty & (G . 0 ) = {} & for n be Nat holds (G . (n + 1)) = ((F . 0 ) \ (F . n)) & (F . (n + 1)) c= (F . n)) holds ( sup ( rng (M * G))) = ((M . (F . 0 )) - ( inf ( rng (M * F))))

    proof

      let S be SigmaField of X, M be sigma_Measure of S, G,F be sequence of S;

      assume that

       A1: (M . (F . 0 )) < +infty and

       A2: (G . 0 ) = {} and

       A3: for n be Nat holds (G . (n + 1)) = ((F . 0 ) \ (F . n)) & (F . (n + 1)) c= (F . n);

      set l = ((M . (F . 0 )) - ( inf ( rng (M * F))));

      for x be ExtReal st x in ( rng (M * G)) holds x <= l

      proof

        let x be ExtReal;

        

         A4: ( dom (M * G)) = NAT by FUNCT_2:def 1;

        assume x in ( rng (M * G));

        then

        consider n be object such that

         A5: n in NAT and

         A6: ((M * G) . n) = x by A4, FUNCT_1:def 3;

        (M * G) is nonnegative by MEASURE2: 1;

        then x >= ( In ( 0 , REAL )) by A5, A6, SUPINF_2: 39;

        then

         A7: x > -infty by XXREAL_0: 2, XXREAL_0: 12;

        reconsider n as Element of NAT by A5;

        

         A8: n = 0 implies (G . n) c= (F . 0 ) by A2;

        

         A9: ( dom (M * F)) = NAT by FUNCT_2:def 1;

        

         A10: n = 0 implies (M . ((F . 0 ) \ (G . n))) in ( rng (M * F))

        proof

          assume

           A11: n = 0 ;

          (M . (F . 0 )) = ((M * F) . 0 ) by A9, FUNCT_1: 12;

          hence thesis by A2, A11, FUNCT_2: 4;

        end;

        

         A12: (ex k be Nat st n = (k + 1)) implies (M . ((F . 0 ) \ (G . n))) in ( rng (M * F))

        proof

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

          

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

          proof

            let k be Nat;

            assume

             A14: (F . k) c= (F . 0 );

            (F . (k + 1)) c= (F . k) by A3;

            hence thesis by A14, XBOOLE_1: 1;

          end;

          

           A15: P[ 0 ];

          

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

          given k be Nat such that

           A17: n = (k + 1);

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

          

           A18: (M . (F . k)) = ((M * F) . k) by A9, FUNCT_1: 12;

          ((F . 0 ) \ (G . n)) = ((F . 0 ) \ ((F . 0 ) \ (F . k))) by A3, A17

          .= ((F . 0 ) /\ (F . k)) by XBOOLE_1: 48

          .= (F . k) by A16, XBOOLE_1: 28;

          hence thesis by A18, FUNCT_2: 4;

        end;

        

         A19: (ex k be Nat st n = (k + 1)) implies (G . n) c= (F . 0 )

        proof

          given k be Nat such that

           A20: n = (k + 1);

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

          (G . n) = ((F . 0 ) \ (F . k)) by A3, A20;

          hence thesis by XBOOLE_1: 36;

        end;

        

         A21: x = (M . (G . n)) by A4, A6, FUNCT_1: 12;

        then x <> +infty by A1, A8, A19, MEASURE1: 31, NAT_1: 6;

        then

         A22: x in REAL by A7, XXREAL_0: 14;

        reconsider x as R_eal by XXREAL_0:def 1;

        (M . (F . 0 )) in REAL & ( inf ( rng (M * F))) in REAL by A1, A2, A3, Th9;

        then

        consider a,b,c be Real such that

         A23: a = (M . (F . 0 )) and

         A24: b = x and

         A25: c = ( inf ( rng (M * F))) by A22;

        ((M . (F . 0 )) - x) = (a - b) by A23, A24, SUPINF_2: 3;

        

        then

         A26: (((M . (F . 0 )) - x) + x) = ((a - b) + b) by A24, SUPINF_2: 1

        .= (M . (F . 0 )) by A23;

        (( inf ( rng (M * F))) + x) = (c + b) by A24, A25, SUPINF_2: 1;

        

        then

         A27: ((( inf ( rng (M * F))) + x) - ( inf ( rng (M * F)))) = ((b + c) - c) by A25, SUPINF_2: 3

        .= x by A24;

        ((M . (F . 0 )) - x) = (M . ((F . 0 ) \ (G . n))) by A21, A8, A19, A22, MEASURE1: 32, NAT_1: 6, XXREAL_0: 9;

        then ( inf ( rng (M * F))) <= ((M . (F . 0 )) - x) by A10, A12, NAT_1: 6, XXREAL_2: 3;

        then (( inf ( rng (M * F))) + x) <= (M . (F . 0 )) by A26, XXREAL_3: 36;

        hence thesis by A27, XXREAL_3: 37;

      end;

      then

       A28: l is UpperBound of ( rng (M * G)) by XXREAL_2:def 1;

      

       A29: for n be Nat holds (G . n) c= (G . (n + 1)) by A2, A3, MEASURE2: 13;

      for y be UpperBound of ( rng (M * G)) holds l <= y

      proof

        let y be UpperBound of ( rng (M * G));

        l <= y

        proof

          for x be ExtReal st x in ( rng (M * F)) holds (M . ( meet ( rng F))) <= x

          proof

            let x be ExtReal;

            

             A30: ( dom (M * F)) = NAT by FUNCT_2:def 1;

            assume x in ( rng (M * F));

            then

            consider n be object such that

             A31: n in NAT and

             A32: ((M * F) . n) = x by A30, FUNCT_1:def 3;

            reconsider n as Element of NAT by A31;

            

             A33: ( meet ( rng F)) c= (F . n) by FUNCT_2: 4, SETFAM_1: 3;

            x = (M . (F . n)) by A30, A32, FUNCT_1: 12;

            hence thesis by A33, MEASURE1: 31;

          end;

          then (M . ( meet ( rng F))) is LowerBound of ( rng (M * F)) by XXREAL_2:def 2;

          then

           A34: (M . ( meet ( rng F))) <= ( inf ( rng (M * F))) by XXREAL_2:def 4;

          set Q = ( union ( rng G));

          ( sup ( rng (M * G))) = (M . Q) by A29, MEASURE2: 23;

          then

           A35: (M . Q) <= y by XXREAL_2:def 3;

          ((M . (F . 0 )) - (M . ( meet ( rng F)))) = (M . ( union ( rng G))) by A1, A2, A3, Th7;

          then l <= (M . Q) by A34, XXREAL_3: 37;

          hence thesis by A35, XXREAL_0: 2;

        end;

        hence thesis;

      end;

      hence thesis by A28, XXREAL_2:def 3;

    end;

    theorem :: MEASURE3:11

    

     Th11: for S be SigmaField of X, M be sigma_Measure of S, G,F be sequence of S st ((M . (F . 0 )) < +infty & (G . 0 ) = {} & for n be Nat holds (G . (n + 1)) = ((F . 0 ) \ (F . n)) & (F . (n + 1)) c= (F . n)) holds ( inf ( rng (M * F))) = ((M . (F . 0 )) - ( sup ( rng (M * G))))

    proof

      let S be SigmaField of X, M be sigma_Measure of S, G,F be sequence of S;

      assume that

       A1: (M . (F . 0 )) < +infty and

       A2: (G . 0 ) = {} and

       A3: for n be Nat holds (G . (n + 1)) = ((F . 0 ) \ (F . n)) & (F . (n + 1)) c= (F . n);

      set l = ((M . (F . 0 )) - ( sup ( rng (M * G))));

      for x be ExtReal st x in ( rng (M * F)) holds l <= x

      proof

        let x be ExtReal;

        assume

         A4: x in ( rng (M * F));

        x <> +infty implies l <= x

        proof

          

           A5: ( dom (M * F)) = NAT by FUNCT_2:def 1;

          then

          consider n be object such that

           A6: n in NAT and

           A7: ((M * F) . n) = x by A4, FUNCT_1:def 3;

          (M * F) is nonnegative by MEASURE2: 1;

          then

           A8: 0. <= x by A6, A7, SUPINF_2: 39;

          assume

           A9: x <> +infty ;

          reconsider x as R_eal by XXREAL_0:def 1;

          x <= +infty by XXREAL_0: 3;

          then x < +infty by A9, XXREAL_0: 1;

          then

           A10: x in REAL by A8, XXREAL_0: 14, XXREAL_0: 46;

          (M . (F . 0 )) in REAL & ( sup ( rng (M * G))) in REAL by A1, A2, A3, Th9;

          then

          consider a,b,c be Real such that

           A11: a = (M . (F . 0 )) and

           A12: b = x and

           A13: c = ( sup ( rng (M * G))) by A10;

          (( sup ( rng (M * G))) + x) = (c + b) by A12, A13, SUPINF_2: 1;

          

          then

           A14: ((( sup ( rng (M * G))) + x) - ( sup ( rng (M * G)))) = ((b + c) - c) by A13, SUPINF_2: 3

          .= x by A12;

          reconsider n as Element of NAT by A6;

          

           A15: ( dom (M * G)) = NAT by FUNCT_2:def 1;

          

           A16: ((M . (F . 0 )) - x) <= ( sup ( rng (M * G)))

          proof

            set k = (n + 1);

            

             A17: for n be Nat holds (F . n) c= (F . 0 )

            proof

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

              

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

              proof

                let k be Nat;

                assume

                 A19: (F . k) c= (F . 0 );

                (F . (k + 1)) c= (F . k) by A3;

                hence thesis by A19, XBOOLE_1: 1;

              end;

              

               A20: P[ 0 ];

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

            end;

            then (M . (F . n)) <= (M . (F . 0 )) by MEASURE1: 31;

            then

             A21: (M . (F . n)) < +infty by A1, XXREAL_0: 2;

            ((M . (F . 0 )) - x) = ((M . (F . 0 )) - (M . (F . n))) by A5, A7, FUNCT_1: 12

            .= (M . ((F . 0 ) \ (F . n))) by A17, A21, MEASURE1: 32

            .= (M . (G . (n + 1))) by A3;

            then ((M . (F . 0 )) - x) = ((M * G) . k) by A15, FUNCT_1: 12;

            hence thesis by FUNCT_2: 4, XXREAL_2: 4;

          end;

          ((M . (F . 0 )) - x) = (a - b) by A11, A12, SUPINF_2: 3;

          

          then (((M . (F . 0 )) - x) + x) = ((a - b) + b) by A12, SUPINF_2: 1

          .= (M . (F . 0 )) by A11;

          then (M . (F . 0 )) <= (( sup ( rng (M * G))) + x) by A16, XXREAL_3: 36;

          hence thesis by A14, XXREAL_3: 37;

        end;

        hence thesis by XXREAL_0: 4;

      end;

      then

       A22: l is LowerBound of ( rng (M * F)) by XXREAL_2:def 2;

      for y be LowerBound of ( rng (M * F)) holds y <= l

      proof

        

         A23: ( inf ( rng (M * F))) in REAL by A1, A2, A3, Th9;

        ( sup ( rng (M * G))) in REAL & (M . (F . 0 )) in REAL by A1, A2, A3, Th9;

        then

        consider a,b,c be Real such that

         A24: a = ( sup ( rng (M * G))) and

         A25: b = (M . (F . 0 )) and

         A26: c = ( inf ( rng (M * F))) by A23;

        (( sup ( rng (M * G))) + ( inf ( rng (M * F)))) = (a + c) by A24, A26, SUPINF_2: 1;

        

        then

         A27: ((( sup ( rng (M * G))) + ( inf ( rng (M * F)))) - ( sup ( rng (M * G)))) = ((c + a) - a) by A24, SUPINF_2: 3

        .= ( inf ( rng (M * F))) by A26;

        let y be LowerBound of ( rng (M * F));

        consider s,t,r be R_eal such that s = ( sup ( rng (M * G))) and t = ((M . (F . 0 )) - ( inf ( rng (M * F)))) and

         A28: r = ( inf ( rng (M * F)));

        

         A29: ( sup ( rng (M * G))) = ((M . (F . 0 )) - ( inf ( rng (M * F)))) by A1, A2, A3, Th10;

        ((M . (F . 0 )) - ( inf ( rng (M * F)))) = (b - c) by A25, A26, SUPINF_2: 3;

        

        then (((M . (F . 0 )) - ( inf ( rng (M * F)))) + r) = ((b - c) + c) by A26, A28, SUPINF_2: 1

        .= (M . (F . 0 )) by A25;

        hence thesis by A29, A28, A27, XXREAL_2:def 4;

      end;

      hence thesis by A22, XXREAL_2:def 4;

    end;

    theorem :: MEASURE3:12

    for S be SigmaField of X, M be sigma_Measure of S, F be sequence of S st (for n be Nat holds (F . (n + 1)) c= (F . n)) & (M . (F . 0 )) < +infty holds (M . ( meet ( rng F))) = ( inf ( rng (M * F)))

    proof

      let S be SigmaField of X, M be sigma_Measure of S, F be sequence of S;

      assume that

       A1: for n be Nat holds (F . (n + 1)) c= (F . n) and

       A2: (M . (F . 0 )) < +infty ;

      consider G be sequence of S such that

       A3: (G . 0 ) = {} & for n be Nat holds (G . (n + 1)) = ((F . 0 ) \ (F . n)) by MEASURE2: 9;

      

       A4: ( union ( rng G)) = ((F . 0 ) \ ( meet ( rng F))) by A1, A3, Th4;

      

       A5: (M . ((F . 0 ) \ ( union ( rng G)))) = (M . ( meet ( rng F))) by A1, A3, Th5;

      

       A6: for A be Element of S st A = ( union ( rng G)) holds (M . ( meet ( rng F))) = ((M . (F . 0 )) - (M . A))

      proof

        let A be Element of S;

        assume

         A7: A = ( union ( rng G));

        (M . ((F . 0 ) \ ( meet ( rng F)))) <> +infty by A2, MEASURE1: 31, XBOOLE_1: 36;

        then (M . A) < +infty by A4, A7, XXREAL_0: 4;

        hence thesis by A4, A5, A7, MEASURE1: 32, XBOOLE_1: 36;

      end;

      for n be Nat holds (G . n) c= (G . (n + 1)) by A1, A3, MEASURE2: 13;

      then (M . ( union ( rng G))) = ( sup ( rng (M * G))) by MEASURE2: 23;

      then (M . ( meet ( rng F))) = ((M . (F . 0 )) - ( sup ( rng (M * G)))) by A6;

      hence thesis by A1, A2, A3, Th11;

    end;

    theorem :: MEASURE3:13

    

     Th13: for S be SigmaField of X, M be Measure of S, F be Sep_Sequence of S holds ( SUM (M * F)) <= (M . ( union ( rng F)))

    proof

      let S be SigmaField of X, M be Measure of S, F be Sep_Sequence of S;

      set T = ( rng F);

      consider G be sequence of S such that

       A1: (G . 0 ) = (F . 0 ) and

       A2: for n be Nat holds (G . (n + 1)) = ((F . (n + 1)) \/ (G . n)) by MEASURE2: 4;

       {} is Subset of X by XBOOLE_1: 2;

      then

      consider H be sequence of ( bool X) such that

       A3: ( rng H) = {( union T), {} } and

       A4: (H . 0 ) = ( union T) and

       A5: for n be Nat st 0 < n holds (H . n) = {} by MEASURE1: 19;

      ( rng H) c= S

      proof

        let a be object;

        assume a in ( rng H);

        then a = ( union T) or a = {} by A3, TARSKI:def 2;

        hence thesis by PROB_1: 4;

      end;

      then

      reconsider H as sequence of S by FUNCT_2: 6;

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

      

       A6: ( dom (M * F)) = NAT by FUNCT_2:def 1;

      

       A7: for n be Nat holds ((G . n) /\ (F . (n + 1))) = {}

      proof

        let n be Nat;

        

         A8: for n be Nat holds for k be Element of NAT st n < k holds ((G . n) /\ (F . k)) = {}

        proof

          defpred P[ Nat] means for k be Element of NAT st $1 < k holds ((G . $1) /\ (F . k)) = {} ;

          

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

          proof

            let n be Nat;

            assume

             A10: for k be Element of NAT st n < k holds ((G . n) /\ (F . k)) = {} ;

            let k be Element of NAT ;

            assume

             A11: (n + 1) < k;

            then

             A12: n < k by NAT_1: 13;

            (F . (n + 1)) misses (F . k) by A11, PROB_2:def 2;

            then

             A13: ((F . (n + 1)) /\ (F . k)) = {} ;

            ((G . (n + 1)) /\ (F . k)) = (((F . (n + 1)) \/ (G . n)) /\ (F . k)) by A2

            .= (((F . (n + 1)) /\ (F . k)) \/ ((G . n) /\ (F . k))) by XBOOLE_1: 23;

            hence thesis by A10, A12, A13;

          end;

          

           A14: P[ 0 ] by PROB_2:def 2, A1, XBOOLE_0:def 7;

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

        end;

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

        hence thesis by A8;

      end;

      

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

      proof

        let k be Nat;

        ((G . k) /\ (F . (k + 1))) = {} by A7;

        then

         A16: (G . k) misses (F . (k + 1));

        assume (( Ser (M * F)) . k) = (M . (G . k));

        then (( Ser (M * F)) . (k + 1)) = ((M . (G . k)) + ((M * F) . (k + 1))) by SUPINF_2:def 11;

        

        then (( Ser (M * F)) . (k + 1)) = ((M . (G . k)) + (M . (F . (k + 1)))) by A6, FUNCT_1: 12

        .= (M . ((F . (k + 1)) \/ (G . k))) by A16, MEASURE1:def 3

        .= (M . (G . (k + 1))) by A2;

        hence thesis;

      end;

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

      then

       A17: P[ 0 ] by A1, A6, FUNCT_1: 12;

      

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

      defpred P[ Nat] means (( Ser (M * H)) . $1) = (M . ( union T));

      

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

      proof

        let n be Nat;

         0 <= n by NAT_1: 2;

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

        then

         A20: (H . (n + 1)) = {} by A5;

        ( dom (M * H)) = NAT by FUNCT_2:def 1;

        then ((M * H) . (n + 1)) = (M . {} ) by A20, FUNCT_1: 12;

        then

         A21: ((M * H) . (n + 1)) = 0. by VALUED_0:def 19;

        assume (( Ser (M * H)) . n) = (M . ( union T));

        then (( Ser (M * H)) . (n + 1)) = ((M . ( union T)) + ((M * H) . (n + 1))) by SUPINF_2:def 11;

        hence thesis by A21, XXREAL_3: 4;

      end;

      (( Ser (M * H)) . 0 ) = ((M * H) . 0 ) & ( dom (M * H)) = NAT by FUNCT_2:def 1, SUPINF_2:def 11;

      then

       A22: P[ 0 ] by A4, FUNCT_1: 12;

      

       A23: for n be Nat holds P[n] from NAT_1:sch 2( A22, A19);

      

       A24: for r be Element of NAT st 1 <= r holds ((M * H) . r) = 0.

      proof

        let r be Element of NAT ;

        assume 1 <= r;

        then ( 0 + 1) <= r;

        then 0 < r by NAT_1: 13;

        then

         A25: (H . r) = {} by A5;

        ( dom (M * H)) = NAT by FUNCT_2:def 1;

        then ((M * H) . r) = (M . {} ) by A25, FUNCT_1: 12;

        hence thesis by VALUED_0:def 19;

      end;

      

       A26: for n be Nat holds (G . n) c= ( union T)

      proof

        defpred P[ Nat] means (G . $1) c= ( union T);

        

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

        proof

          let n be Nat;

          assume

           A28: (G . n) c= ( union T);

          (G . (n + 1)) = ((F . (n + 1)) \/ (G . n)) & (F . (n + 1)) c= ( union T) by A2, FUNCT_2: 4, ZFMISC_1: 74;

          hence thesis by A28, XBOOLE_1: 8;

        end;

        

         A29: P[ 0 ] by A1, FUNCT_2: 4, ZFMISC_1: 74;

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

      end;

      

       A30: for n be Element of NAT holds (( Ser (M * F)) . n) <= (( Ser (M * H)) . n)

      proof

        let n be Element of NAT ;

        (( Ser (M * F)) . n) = (M . (G . n)) by A18;

        then (( Ser (M * F)) . n) <= (M . ( union T)) by A26, MEASURE1: 8;

        hence thesis by A23;

      end;

      (M * H) is nonnegative by MEASURE1: 25;

      then ( SUM (M * H)) = (( Ser (M * H)) . 1) by A24, SUPINF_2: 48;

      then ( SUM (M * H)) = (M . ( union T)) by A23;

      hence thesis by A30, Th1;

    end;

    theorem :: MEASURE3:14

    for S be SigmaField of X, M be Measure of S st (for F be Sep_Sequence of S holds (M . ( union ( rng F))) <= ( SUM (M * F))) holds M is sigma_Measure of S

    proof

      let S be SigmaField of X, M be Measure of S;

      assume

       A1: for F be Sep_Sequence of S holds (M . ( union ( rng F))) <= ( SUM (M * F));

      for F be Sep_Sequence of S holds ( SUM (M * F)) = (M . ( union ( rng F)))

      proof

        let F be Sep_Sequence of S;

        (M . ( union ( rng F))) <= ( SUM (M * F)) & ( SUM (M * F)) <= (M . ( union ( rng F))) by A1, Th13;

        hence thesis by XXREAL_0: 1;

      end;

      hence thesis by MEASURE1:def 6;

    end;

    definition

      let X be set;

      let Sigma be SigmaField of X;

      let M be sigma_Measure of Sigma;

      :: MEASURE3:def1

      attr M is complete means for A be Subset of X, B be set st B in Sigma & A c= B & (M . B) = 0. holds A in Sigma;

    end

    definition

      let X be set;

      let S be SigmaField of X;

      let M be sigma_Measure of S;

      :: MEASURE3:def2

      mode thin of M -> Subset of X means

      : Def2: ex B be set st B in S & it c= B & (M . B) = 0. ;

      existence

      proof

        reconsider A = {} as Subset of X by XBOOLE_1: 2;

        take A;

        take B = {} ;

        thus B in S by PROB_1: 4;

        thus A c= B;

        thus thesis by VALUED_0:def 19;

      end;

    end

    definition

      let X be set;

      let S be SigmaField of X;

      let M be sigma_Measure of S;

      :: MEASURE3:def3

      func COM (S,M) -> non empty Subset-Family of X means

      : Def3: for A be set holds (A in it iff ex B be set st B in S & ex C be thin of M st A = (B \/ C));

      existence

      proof

        

         A1: ex B be set st B in S & {} c= B & (M . B) = 0.

        proof

          consider B be set such that

           A2: B = {} & B in S by PROB_1: 4;

          take B;

          thus thesis by A2, VALUED_0:def 19;

        end;

        

         A3: {} is Subset of X by XBOOLE_1: 2;

        

         A4: for A be set st A = {} holds ex B be set st B in S & ex C be thin of M st A = (B \/ C)

        proof

          reconsider C = {} as thin of M by A3, A1, Def2;

          let A be set;

          consider B be set such that

           A5: B = {} and

           A6: B in S by PROB_1: 4;

          assume A = {} ;

          then A = (B \/ C) by A5;

          hence thesis by A6;

        end;

        defpred P[ set] means for A be set st A = $1 holds ex B be set st B in S & ex C be thin of M st A = (B \/ C);

        consider D be set such that

         A7: for y be set holds y in D iff y in ( bool X) & P[y] from XFAMILY:sch 1;

        

         A8: for A be set holds (A in D iff ex B be set st (B in S & ex C be thin of M st A = (B \/ C)))

        proof

          let A be set;

          

           A9: A in D iff (A in ( bool X) & for y be set st y = A holds ex B be set st (B in S & ex C be thin of M st y = (B \/ C))) by A7;

          (ex B be set st (B in S & ex C be thin of M st A = (B \/ C))) implies A in D

          proof

            assume

             A10: ex B be set st (B in S & ex C be thin of M st A = (B \/ C));

            then A c= X by XBOOLE_1: 8;

            hence thesis by A9, A10;

          end;

          hence thesis by A7;

        end;

        

         A11: D c= ( bool X) by A7;

         {} c= X;

        then

        reconsider D as non empty Subset-Family of X by A7, A11, A4;

        take D;

        thus thesis by A8;

      end;

      uniqueness

      proof

        let D1,D2 be non empty Subset-Family of X such that

         A12: for A be set holds (A in D1 iff ex B be set st (B in S & ex C be thin of M st A = (B \/ C))) and

         A13: for A be set holds (A in D2 iff ex B be set st (B in S & ex C be thin of M st A = (B \/ C)));

        for A be object holds A in D1 iff A in D2

        proof

          let A be object;

          thus A in D1 implies A in D2

          proof

            assume A in D1;

            then ex B be set st (B in S & ex C be thin of M st A = (B \/ C)) by A12;

            hence thesis by A13;

          end;

          assume A in D2;

          then ex B be set st (B in S & ex C be thin of M st A = (B \/ C)) by A13;

          hence thesis by A12;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    definition

      let X be set;

      let S be SigmaField of X;

      let M be sigma_Measure of S;

      let A be Element of ( COM (S,M));

      :: MEASURE3:def4

      func MeasPart (A) -> non empty Subset-Family of X means

      : Def4: for B be set holds (B in it iff B in S & B c= A & (A \ B) is thin of M);

      existence

      proof

        defpred P[ set] means for t be set st t = $1 holds t in S & t c= A & (A \ t) is thin of M;

        consider D be set such that

         A1: for t be set holds t in D iff t in ( bool X) & P[t] from XFAMILY:sch 1;

        

         A2: for B be set holds B in D iff B in S & B c= A & (A \ B) is thin of M

        proof

          let B be set;

          B in S & B c= A & (A \ B) is thin of M implies B in D

          proof

            assume that

             A3: B in S and

             A4: B c= A & (A \ B) is thin of M;

            for t be set st t = B holds t in S & t c= A & (A \ t) is thin of M by A3, A4;

            hence thesis by A1, A3;

          end;

          hence thesis by A1;

        end;

        

         A5: D c= ( bool X)

        proof

          let B be object;

          assume B in D;

          then B in S by A2;

          hence thesis;

        end;

        D <> {}

        proof

          consider B be set such that

           A6: B in S and

           A7: ex C be thin of M st A = (B \/ C) by Def3;

          consider C be thin of M such that

           A8: A = (B \/ C) by A7;

          consider E be set such that

           A9: E in S and

           A10: C c= E and

           A11: (M . E) = 0. by Def2;

          (A \ B) = (C \ B) by A8, XBOOLE_1: 40;

          then (A \ B) c= C by XBOOLE_1: 36;

          then (A \ B) c= E by A10;

          then

           A12: (A \ B) is thin of M by A9, A11, Def2;

          B c= A by A8, XBOOLE_1: 7;

          hence thesis by A2, A6, A12;

        end;

        then

        reconsider D as non empty Subset-Family of X by A5;

        take D;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let D1,D2 be non empty Subset-Family of X such that

         A13: for B be set holds B in D1 iff B in S & B c= A & (A \ B) is thin of M and

         A14: for B be set holds B in D2 iff B in S & B c= A & (A \ B) is thin of M;

        for B be object holds B in D1 iff B in D2

        proof

          let B be object;

          reconsider BB = B as set by TARSKI: 1;

          thus B in D1 implies B in D2

          proof

            assume

             A15: B in D1;

            then

             A16: (A \ BB) is thin of M by A13;

            B in S & BB c= A by A13, A15;

            hence thesis by A14, A16;

          end;

          assume

           A17: B in D2;

          then

           A18: (A \ BB) is thin of M by A14;

          B in S & BB c= A by A14, A17;

          hence thesis by A13, A18;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    theorem :: MEASURE3:15

    

     Th15: for S be SigmaField of X, M be sigma_Measure of S, F be sequence of ( COM (S,M)) holds ex G be sequence of S st for n be Element of NAT holds (G . n) in ( MeasPart (F . n))

    proof

      let S be SigmaField of X, M be sigma_Measure of S, F be sequence of ( COM (S,M));

      defpred P[ Element of NAT , set] means for n be Element of NAT , y be set st n = $1 & y = $2 holds y in ( MeasPart (F . n));

      

       A1: for t be Element of NAT holds ex A be Element of S st P[t, A]

      proof

        let t be Element of NAT ;

        set A = the Element of ( MeasPart (F . t));

        reconsider A as Element of S by Def4;

        take A;

        thus thesis;

      end;

      ex G be sequence of S st for t be Element of NAT holds P[t, (G . t)] from FUNCT_2:sch 3( A1);

      then

      consider G be sequence of S such that

       A2: for t be Element of NAT , n be Element of NAT , y be set st n = t & y = (G . t) holds y in ( MeasPart (F . n));

      take G;

      thus thesis by A2;

    end;

    theorem :: MEASURE3:16

    

     Th16: for S be SigmaField of X, M be sigma_Measure of S, F be sequence of ( COM (S,M)), G be sequence of S holds ex H be sequence of ( bool X) st for n be Element of NAT holds (H . n) = ((F . n) \ (G . n))

    proof

      let S be SigmaField of X, M be sigma_Measure of S, F be sequence of ( COM (S,M)), G be sequence of S;

      defpred P[ Element of NAT , set] means for n be Element of NAT , y be set st n = $1 & y = $2 holds y = ((F . n) \ (G . n));

      

       A1: for t be Element of NAT holds ex A be Subset of X st P[t, A]

      proof

        let t be Element of NAT ;

        (F . t) is Element of ( COM (S,M));

        then

        reconsider A = ((F . t) \ (G . t)) as Subset of X by XBOOLE_1: 1;

        take A;

        thus thesis;

      end;

      ex H be sequence of ( bool X) st for t be Element of NAT holds P[t, (H . t)] from FUNCT_2:sch 3( A1);

      then

      consider H be sequence of ( bool X) such that

       A2: for t be Element of NAT holds for n be Element of NAT holds for y be set holds (n = t & y = (H . t) implies y = ((F . n) \ (G . n)));

      take H;

      thus thesis by A2;

    end;

    theorem :: MEASURE3:17

    

     Th17: for S be SigmaField of X, M be sigma_Measure of S, F be sequence of ( bool X) st (for n be Element of NAT holds (F . n) is thin of M) holds ex G be sequence of S st for n be Element of NAT holds (F . n) c= (G . n) & (M . (G . n)) = 0.

    proof

      let S be SigmaField of X, M be sigma_Measure of S, F be sequence of ( bool X);

      defpred P[ Element of NAT , set] means for n be Element of NAT , y be set st n = $1 & y = $2 holds y in S & (F . n) c= y & (M . y) = 0. ;

      assume

       A1: for n be Element of NAT holds (F . n) is thin of M;

      

       A2: for t be Element of NAT holds ex A be Element of S st P[t, A]

      proof

        let t be Element of NAT ;

        (F . t) is thin of M by A1;

        then

        consider A be set such that

         A3: A in S and

         A4: (F . t) c= A & (M . A) = 0. by Def2;

        reconsider A as Element of S by A3;

        take A;

        thus thesis by A4;

      end;

      ex G be sequence of S st for t be Element of NAT holds P[t, (G . t)] from FUNCT_2:sch 3( A2);

      then

      consider G be sequence of S such that

       A5: for t be Element of NAT , n be Element of NAT , y be set st n = t & y = (G . t) holds y in S & (F . n) c= y & (M . y) = 0. ;

      take G;

      thus thesis by A5;

    end;

    theorem :: MEASURE3:18

    

     Th18: for S be SigmaField of X, M be sigma_Measure of S, D be non empty Subset-Family of X st (for A be set holds (A in D iff ex B be set st B in S & ex C be thin of M st A = (B \/ C))) holds D is SigmaField of X

    proof

      let S be SigmaField of X, M be sigma_Measure of S, D be non empty Subset-Family of X;

      assume

       A1: for A be set holds A in D iff ex B be set st B in S & ex C be thin of M st A = (B \/ C);

      

       A2: for K be N_Sub_set_fam of X st K c= D holds ( union K) in D

      proof

        let K be N_Sub_set_fam of X;

        consider F be sequence of ( bool X) such that

         A3: K = ( rng F) by SUPINF_2:def 8;

        assume

         A4: K c= D;

        

         A5: for n be Element of NAT holds (F . n) in D

        proof

          let n be Element of NAT ;

          (F . n) in K by A3, FUNCT_2: 4;

          hence thesis by A4;

        end;

        

         A6: for n be Element of NAT holds ex B be set st B in S & ex C be thin of M st (F . n) = (B \/ C) by A5, A1;

        for n be Element of NAT holds (F . n) in ( COM (S,M))

        proof

          let n be Element of NAT ;

          ex B be set st B in S & ex C be thin of M st (F . n) = (B \/ C) by A6;

          hence thesis by Def3;

        end;

        then

         A7: for n be object st n in NAT holds (F . n) in ( COM (S,M));

        

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

        then

        reconsider F as sequence of ( COM (S,M)) by A7, FUNCT_2: 3;

        consider G be sequence of S such that

         A9: for n be Element of NAT holds (G . n) in ( MeasPart (F . n)) by Th15;

        consider H be sequence of ( bool X) such that

         A10: for n be Element of NAT holds (H . n) = ((F . n) \ (G . n)) by Th16;

        

         A11: for n be Element of NAT holds (G . n) in S & (G . n) c= (F . n) & ((F . n) \ (G . n)) is thin of M

        proof

          let n be Element of NAT ;

          (G . n) in ( MeasPart (F . n)) by A9;

          hence thesis by Def4;

        end;

        for n be Element of NAT holds (H . n) is thin of M

        proof

          let n be Element of NAT ;

          ((F . n) \ (G . n)) is thin of M by A11;

          hence thesis by A10;

        end;

        then

        consider L be sequence of S such that

         A12: for n be Element of NAT holds (H . n) c= (L . n) & (M . (L . n)) = 0. by Th17;

        ex B be set st B in S & ex C be thin of M st ( union K) = (B \/ C)

        proof

          set B = ( union ( rng G));

          take B;

          

           A13: ( union ( rng G)) c= ( union ( rng F))

          proof

            let x be object;

            assume x in ( union ( rng G));

            then

            consider Z be set such that

             A14: x in Z and

             A15: Z in ( rng G) by TARSKI:def 4;

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

            then

            consider n be object such that

             A16: n in NAT and

             A17: Z = (G . n) by A15, FUNCT_1:def 3;

            reconsider n as Element of NAT by A16;

            set P = (F . n);

            

             A18: (G . n) c= P by A11;

            ex P be set st P in ( rng F) & x in P

            proof

              take P;

              thus thesis by A8, A14, A17, A18, FUNCT_1:def 3;

            end;

            hence thesis by TARSKI:def 4;

          end;

          ex C be thin of M st ( union K) = (B \/ C)

          proof

            for A be set st A in ( rng L) holds A is measure_zero of M

            proof

              let A be set;

              assume

               A19: A in ( rng L);

              ( dom L) = NAT by FUNCT_2:def 1;

              then

               A20: ex n be object st n in NAT & A = (L . n) by A19, FUNCT_1:def 3;

              ( rng L) c= S by MEASURE2:def 1;

              then

              reconsider A as Element of S by A19;

              (M . A) = 0. by A12, A20;

              hence thesis by MEASURE1:def 7;

            end;

            then ( union ( rng L)) is measure_zero of M by MEASURE2: 14;

            then

             A21: (M . ( union ( rng L))) = 0. by MEASURE1:def 7;

            set C = (( union K) \ B);

            

             A22: ( union K) = (C \/ (( union ( rng F)) /\ ( union ( rng G)))) by A3, XBOOLE_1: 51

            .= (B \/ C) by A13, XBOOLE_1: 28;

            reconsider C as Subset of X;

            

             A23: C c= ( union ( rng H))

            proof

              let x be object;

              assume

               A24: x in C;

              then x in ( union ( rng F)) by A3, XBOOLE_0:def 5;

              then

              consider Z be set such that

               A25: x in Z and

               A26: Z in ( rng F) by TARSKI:def 4;

              consider n be object such that

               A27: n in NAT and

               A28: Z = (F . n) by A8, A26, FUNCT_1:def 3;

              reconsider n as Element of NAT by A27;

              

               A29: not x in ( union ( rng G)) by A24, XBOOLE_0:def 5;

               not x in (G . n)

              proof

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

                then

                 A30: (G . n) in ( rng G) by FUNCT_1:def 3;

                assume x in (G . n);

                hence thesis by A29, A30, TARSKI:def 4;

              end;

              then

               A31: x in ((F . n) \ (G . n)) by A25, A28, XBOOLE_0:def 5;

              ex Z be set st x in Z & Z in ( rng H)

              proof

                take (H . n);

                ( dom H) = NAT by FUNCT_2:def 1;

                hence thesis by A10, A31, FUNCT_1:def 3;

              end;

              hence thesis by TARSKI:def 4;

            end;

            ( union ( rng H)) c= ( union ( rng L))

            proof

              let x be object;

              assume x in ( union ( rng H));

              then

              consider Z be set such that

               A32: x in Z and

               A33: Z in ( rng H) by TARSKI:def 4;

              ( dom H) = NAT by FUNCT_2:def 1;

              then

              consider n be object such that

               A34: n in NAT and

               A35: Z = (H . n) by A33, FUNCT_1:def 3;

              reconsider n as Element of NAT by A34;

              n in ( dom L) by A34, FUNCT_2:def 1;

              then

               A36: (L . n) in ( rng L) by FUNCT_1:def 3;

              (H . n) c= (L . n) by A12;

              hence thesis by A32, A35, A36, TARSKI:def 4;

            end;

            then C c= ( union ( rng L)) by A23;

            then C is thin of M by A21, Def2;

            then

            consider C be thin of M such that

             A37: ( union K) = (B \/ C) by A22;

            take C;

            thus thesis by A37;

          end;

          hence thesis;

        end;

        hence thesis by A1;

      end;

      for A be set holds A in D implies (X \ A) in D

      proof

        let A be set;

        assume

         A38: A in D;

        ex Q be set st Q in S & ex W be thin of M st (X \ A) = (Q \/ W)

        proof

          consider B be set such that

           A39: B in S and

           A40: ex C be thin of M st A = (B \/ C) by A1, A38;

          set P = (X \ B);

          consider C be thin of M such that

           A41: A = (B \/ C) by A40;

          consider G be set such that

           A42: G in S and

           A43: C c= G and

           A44: (M . G) = 0. by Def2;

          set Q = (P \ G);

          

           A45: (X \ A) = (P \ C) by A41, XBOOLE_1: 41;

          

           A46: ex W be thin of M st (X \ A) = (Q \/ W)

          proof

            set W = (P /\ (G \ C));

            W c= P by XBOOLE_1: 17;

            then

            reconsider W as Subset of X by XBOOLE_1: 1;

            reconsider W as thin of M by A42, A44, Def2;

            take W;

            thus thesis by A43, A45, XBOOLE_1: 117;

          end;

          take Q;

          (X \ B) in S by A39, MEASURE1:def 1;

          hence thesis by A42, A46, MEASURE1: 6;

        end;

        hence thesis by A1;

      end;

      then

      reconsider D9 = D as compl-closed sigma-additive non empty Subset-Family of X by A2, MEASURE1:def 1, MEASURE1:def 5;

      D9 is SigmaField of X;

      hence thesis;

    end;

    registration

      let X be set;

      let S be SigmaField of X;

      let M be sigma_Measure of S;

      cluster ( COM (S,M)) -> sigma-additive compl-closed non empty;

      coherence

      proof

        for A be set holds A in ( COM (S,M)) iff ex B be set st B in S & ex C be thin of M st A = (B \/ C) by Def3;

        hence thesis by Th18;

      end;

    end

    theorem :: MEASURE3:19

    

     Th19: for S be SigmaField of X, M be sigma_Measure of S, B1,B2 be set st B1 in S & B2 in S holds for C1,C2 be thin of M holds (B1 \/ C1) = (B2 \/ C2) implies (M . B1) = (M . B2)

    proof

      let S be SigmaField of X, M be sigma_Measure of S, B1,B2 be set;

      assume

       A1: B1 in S & B2 in S;

      let C1,C2 be thin of M;

      assume

       A2: (B1 \/ C1) = (B2 \/ C2);

      then

       A3: B1 c= (B2 \/ C2) by XBOOLE_1: 7;

      

       A4: B2 c= (B1 \/ C1) by A2, XBOOLE_1: 7;

      consider D1 be set such that

       A5: D1 in S and

       A6: C1 c= D1 and

       A7: (M . D1) = 0. by Def2;

      

       A8: (B1 \/ C1) c= (B1 \/ D1) by A6, XBOOLE_1: 9;

      consider D2 be set such that

       A9: D2 in S and

       A10: C2 c= D2 and

       A11: (M . D2) = 0. by Def2;

      

       A12: (B2 \/ C2) c= (B2 \/ D2) by A10, XBOOLE_1: 9;

      reconsider B1, B2, D1, D2 as Element of S by A1, A5, A9;

      

       A13: (M . (B1 \/ D1)) <= ((M . B1) + (M . D1)) & ((M . B1) + (M . D1)) = (M . B1) by A7, MEASURE1: 33, XXREAL_3: 4;

      (M . B2) <= (M . (B1 \/ D1)) by A4, A8, MEASURE1: 31, XBOOLE_1: 1;

      then

       A14: (M . B2) <= (M . B1) by A13, XXREAL_0: 2;

      

       A15: (M . (B2 \/ D2)) <= ((M . B2) + (M . D2)) & ((M . B2) + (M . D2)) = (M . B2) by A11, MEASURE1: 33, XXREAL_3: 4;

      (M . B1) <= (M . (B2 \/ D2)) by A3, A12, MEASURE1: 31, XBOOLE_1: 1;

      then (M . B1) <= (M . B2) by A15, XXREAL_0: 2;

      hence thesis by A14, XXREAL_0: 1;

    end;

    definition

      let X be set;

      let S be SigmaField of X;

      let M be sigma_Measure of S;

      :: MEASURE3:def5

      func COM (M) -> sigma_Measure of ( COM (S,M)) means

      : Def5: for B be set st B in S holds for C be thin of M holds (it . (B \/ C)) = (M . B);

      existence

      proof

        set B = {} ;

        defpred P[ object, object] means for x,y be set st x in ( COM (S,M)) holds (x = $1 & y = $2 implies (for B be set st B in S holds for C be thin of M st x = (B \/ C) holds y = (M . B)));

        

         A1: ex B1 be set st B1 in S & {} c= B1 & (M . B1) = 0.

        proof

          take {} ;

          thus thesis by PROB_1: 4, VALUED_0:def 19;

        end;

         {} is Subset of X by XBOOLE_1: 2;

        then

        reconsider C = {} as thin of M by A1, Def2;

        

         A2: for x be object st x in ( COM (S,M)) holds ex y be object st y in ExtREAL & P[x, y]

        proof

          let x be object;

          assume x in ( COM (S,M));

          then

          consider B be set such that

           A3: B in S & ex C be thin of M st x = (B \/ C) by Def3;

          take (M . B);

          thus thesis by A3, Th19;

        end;

        consider comM be Function of ( COM (S,M)), ExtREAL such that

         A4: for x be object st x in ( COM (S,M)) holds P[x, (comM . x)] from FUNCT_2:sch 1( A2);

        

         A5: for B be set st B in S holds for C be thin of M holds (comM . (B \/ C)) = (M . B)

        proof

          let B be set;

          assume

           A6: B in S;

          let C be thin of M;

          (B \/ C) in ( COM (S,M)) by A6, Def3;

          hence thesis by A4, A6;

        end;

        

         A7: for F be Sep_Sequence of ( COM (S,M)) holds ( SUM (comM * F)) = (comM . ( union ( rng F)))

        proof

          let F be Sep_Sequence of ( COM (S,M));

          consider G be sequence of S such that

           A8: for n be Element of NAT holds (G . n) in ( MeasPart (F . n)) by Th15;

          consider H be sequence of ( bool X) such that

           A9: for n be Element of NAT holds (H . n) = ((F . n) \ (G . n)) by Th16;

          

           A10: for n be Element of NAT holds (G . n) in S & (G . n) c= (F . n) & ((F . n) \ (G . n)) is thin of M

          proof

            let n be Element of NAT ;

            (G . n) in ( MeasPart (F . n)) by A8;

            hence thesis by Def4;

          end;

          for n be Element of NAT holds (H . n) is thin of M

          proof

            let n be Element of NAT ;

            ((F . n) \ (G . n)) is thin of M by A10;

            hence thesis by A9;

          end;

          then

          consider L be sequence of S such that

           A11: for n be Element of NAT holds (H . n) c= (L . n) & (M . (L . n)) = 0. by Th17;

          

           A12: for n,m be object st n <> m holds (G . n) misses (G . m)

          proof

            let n,m be object;

            

             A13: ( dom F) = NAT by FUNCT_2:def 1

            .= ( dom G) by FUNCT_2:def 1;

            for n be object holds (G . n) c= (F . n)

            proof

              let n be object;

              per cases ;

                suppose n in ( dom F);

                hence thesis by A10;

              end;

                suppose

                 A14: not n in ( dom F);

                

                then (F . n) = {} by FUNCT_1:def 2

                .= (G . n) by A13, A14, FUNCT_1:def 2;

                hence thesis;

              end;

            end;

            then

             A15: (G . n) c= (F . n) & (G . m) c= (F . m);

            assume n <> m;

            then (F . n) misses (F . m) by PROB_2:def 2;

            then ((F . n) /\ (F . m)) = {} ;

            then ((G . n) /\ (G . m)) = {} by A15, XBOOLE_1: 3, XBOOLE_1: 27;

            hence thesis;

          end;

          consider B be set such that

           A16: B = ( union ( rng G));

          

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

          

           A18: B c= ( union ( rng F))

          proof

            let x be object;

            assume x in B;

            then

            consider Z be set such that

             A19: x in Z and

             A20: Z in ( rng G) by A16, TARSKI:def 4;

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

            then

            consider n be object such that

             A21: n in NAT and

             A22: Z = (G . n) by A20, FUNCT_1:def 3;

            reconsider n as Element of NAT by A21;

            set P = (F . n);

            

             A23: (G . n) c= P by A10;

            ex P be set st P in ( rng F) & x in P

            proof

              take P;

              thus thesis by A17, A19, A22, A23, FUNCT_1:def 3;

            end;

            hence thesis by TARSKI:def 4;

          end;

          

           A24: ex C be thin of M st ( union ( rng F)) = (B \/ C)

          proof

            for A be set st A in ( rng L) holds A is measure_zero of M

            proof

              let A be set;

              assume

               A25: A in ( rng L);

              ( dom L) = NAT by FUNCT_2:def 1;

              then

               A26: ex n be object st n in NAT & A = (L . n) by A25, FUNCT_1:def 3;

              ( rng L) c= S by MEASURE2:def 1;

              then

              reconsider A as Element of S by A25;

              (M . A) = 0. by A11, A26;

              hence thesis by MEASURE1:def 7;

            end;

            then ( union ( rng L)) is measure_zero of M by MEASURE2: 14;

            then

             A27: (M . ( union ( rng L))) = 0. by MEASURE1:def 7;

            set C = (( union ( rng F)) \ B);

            

             A28: ( union ( rng F)) = (C \/ (( union ( rng F)) /\ B)) by XBOOLE_1: 51

            .= (B \/ C) by A18, XBOOLE_1: 28;

            reconsider C as Subset of X;

            

             A29: C c= ( union ( rng H))

            proof

              let x be object;

              assume

               A30: x in C;

              then x in ( union ( rng F)) by XBOOLE_0:def 5;

              then

              consider Z be set such that

               A31: x in Z and

               A32: Z in ( rng F) by TARSKI:def 4;

              consider n be object such that

               A33: n in NAT and

               A34: Z = (F . n) by A17, A32, FUNCT_1:def 3;

              reconsider n as Element of NAT by A33;

              

               A35: not x in ( union ( rng G)) by A16, A30, XBOOLE_0:def 5;

               not x in (G . n)

              proof

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

                then

                 A36: (G . n) in ( rng G) by FUNCT_1:def 3;

                assume x in (G . n);

                hence thesis by A35, A36, TARSKI:def 4;

              end;

              then

               A37: x in ((F . n) \ (G . n)) by A31, A34, XBOOLE_0:def 5;

              ex Z be set st x in Z & Z in ( rng H)

              proof

                take (H . n);

                ( dom H) = NAT by FUNCT_2:def 1;

                hence thesis by A9, A37, FUNCT_1:def 3;

              end;

              hence thesis by TARSKI:def 4;

            end;

            ( union ( rng H)) c= ( union ( rng L))

            proof

              let x be object;

              assume x in ( union ( rng H));

              then

              consider Z be set such that

               A38: x in Z and

               A39: Z in ( rng H) by TARSKI:def 4;

              ( dom H) = NAT by FUNCT_2:def 1;

              then

              consider n be object such that

               A40: n in NAT and

               A41: Z = (H . n) by A39, FUNCT_1:def 3;

              reconsider n as Element of NAT by A40;

              n in ( dom L) by A40, FUNCT_2:def 1;

              then

               A42: (L . n) in ( rng L) by FUNCT_1:def 3;

              (H . n) c= (L . n) by A11;

              hence thesis by A38, A41, A42, TARSKI:def 4;

            end;

            then C c= ( union ( rng L)) by A29;

            then C is thin of M by A27, Def2;

            then

            consider C be thin of M such that

             A43: ( union ( rng F)) = (B \/ C) by A28;

            take C;

            thus thesis by A43;

          end;

          reconsider G as Sep_Sequence of S by A12, PROB_2:def 2;

          

           A44: for n be Element of NAT holds (comM . (F . n)) = (M . (G . n))

          proof

            let n be Element of NAT ;

            ((F . n) \ (G . n)) is thin of M by A10;

            then

            consider C be thin of M such that

             A45: C = ((F . n) \ (G . n));

            (F . n) = (((F . n) /\ (G . n)) \/ ((F . n) \ (G . n))) by XBOOLE_1: 51

            .= ((G . n) \/ C) by A10, A45, XBOOLE_1: 28;

            hence thesis by A5;

          end;

          

           A46: for n be Element of NAT holds ((comM * F) . n) = ((M * G) . n)

          proof

            let n be Element of NAT ;

            ((comM * F) . n) = (comM . (F . n)) by FUNCT_2: 15

            .= (M . (G . n)) by A44

            .= ((M * G) . n) by FUNCT_2: 15;

            hence thesis;

          end;

          then for n be Element of NAT holds ((M * G) . n) <= ((comM * F) . n);

          then

           A47: ( SUM (M * G)) <= ( SUM (comM * F)) by SUPINF_2: 43;

          for n be Element of NAT holds ((comM * F) . n) <= ((M * G) . n) by A46;

          then ( SUM (comM * F)) <= ( SUM (M * G)) by SUPINF_2: 43;

          then ( SUM (M * G)) = (M . ( union ( rng G))) & ( SUM (comM * F)) = ( SUM (M * G)) by A47, MEASURE1:def 6, XXREAL_0: 1;

          hence thesis by A5, A16, A24;

        end;

        

         A48: for x be Element of ( COM (S,M)) holds 0. <= (comM . x)

        proof

          let x be Element of ( COM (S,M));

          consider B be set such that

           A49: B in S and

           A50: ex C be thin of M st x = (B \/ C) by Def3;

          reconsider B as Element of S by A49;

          (comM . x) = (M . B) by A4, A50;

          hence thesis by MEASURE1:def 2;

        end;

         {} = (B \/ C);

        

        then (comM . {} ) = (M . {} ) by A5, PROB_1: 4

        .= 0. by VALUED_0:def 19;

        then

        reconsider comM as sigma_Measure of ( COM (S,M)) by A48, A7, MEASURE1:def 2, MEASURE1:def 6, VALUED_0:def 19;

        take comM;

        thus thesis by A5;

      end;

      uniqueness

      proof

        let M1,M2 be sigma_Measure of ( COM (S,M)) such that

         A51: for B be set st B in S holds for C be thin of M holds (M1 . (B \/ C)) = (M . B) and

         A52: for B be set st B in S holds for C be thin of M holds (M2 . (B \/ C)) = (M . B);

        for x be object st x in ( COM (S,M)) holds (M1 . x) = (M2 . x)

        proof

          let x be object;

          assume x in ( COM (S,M));

          then

          consider B be set such that

           A53: B in S & ex C be thin of M st x = (B \/ C) by Def3;

          (M1 . x) = (M . B) by A51, A53

          .= (M2 . x) by A52, A53;

          hence thesis;

        end;

        hence thesis by FUNCT_2: 12;

      end;

    end

    theorem :: MEASURE3:20

    for S be SigmaField of X, M be sigma_Measure of S holds ( COM M) is complete

    proof

      let S be SigmaField of X, M be sigma_Measure of S;

      for A be Subset of X, B be set st B in ( COM (S,M)) holds (A c= B & (( COM M) . B) = 0. implies A in ( COM (S,M)))

      proof

        let A be Subset of X;

        let B be set;

        assume

         A1: B in ( COM (S,M));

        assume that

         A2: A c= B and

         A3: (( COM M) . B) = 0. ;

        ex B1 be set st (B1 in S & ex C1 be thin of M st A = (B1 \/ C1))

        proof

          take {} ;

          consider B2 be set such that

           A4: B2 in S and

           A5: ex C2 be thin of M st B = (B2 \/ C2) by A1, Def3;

          

           A6: (M . B2) = 0. by A3, A4, A5, Def5;

          consider C2 be thin of M such that

           A7: B = (B2 \/ C2) by A5;

          set C1 = ((A /\ B2) \/ (A /\ C2));

          consider D2 be set such that

           A8: D2 in S and

           A9: C2 c= D2 and

           A10: (M . D2) = 0. by Def2;

          set O = (B2 \/ D2);

          (A /\ C2) c= C2 by XBOOLE_1: 17;

          then

           A11: (A /\ B2) c= B2 & (A /\ C2) c= D2 by A9, XBOOLE_1: 17;

          ex O be set st O in S & C1 c= O & (M . O) = 0.

          proof

            reconsider B2, D2 as Element of S by A4, A8;

            reconsider O1 = O as Element of S by A4, A8, FINSUB_1:def 1;

            take O;

            (M . (B2 \/ D2)) <= ( 0. + 0. ) & 0. <= (M . O1) by A6, A10, MEASURE1: 33, MEASURE1:def 2;

            hence thesis by A11, XBOOLE_1: 13, XXREAL_0: 1;

          end;

          then

           A12: C1 is thin of M by Def2;

          A = (A /\ (B2 \/ C2)) by A2, A7, XBOOLE_1: 28

          .= ( {} \/ C1) by XBOOLE_1: 23;

          hence thesis by A12, PROB_1: 4;

        end;

        hence thesis by Def3;

      end;

      hence thesis;

    end;