measure8.miz



    begin

    reserve X for set,

F for Field_Subset of X,

M for Measure of F,

A,B for Subset of X,

Sets for SetSequence of X,

seq,seq1,seq2 for ExtREAL_sequence,

n,k for Nat;

    theorem :: MEASURE8:1

    

     Th1: ( Ser seq) = ( Partial_Sums seq)

    proof

      for x be object st x in NAT holds (( Ser seq) . x) = (( Partial_Sums seq) . x)

      proof

        defpred P[ Nat] means (( Ser seq) . $1) = (( Partial_Sums seq) . $1);

        let x be object;

        

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

        proof

          let k be Nat;

          assume P[k];

          then (( Ser seq) . (k + 1)) = ((( Partial_Sums seq) . k) + (seq . (k + 1))) by SUPINF_2:def 11;

          hence P[(k + 1)] by MESFUNC9:def 1;

        end;

        assume x in NAT ;

        then

        reconsider n = x as Element of NAT ;

        (( Ser seq) . 0 ) = (seq . 0 ) by SUPINF_2:def 11

        .= (( Partial_Sums seq) . 0 ) by MESFUNC9:def 1;

        then

         A2: P[ 0 ];

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

        then (( Ser seq) . x) = (( Partial_Sums seq) . n);

        hence (( Ser seq) . x) = (( Partial_Sums seq) . x);

      end;

      hence ( Ser seq) = ( Partial_Sums seq) by FUNCT_2: 12;

    end;

    theorem :: MEASURE8:2

    

     Th2: seq is nonnegative implies seq is summable & ( SUM seq) = ( Sum seq)

    proof

      assume seq is nonnegative;

      then

       A1: ( Partial_Sums seq) is non-decreasing by MESFUNC9: 16;

      then ( Partial_Sums seq) is convergent by RINFSUP2: 37;

      hence seq is summable;

      ( lim ( Partial_Sums seq)) = ( sup ( Partial_Sums seq)) by A1, RINFSUP2: 37;

      hence ( Sum seq) = ( SUM seq) by Th1;

    end;

    theorem :: MEASURE8:3

    

     Th3: seq1 is nonnegative & seq2 is nonnegative & (for n be Nat holds (seq . n) = ((seq1 . n) + (seq2 . n))) implies seq is nonnegative & ( SUM seq) = (( SUM seq1) + ( SUM seq2)) & ( Sum seq) = (( Sum seq1) + ( Sum seq2))

    proof

      assume that

       A1: seq1 is nonnegative and

       A2: seq2 is nonnegative;

      reconsider Hseq = ( Ser seq2) as ExtREAL_sequence;

      reconsider Gseq = ( Ser seq1) as ExtREAL_sequence;

      reconsider Fseq = ( Ser seq) as ExtREAL_sequence;

      assume

       A3: for n be Nat holds (seq . n) = ((seq1 . n) + (seq2 . n));

      then

       A4: for n be Element of NAT holds (seq . n) = ((seq1 . n) + (seq2 . n));

      

       A5: for k be Nat holds (Fseq . k) = ((Gseq . k) + (Hseq . k)) by A1, A2, A4, MEASURE7: 3;

      for m,n be ExtReal st m in ( dom Fseq) & n in ( dom Fseq) & m <= n holds (Fseq . m) <= (Fseq . n)

      proof

        let m,n be ExtReal;

        assume that

         A6: m in ( dom Fseq) and

         A7: n in ( dom Fseq) and

         A8: m <= n;

        (Gseq . m) <= (Gseq . n) & (Hseq . m) <= (Hseq . n) by A1, A2, A6, A7, A8, MEASURE7: 8;

        then ((Gseq . m) + (Hseq . m)) <= ((Gseq . n) + (Hseq . n)) by XXREAL_3: 36;

        then (Fseq . m) <= ((Gseq . n) + (Hseq . n)) by A1, A2, A4, A6, MEASURE7: 3;

        hence thesis by A1, A2, A4, A7, MEASURE7: 3;

      end;

      then Fseq is non-decreasing by VALUED_0:def 15;

      then

       A9: ( lim Fseq) = ( sup Fseq) by RINFSUP2: 37;

      ( Partial_Sums seq1) is non-decreasing by A1, MESFUNC9: 16;

      then Gseq is non-decreasing by Th1;

      then

       A10: Gseq is convergent & ( lim Gseq) = ( sup Gseq) by RINFSUP2: 37;

      ( Partial_Sums seq2) is nonnegative by A2, MESFUNC9: 16;

      then

       A11: Hseq is nonnegative by Th1;

      now

        let n be object;

        assume n in ( dom seq);

        then

        reconsider n9 = n as Element of NAT ;

        

         A12: (seq2 . n9) >= 0 by A2, SUPINF_2: 51;

        (seq . n) = ((seq1 . n9) + (seq2 . n9)) & (seq1 . n9) >= 0 by A1, A3, SUPINF_2: 51;

        hence (seq . n) >= 0 by A12;

      end;

      hence

       A13: seq is nonnegative by SUPINF_2: 52;

      ( Partial_Sums seq2) is non-decreasing by A2, MESFUNC9: 16;

      then Hseq is non-decreasing by Th1;

      then

       A14: Hseq is convergent & ( lim Hseq) = ( sup Hseq) by RINFSUP2: 37;

      ( Partial_Sums seq1) is nonnegative by A1, MESFUNC9: 16;

      then Gseq is nonnegative by Th1;

      hence ( SUM seq) = (( SUM seq1) + ( SUM seq2)) by A10, A11, A14, A5, A9, MESFUNC9: 11;

      then ( Sum seq) = (( SUM seq1) + ( SUM seq2)) by A13, Th2;

      then ( Sum seq) = (( Sum seq1) + ( SUM seq2)) by A1, Th2;

      hence ( Sum seq) = (( Sum seq1) + ( Sum seq2)) by A2, Th2;

    end;

    registration

      let X, F;

      cluster disjoint_valued for sequence of F;

      existence

      proof

        consider f be sequence of { {} } such that

         A1: for n be Element of NAT holds (f . n) = {} by MEASURE1: 16;

         {} in F by PROB_1: 4;

        then { {} } c= F by ZFMISC_1: 31;

        then

        reconsider f as sequence of F by FUNCT_2: 7;

        take f;

        

         A2: for x be object holds (f . x) = {}

        proof

          let x be object;

          x in ( dom f) implies (f . x) = {} by A1;

          hence thesis by FUNCT_1:def 2;

        end;

        thus for x,y be object st x <> y holds (f . x) misses (f . y)

        proof

          let x,y be object;

          (f . x) = {} by A2;

          hence thesis by XBOOLE_1: 65;

        end;

      end;

    end

    definition

      let X, F;

      :: MEASURE8:def1

      mode FinSequence of F -> FinSequence of ( bool X) means

      : Def1: for k be Nat st k in ( dom it ) holds (it . k) in F;

      existence

      proof

        consider f be FinSequence of ( bool X) such that

         A1: for k be Nat st k in ( dom f) holds (f . k) = X by PROB_3: 47;

        take f;

        hereby

          let k be Nat;

          assume k in ( dom f);

          then (f . k) = X by A1;

          hence (f . k) in F by PROB_1: 5;

        end;

      end;

    end

    registration

      let X, F;

      cluster disjoint_valued for FinSequence of F;

      existence

      proof

         {} c= X;

        then

        reconsider f = <* {} *> as FinSequence of ( bool X) by FINSEQ_1: 74;

        for k be Nat st k in ( dom f) holds (f . k) in F

        proof

          let k be Nat;

          assume k in ( dom f);

          then k in ( Seg 1) by FINSEQ_1:def 8;

          then k = 1 by FINSEQ_1: 2, TARSKI:def 1;

          then (f . k) = {} by FINSEQ_1:def 8;

          hence (f . k) in F by PROB_1: 4;

        end;

        then

        reconsider f = <* {} *> as FinSequence of F by Def1;

        take f;

        

         A1: for n be object holds (f . n) = {}

        proof

          let n be object;

          now

            assume n in ( dom f);

            then n in ( Seg 1) by FINSEQ_1:def 8;

            then n = 1 by FINSEQ_1: 2, TARSKI:def 1;

            hence (f . n) = {} by FINSEQ_1:def 8;

          end;

          hence thesis by FUNCT_1:def 2;

        end;

        thus for x,y be object st x <> y holds (f . x) misses (f . y)

        proof

          let x,y be object;

          (f . x) = {} by A1;

          hence thesis by XBOOLE_1: 65;

        end;

      end;

    end

    definition

      let X, F;

      mode Sep_FinSequence of F is disjoint_valued FinSequence of F;

    end

    definition

      let X, F;

      mode Sep_Sequence of F is disjoint_valued sequence of F;

    end

    definition

      let X, F;

      :: MEASURE8:def2

      mode Set_Sequence of F -> SetSequence of X means

      : Def2: for n be Nat holds (it . n) in F;

      existence

      proof

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

        then

        reconsider A = ( NAT --> X) as SetSequence of X by FUNCOP_1: 45;

        take A;

        let n be Nat;

        n is Element of NAT by ORDINAL1:def 12;

        then (A . n) = X by FUNCOP_1: 7;

        hence thesis by PROB_1: 5;

      end;

    end

    definition

      let X, A, F;

      :: MEASURE8:def3

      mode Covering of A,F -> Set_Sequence of F means

      : Def3: A c= ( union ( rng it ));

      existence

      proof

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

        then

        reconsider IT = ( NAT --> X) as SetSequence of X by FUNCOP_1: 45;

        for n be Nat holds (IT . n) in F

        proof

          let n be Nat;

          n in NAT by ORDINAL1:def 12;

          then (IT . n) = X by FUNCOP_1: 7;

          hence (IT . n) in F by PROB_1: 5;

        end;

        then

        reconsider IT as Set_Sequence of F by Def2;

        take IT;

        ( rng IT) = {X} by FUNCOP_1: 8;

        then X c= ( union ( rng IT)) by ZFMISC_1: 25;

        hence thesis;

      end;

    end

    reserve FSets for Set_Sequence of F,

CA for Covering of A, F;

    definition

      let X, F, FSets, n;

      :: original: .

      redefine

      func FSets . n -> Element of F ;

      correctness by Def2;

    end

    

     Lm1: ( NAT --> X) is Set_Sequence of F

    proof

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

      then

      reconsider G0 = ( NAT --> X) as SetSequence of X by FUNCOP_1: 45;

      

       A1: ( rng ( NAT --> X)) = {X} by FUNCOP_1: 8;

      for n be Nat holds (G0 . n) in F

      proof

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        then (G0 . n) in {X} by A1, FUNCT_2: 4;

        then (G0 . n) = X by TARSKI:def 1;

        hence (G0 . n) in F by PROB_1: 5;

      end;

      hence ( NAT --> X) is Set_Sequence of F by Def2;

    end;

    definition

      let X, F, Sets;

      :: MEASURE8:def4

      mode Covering of Sets,F -> sequence of ( Funcs ( NAT ,( bool X))) means

      : Def4: for n be Nat holds (it . n) is Covering of (Sets . n), F;

      existence

      proof

        reconsider G0 = ( NAT --> X) as Set_Sequence of F by Lm1;

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

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

        take H;

        hereby

          let n be Nat;

          ( rng ( NAT --> X)) = {X} by FUNCOP_1: 8;

          then X c= ( union ( rng ( NAT --> X))) by ZFMISC_1: 25;

          then

           A1: (Sets . n) c= ( union ( rng ( NAT --> X)));

          n in NAT by ORDINAL1:def 12;

          then (H . n) = ( NAT --> X) by FUNCOP_1: 7;

          hence (H . n) is Covering of (Sets . n), F by A1, Def3;

        end;

      end;

    end

    reserve Cvr for Covering of Sets, F;

    definition

      let X, F, M, FSets;

      :: MEASURE8:def5

      func vol (M,FSets) -> ExtREAL_sequence means

      : Def5: for n holds (it . n) = (M . (FSets . n));

      existence

      proof

        deffunc H( Element of NAT ) = (M . (FSets . $1));

        consider IT be sequence of ExtREAL such that

         A1: for n be Element of NAT holds (IT . n) = H(n) from FUNCT_2:sch 4;

        take IT;

        hereby

          let n be Nat;

          n in NAT by ORDINAL1:def 12;

          hence (IT . n) = (M . (FSets . n)) by A1;

        end;

      end;

      uniqueness

      proof

        let V1,V2 be sequence of ExtREAL ;

        assume that

         A2: for n be Nat holds (V1 . n) = (M . (FSets . n)) and

         A3: for n be Nat holds (V2 . n) = (M . (FSets . n));

        now

          let x be object;

          assume x in NAT ;

          then

          reconsider n = x as Nat;

          

          thus (V1 . x) = (M . (FSets . n)) by A2

          .= (V2 . x) by A3;

        end;

        hence thesis by FUNCT_2: 12;

      end;

    end

    theorem :: MEASURE8:4

    

     Th4: ( vol (M,FSets)) is nonnegative

    proof

      for n be Element of NAT holds 0 <= (( vol (M,FSets)) . n)

      proof

        let n be Element of NAT ;

        (( vol (M,FSets)) . n) = (M . (FSets . n)) & {} in F by Def5, PROB_1: 4;

        then (M . {} ) <= (( vol (M,FSets)) . n) by MEASURE1: 8, XBOOLE_1: 2;

        hence 0 <= (( vol (M,FSets)) . n) by VALUED_0:def 19;

      end;

      hence thesis by SUPINF_2: 39;

    end;

    definition

      let X, F, Sets, Cvr, n;

      :: original: .

      redefine

      func Cvr . n -> Covering of (Sets . n), F ;

      correctness by Def4;

    end

    definition

      let X, F, Sets, M, Cvr;

      :: MEASURE8:def6

      func Volume (M,Cvr) -> ExtREAL_sequence means

      : Def6: for n be Nat holds (it . n) = ( SUM ( vol (M,(Cvr . n))));

      existence

      proof

        defpred P[ Element of NAT , Element of ExtREAL ] means $2 = ( SUM ( vol (M,(Cvr . $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;

        hereby

          let n be Nat;

          n in NAT by ORDINAL1:def 12;

          hence (G0 . n) = ( SUM ( vol (M,(Cvr . n)))) by A2;

        end;

      end;

      uniqueness

      proof

        let G1,G2 be sequence of ExtREAL ;

        assume that

         A3: for n be Nat holds (G1 . n) = ( SUM ( vol (M,(Cvr . n)))) and

         A4: for n be Nat holds (G2 . n) = ( SUM ( vol (M,(Cvr . n))));

        now

          let x be object;

          assume x in NAT ;

          then

          reconsider n = x as Nat;

          

          thus (G1 . x) = ( SUM ( vol (M,(Cvr . n)))) by A3

          .= (G2 . x) by A4;

        end;

        hence thesis by FUNCT_2: 12;

      end;

    end

    theorem :: MEASURE8:5

    

     Th5: 0 <= (( Volume (M,Cvr)) . n)

    proof

      for k be Element of NAT holds 0 <= (( vol (M,(Cvr . n))) . k)

      proof

        let k be Element of NAT ;

         0 <= (M . ((Cvr . n) . k)) by SUPINF_2: 51;

        hence thesis by Def5;

      end;

      then

       A1: ( vol (M,(Cvr . n))) is nonnegative by SUPINF_2: 39;

      (( Volume (M,Cvr)) . n) = ( SUM ( vol (M,(Cvr . n)))) by Def6;

      hence thesis by A1, MEASURE6: 2;

    end;

    definition

      let X, F, M, A;

      :: MEASURE8:def7

      func Svc (M,A) -> Subset of ExtREAL means

      : Def7: for x be R_eal holds x in it iff ex CA be Covering of A, F st x = ( SUM ( vol (M,CA)));

      existence

      proof

        defpred P[ object] means ex CA be Covering of A, F st $1 = ( SUM ( vol (M,CA)));

        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

        defpred P[ set] means ex CA be Covering of A, F st $1 = ( SUM ( vol (M,CA)));

        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 X, A, F, M;

      cluster ( Svc (M,A)) -> non empty;

      coherence

      proof

        X c= X & {} c= X;

        then

        consider CA be sequence of ( bool X) such that

         A1: ( rng CA) = {X, {} } and (CA . 0 ) = X and for n be Nat st 0 < n holds (CA . n) = {} by MEASURE1: 19;

        for n be Nat holds (CA . n) in F

        proof

          let n be Nat;

          n in NAT by ORDINAL1:def 12;

          then

           A2: (CA . n) in ( rng CA) by FUNCT_2: 4;

          X in F & {} in F by PROB_1: 4, PROB_1: 5;

          then ( rng CA) c= F by A1, ZFMISC_1: 32;

          hence (CA . n) in F by A2;

        end;

        then ( union {X, {} }) = (X \/ {} ) & CA is Set_Sequence of F by Def2, ZFMISC_1: 75;

        then

        reconsider CA as Covering of A, F by A1, Def3;

        defpred P[ object] means ex G be Covering of A, F st $1 = ( SUM ( vol (M,G)));

        consider D be set such that

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

        ( SUM ( vol (M,CA))) in D by A3;

        hence thesis by Def7;

      end;

    end

    definition

      let X, F, M;

      :: MEASURE8:def8

      func C_Meas M -> Function of ( bool X), ExtREAL means

      : Def8: for A be Subset of X holds (it . A) = ( inf ( Svc (M,A)));

      existence

      proof

        deffunc F( Element of ( bool X) qua set) = ( inf ( Svc (M,$1)));

        thus ex G be Function of ( bool X), ExtREAL st for A be Subset of X holds (G . A) = F(A) from FUNCT_2:sch 4;

      end;

      uniqueness

      proof

        deffunc F( Subset of X) = ( inf ( Svc (M,$1)));

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

      end;

    end

    definition

      :: MEASURE8:def9

      func InvPairFunc -> sequence of [: NAT , NAT :] equals ( PairFunc " );

      correctness by FUNCTOR1: 2, NAGATA_2: 2;

    end

    definition

      let X, F, Sets, Cvr;

      :: MEASURE8:def10

      func On Cvr -> Covering of ( union ( rng Sets)), F means

      : Def10: for n be Nat holds (it . n) = ((Cvr . (( pr1 InvPairFunc ) . n)) . (( pr2 InvPairFunc ) . n));

      existence

      proof

        defpred P[ Element of NAT , Subset of X] means $2 = ((Cvr . (( pr1 InvPairFunc ) . $1)) . (( pr2 InvPairFunc ) . $1));

        

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

        consider Seq0 be sequence of ( bool X) such that

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

        reconsider Seq0 as SetSequence of X;

        for n be Nat holds (Seq0 . n) in F

        proof

          let n be Nat;

          n in NAT by ORDINAL1:def 12;

          then (Seq0 . n) = ((Cvr . (( pr1 InvPairFunc ) . n)) . (( pr2 InvPairFunc ) . n)) by A2;

          hence (Seq0 . n) in F;

        end;

        then

        reconsider Seq0 as Set_Sequence of F by Def2;

        ( union ( rng Sets)) c= ( union ( rng Seq0))

        proof

          let x be object;

          assume x in ( union ( rng Sets));

          then

          consider A be set such that

           A3: x in A and

           A4: A in ( rng Sets) by TARSKI:def 4;

          consider n1 be Element of NAT such that

           A5: A = (Sets . n1) by A4, FUNCT_2: 113;

          (Sets . n1) c= ( union ( rng (Cvr . n1))) by Def3;

          then

          consider AA be set such that

           A6: x in AA and

           A7: AA in ( rng (Cvr . n1)) by A3, A5, TARSKI:def 4;

          consider n2 be Element of NAT such that

           A8: AA = ((Cvr . n1) . n2) by A7, FUNCT_2: 113;

          ( dom PairFunc ) = ( rng InvPairFunc ) by FUNCT_1: 33, NAGATA_2: 2;

          then ( rng InvPairFunc ) = [: NAT , NAT :] by FUNCT_2:def 1;

          then [n1, n2] in ( rng InvPairFunc ) by ZFMISC_1:def 2;

          then

          consider n be Element of NAT such that

           A9: [n1, n2] = ( InvPairFunc . n) by FUNCT_2: 113;

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

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

          then

           A10: x in (Seq0 . n) by A2, A6, A8;

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

          hence thesis by A10, TARSKI:def 4;

        end;

        then

        reconsider Seq0 as Covering of ( union ( rng Sets)), F by Def3;

        take Seq0;

        hereby

          let n be Nat;

          n in NAT by ORDINAL1:def 12;

          hence (Seq0 . n) = ((Cvr . (( pr1 InvPairFunc ) . n)) . (( pr2 InvPairFunc ) . n)) by A2;

        end;

      end;

      uniqueness

      proof

        let Seq1,Seq2 be Covering of ( union ( rng Sets)), F such that

         A11: for n be Nat holds (Seq1 . n) = ((Cvr . (( pr1 InvPairFunc ) . n)) . (( pr2 InvPairFunc ) . n)) and

         A12: for n be Nat holds (Seq2 . n) = ((Cvr . (( pr1 InvPairFunc ) . n)) . (( pr2 InvPairFunc ) . n));

        for n be object st n in NAT holds (Seq1 . n) = (Seq2 . n)

        proof

          let n be object;

          assume n in NAT ;

          then

          reconsider n as Element of NAT ;

          (Seq1 . n) = ((Cvr . (( pr1 InvPairFunc ) . n)) . (( pr2 InvPairFunc ) . n)) by A11;

          hence thesis by A12;

        end;

        hence thesis by FUNCT_2: 12;

      end;

    end

    theorem :: MEASURE8:6

    

     Th6: for k be Nat holds ex m be Nat st for Sets be SetSequence of X holds for Cvr be Covering of Sets, F holds (( Partial_Sums ( vol (M,( On Cvr)))) . k) <= (( Partial_Sums ( Volume (M,Cvr))) . m)

    proof

      defpred P[ Nat] means ex m be Nat st for Sets be SetSequence of X holds for Cvr be Covering of Sets, F holds (( Partial_Sums ( vol (M,( On Cvr)))) . $1) <= (( Partial_Sums ( Volume (M,Cvr))) . m);

       {} c= X;

      then

      reconsider D = ( NAT --> {} ) as sequence of ( bool X) by FUNCOP_1: 45;

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

      

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

      proof

        let k be Nat;

        set a = (( pr1 InvPairFunc ) . (k + 1));

        set b = (( pr2 InvPairFunc ) . (k + 1));

        set N0 = { s where s be Element of NAT : a = (( pr1 InvPairFunc ) . s) };

        

         A2: N0 c= NAT

        proof

          let s1 be object;

          assume s1 in N0;

          then ex s be Element of NAT st s = s1 & a = (( pr1 InvPairFunc ) . s);

          hence thesis;

        end;

        (k + 1) in N0;

        then

        reconsider N0 as non empty Subset of NAT by A2;

        given m0 be Nat such that

         A3: for Sets be SetSequence of X holds for Cvr be Covering of Sets, F holds (( Partial_Sums ( vol (M,( On Cvr)))) . k) <= (( Partial_Sums ( Volume (M,Cvr))) . m0);

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

        let Sets be SetSequence of X;

        let Cvr be Covering of Sets, F;

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

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

        

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

        proof

          let n be Element of NAT ;

           A5:

          now

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

            assume

             A6: n = a;

            take y;

            thus QQ0[n, y] by A6;

          end;

          n <> a implies QQ0[n, y] by FUNCOP_1: 7;

          hence thesis by A5;

        end;

        consider Cvr0 be sequence of ( Funcs ( NAT ,( bool X))) such that

         A7: for n be Element of NAT holds QQ0[n, (Cvr0 . n)] from FUNCT_2:sch 3( A4);

        

         A8: for n be Nat holds (Cvr0 . n) is Covering of (D . n), F

        proof

          let n be Nat;

          consider FSets0 be Function such that

           A9: (Cvr0 . n) = FSets0 and

           A10: ( dom FSets0) = NAT & ( rng FSets0) c= ( bool X) by FUNCT_2:def 2;

          reconsider FSets0 as SetSequence of X by A10, FUNCT_2: 2;

          for s be Nat holds (FSets0 . s) in F

          proof

            let s be Nat;

            

             A11: s in NAT by ORDINAL1:def 12;

             A12:

            now

              assume n = a;

              then (FSets0 . s) = ((Cvr . n) . s) by A7, A9, A11;

              hence (FSets0 . s) in F;

            end;

            n in NAT by ORDINAL1:def 12;

            then n <> a implies (FSets0 . s) = {} by A7, A9, A11;

            hence thesis by A12, PROB_1: 4;

          end;

          then

           A13: FSets0 is Set_Sequence of F by Def2;

          n in NAT by ORDINAL1:def 12;

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

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

          hence (Cvr0 . n) is Covering of (D . n), F by A9, A13, Def3;

        end;

        

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

        proof

          let n be Element of NAT ;

           A15:

          now

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

            assume

             A16: n <> a;

            take y;

            thus QQ1[n, y] by A16;

          end;

          n = a implies QQ1[n, y] by FUNCOP_1: 7;

          hence thesis by A15;

        end;

        consider Cvr1 be sequence of ( Funcs ( NAT ,( bool X))) such that

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

        for n be Nat holds (Cvr1 . n) is Covering of (D . n), F

        proof

          let n be Nat;

          consider FSets1 be Function such that

           A18: (Cvr1 . n) = FSets1 and

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

          reconsider FSets1 as sequence of ( bool X) by A19, FUNCT_2: 2;

          for s be Nat holds (FSets1 . s) in F

          proof

            let s be Nat;

            

             A20: s in NAT by ORDINAL1:def 12;

            

             A21: n in NAT by ORDINAL1:def 12;

             A22:

            now

              assume n <> a;

              then (FSets1 . s) = ((Cvr . n) . s) by A17, A18, A21, A20;

              hence (FSets1 . s) in F;

            end;

            n = a implies (FSets1 . s) = {} by A17, A18, A20;

            hence thesis by A22, PROB_1: 4;

          end;

          then

           A23: FSets1 is Set_Sequence of F by Def2;

          n in NAT by ORDINAL1:def 12;

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

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

          hence (Cvr1 . n) is Covering of (D . n), F by A18, A23, Def3;

        end;

        then

        reconsider Cvr1 as Covering of D, F by Def4;

        reconsider Cvr0 as Covering of D, F by A8, Def4;

        set PSv1 = ( Partial_Sums ( vol (M,( On Cvr1))));

        (( On Cvr1) . (k + 1)) = ((Cvr1 . a) . b) by Def10

        .= {} by A17;

        

        then

         A24: (( vol (M,( On Cvr1))) . (k + 1)) = (M . {} ) by Def5

        .= 0 by VALUED_0:def 19;

        set PSv0 = ( Partial_Sums ( vol (M,( On Cvr0))));

        set PSv = ( Partial_Sums ( vol (M,( On Cvr))));

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

        

         A25: 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

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

        

         A27: for s be Element of NAT holds (s in N0 implies (( vol (M,( On Cvr0))) . s) = ((( vol (M,(Cvr0 . a))) * SOS) . s)) & ( not s in N0 implies (( vol (M,( On Cvr0))) . s) = 0 )

        proof

          let s be Element of NAT ;

          thus s in N0 implies (( vol (M,( On Cvr0))) . s) = ((( vol (M,(Cvr0 . a))) * SOS) . s)

          proof

            

             A28: (( vol (M,( On Cvr0))) . s) = (M . (( On Cvr0) . s)) by Def5;

            assume

             A29: s in N0;

            then (ex s1 be Element of NAT st s1 = s & a = (( pr1 InvPairFunc ) . s1)) & (( pr2 InvPairFunc ) . s) = (SOS . s) by A26;

            then (( vol (M,( On Cvr0))) . s) = (M . ((Cvr0 . a) . (SOS . s))) by A28, Def10;

            then (( vol (M,( On Cvr0))) . s) = (( vol (M,(Cvr0 . a))) . (SOS . s)) by Def5;

            hence thesis by A29, FUNCT_2: 15;

          end;

          assume not s in N0;

          then

           A30: not a = (( pr1 InvPairFunc ) . s);

          (( vol (M,( On Cvr0))) . s) = (M . (( On Cvr0) . s)) by Def5

          .= (M . ((Cvr0 . (( pr1 InvPairFunc ) . s)) . (( pr2 InvPairFunc ) . s))) by Def10

          .= (M . {} ) by A7, A30;

          hence thesis by VALUED_0:def 19;

        end;

        now

          let s1,s2 be object;

          assume that

           A31: s1 in N0 & s2 in N0 and

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

          

           A33: (ex s11 be Element of NAT st s11 = s1 & a = (( pr1 InvPairFunc ) . s11)) & ex s22 be Element of NAT st s22 = s2 & a = (( pr1 InvPairFunc ) . s22) by A31;

          

           A34: ( InvPairFunc . s1) = [(( pr1 InvPairFunc ) . s1), (( pr2 InvPairFunc ) . s1)] & ( InvPairFunc . s2) = [(( pr1 InvPairFunc ) . s2), (( pr2 InvPairFunc ) . s2)] by A31, FUNCT_2: 119;

          (SOS . s1) = (( pr2 InvPairFunc ) . s1) & (SOS . s2) = (( pr2 InvPairFunc ) . s2) by A26, A31;

          hence s1 = s2 by A32, A33, A34, FUNCT_2: 19, NAGATA_2: 2;

        end;

        then

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

        (( Ser ( vol (M,( On Cvr1)))) . (k + 1)) = ((( Ser ( vol (M,( On Cvr1)))) . k) + (( vol (M,( On Cvr1))) . (k + 1))) by SUPINF_2:def 11

        .= (( Ser ( vol (M,( On Cvr1)))) . k) by A24, XXREAL_3: 4;

        then (PSv1 . (k + 1)) = (( Ser ( vol (M,( On Cvr1)))) . k) by Th1;

        then

         A36: (PSv1 . (k + 1)) = (PSv1 . k) by Th1;

        for s be Element of NAT holds 0. <= (( Volume (M,Cvr0)) . s) by Th5;

        then

         A37: ( Volume (M,Cvr0)) is nonnegative by SUPINF_2: 39;

        then (( Volume (M,Cvr0)) . a) <= (( Ser ( Volume (M,Cvr0))) . a) by MEASURE7: 2;

        then

         A38: ( SUM ( vol (M,(Cvr0 . a)))) <= (( Ser ( Volume (M,Cvr0))) . a) by Def6;

        (( Ser ( Volume (M,Cvr0))) . a) <= (( Ser ( Volume (M,Cvr0))) . m) by A37, SUPINF_2: 41;

        then

         A39: ( SUM ( vol (M,(Cvr0 . a)))) <= (( Ser ( Volume (M,Cvr0))) . m) by A38, XXREAL_0: 2;

        ( vol (M,(Cvr0 . a))) is nonnegative by Th4;

        then ( SUM ( vol (M,( On Cvr0)))) <= ( SUM ( vol (M,(Cvr0 . a)))) by A35, A27, MEASURE7: 11;

        then

         A40: ( SUM ( vol (M,( On Cvr0)))) <= (( Ser ( Volume (M,Cvr0))) . m) by A39, XXREAL_0: 2;

        (( Ser ( vol (M,( On Cvr0)))) . (k + 1)) <= ( SUM ( vol (M,( On Cvr0)))) by Th4, MEASURE7: 6;

        then (( Ser ( vol (M,( On Cvr0)))) . (k + 1)) <= (( Ser ( Volume (M,Cvr0))) . m) by A40, XXREAL_0: 2;

        then (PSv0 . (k + 1)) <= (( Ser ( Volume (M,Cvr0))) . m) by Th1;

        then

         A41: (PSv0 . (k + 1)) <= (( Partial_Sums ( Volume (M,Cvr0))) . m) by Th1;

        for s be Element of NAT holds 0. <= (( Volume (M,Cvr1)) . s) by Th5;

        then

         A42: ( Volume (M,Cvr1)) is nonnegative by SUPINF_2: 39;

        then m0 <= m & ( Partial_Sums ( Volume (M,Cvr1))) is non-decreasing by MESFUNC9: 16, NAT_1: 11;

        then

         A43: (( Partial_Sums ( Volume (M,Cvr1))) . m0) <= (( Partial_Sums ( Volume (M,Cvr1))) . m) by RINFSUP2: 7;

        

         A44: for n be Element of NAT holds (( vol (M,( On Cvr))) . n) = ((( vol (M,( On Cvr0))) . n) + (( vol (M,( On Cvr1))) . n))

        proof

          let n be Element of NAT ;

          set n1 = (( pr1 InvPairFunc ) . n);

          set n2 = (( pr2 InvPairFunc ) . n);

          

           A45: (( vol (M,( On Cvr0))) . n) = (M . (( On Cvr0) . n)) & (( vol (M,( On Cvr1))) . n) = (M . (( On Cvr1) . n)) by Def5;

          (( vol (M,( On Cvr))) . n) = (M . (( On Cvr) . n)) by Def5;

          then

           A46: (( vol (M,( On Cvr))) . n) = (M . ((Cvr . n1) . n2)) by Def10;

          per cases ;

            suppose

             A47: n1 = a;

            (( On Cvr1) . n) = ((Cvr1 . n1) . n2) by Def10

            .= {} by A17, A47;

            then

             A48: (M . (( On Cvr1) . n)) = 0 by VALUED_0:def 19;

            (( On Cvr0) . n) = ((Cvr0 . n1) . n2) by Def10

            .= ((Cvr . n1) . n2) by A7, A47;

            hence thesis by A45, A46, A48, XXREAL_3: 4;

          end;

            suppose

             A49: n1 <> a;

            (( On Cvr0) . n) = ((Cvr0 . n1) . n2) by Def10

            .= {} by A7, A49;

            then

             A50: (M . (( On Cvr0) . n)) = 0 by VALUED_0:def 19;

            (( On Cvr1) . n) = ((Cvr1 . n1) . n2) by Def10

            .= ((Cvr . n1) . n2) by A17, A49;

            hence thesis by A45, A46, A50, XXREAL_3: 4;

          end;

        end;

        ( vol (M,( On Cvr0))) is nonnegative & ( vol (M,( On Cvr1))) is nonnegative by Th4;

        then (( Ser ( vol (M,( On Cvr)))) . (k + 1)) = ((( Ser ( vol (M,( On Cvr0)))) . (k + 1)) + (( Ser ( vol (M,( On Cvr1)))) . (k + 1))) by A44, MEASURE7: 3;

        then (PSv . (k + 1)) = ((( Ser ( vol (M,( On Cvr0)))) . (k + 1)) + (( Ser ( vol (M,( On Cvr1)))) . (k + 1))) by Th1;

        then (PSv . (k + 1)) = ((PSv0 . (k + 1)) + (( Ser ( vol (M,( On Cvr1)))) . (k + 1))) by Th1;

        then

         A51: (PSv . (k + 1)) = ((PSv0 . (k + 1)) + (PSv1 . (k + 1))) by Th1;

        (PSv1 . k) <= (( Partial_Sums ( Volume (M,Cvr1))) . m0) by A3;

        then

         A52: (PSv1 . (k + 1)) <= (( Partial_Sums ( Volume (M,Cvr1))) . m) by A36, A43, XXREAL_0: 2;

        for n be Element of NAT holds (( Volume (M,Cvr)) . n) = ((( Volume (M,Cvr0)) . n) + (( Volume (M,Cvr1)) . n))

        proof

          let n be Element of NAT ;

           A53:

          now

            assume

             A54: n <> a;

            for s be Element of NAT holds (( vol (M,(Cvr0 . n))) . s) = 0.

            proof

              let s be Element of NAT ;

              ((Cvr0 . n) . s) = {} by A7, A54;

              then (M . ((Cvr0 . n) . s)) = 0 by VALUED_0:def 19;

              hence thesis by Def5;

            end;

            then

             A55: ( SUM ( vol (M,(Cvr0 . n)))) = 0. by MEASURE7: 1;

            for s be Element of NAT holds (( vol (M,(Cvr1 . n))) . s) <= (( vol (M,(Cvr . n))) . s) & (( vol (M,(Cvr . n))) . s) <= (( vol (M,(Cvr1 . n))) . s)

            proof

              let s be Element of NAT ;

              (( vol (M,(Cvr1 . n))) . s) = (M . ((Cvr1 . n) . s)) & (( vol (M,(Cvr . n))) . s) = (M . ((Cvr . n) . s)) by Def5;

              hence thesis by A17, A54;

            end;

            then ( SUM ( vol (M,(Cvr1 . n)))) <= ( SUM ( vol (M,(Cvr . n)))) & ( SUM ( vol (M,(Cvr . n)))) <= ( SUM ( vol (M,(Cvr1 . n)))) by SUPINF_2: 43;

            then ( SUM ( vol (M,(Cvr . n)))) = ( SUM ( vol (M,(Cvr1 . n)))) by XXREAL_0: 1;

            hence ( SUM ( vol (M,(Cvr . n)))) = (( SUM ( vol (M,(Cvr0 . n)))) + ( SUM ( vol (M,(Cvr1 . n))))) by A55, XXREAL_3: 4;

          end;

           A56:

          now

            assume

             A57: n = a;

            for s be Element of NAT holds (( vol (M,(Cvr1 . n))) . s) = 0

            proof

              let s be Element of NAT ;

              ((Cvr1 . n) . s) = {} by A17, A57;

              then (M . ((Cvr1 . n) . s)) = 0 by VALUED_0:def 19;

              hence (( vol (M,(Cvr1 . n))) . s) = 0 by Def5;

            end;

            then

             A58: ( SUM ( vol (M,(Cvr1 . n)))) = 0 by MEASURE7: 1;

            for s be Element of NAT holds (( vol (M,(Cvr . n))) . s) <= (( vol (M,(Cvr0 . n))) . s) & (( vol (M,(Cvr0 . n))) . s) <= (( vol (M,(Cvr . n))) . s)

            proof

              let s be Element of NAT ;

              (( vol (M,(Cvr0 . n))) . s) = (M . ((Cvr0 . n) . s)) by Def5

              .= (M . ((Cvr . n) . s)) by A7, A57;

              hence thesis by Def5;

            end;

            then ( SUM ( vol (M,(Cvr . n)))) <= ( SUM ( vol (M,(Cvr0 . n)))) & ( SUM ( vol (M,(Cvr0 . n)))) <= ( SUM ( vol (M,(Cvr . n)))) by SUPINF_2: 43;

            then ( SUM ( vol (M,(Cvr . n)))) = ( SUM ( vol (M,(Cvr0 . n)))) by XXREAL_0: 1;

            hence ( SUM ( vol (M,(Cvr . n)))) = (( SUM ( vol (M,(Cvr0 . n)))) + ( SUM ( vol (M,(Cvr1 . n))))) by A58, XXREAL_3: 4;

          end;

          (( Volume (M,Cvr)) . n) = ( SUM ( vol (M,(Cvr . n)))) & (( Volume (M,Cvr0)) . n) = ( SUM ( vol (M,(Cvr0 . n)))) by Def6;

          hence thesis by A56, A53, Def6;

        end;

        then (( Ser ( Volume (M,Cvr))) . m) = ((( Ser ( Volume (M,Cvr0))) . m) + (( Ser ( Volume (M,Cvr1))) . m)) by A37, A42, MEASURE7: 3;

        

        then (( Partial_Sums ( Volume (M,Cvr))) . m) = ((( Ser ( Volume (M,Cvr0))) . m) + (( Ser ( Volume (M,Cvr1))) . m)) by Th1

        .= ((( Partial_Sums ( Volume (M,Cvr0))) . m) + (( Ser ( Volume (M,Cvr1))) . m)) by Th1

        .= ((( Partial_Sums ( Volume (M,Cvr0))) . m) + (( Partial_Sums ( Volume (M,Cvr1))) . m)) by Th1;

        hence thesis by A41, A52, A51, XXREAL_3: 36;

      end;

      

       A59: P[ 0 ]

      proof

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

        let Sets be SetSequence of X;

        let Cvr be Covering of Sets, F;

        for n be Element of NAT holds 0 <= (( Volume (M,Cvr)) . n) by Th5;

        then ( Volume (M,Cvr)) is nonnegative by SUPINF_2: 39;

        then (( Volume (M,Cvr)) . m) <= (( Ser ( Volume (M,Cvr))) . m) by MEASURE7: 2;

        then

         A60: (( Volume (M,Cvr)) . m) <= (( Partial_Sums ( Volume (M,Cvr))) . m) by Th1;

        (( vol (M,( On Cvr))) . 0 ) = (M . (( On Cvr) . 0 )) & (( vol (M,(Cvr . (( pr1 InvPairFunc ) . 0 )))) . (( pr2 InvPairFunc ) . 0 )) = (M . ((Cvr . (( pr1 InvPairFunc ) . 0 )) . (( pr2 InvPairFunc ) . 0 ))) by Def5;

        then (( vol (M,( On Cvr))) . 0 ) <= (( vol (M,(Cvr . (( pr1 InvPairFunc ) . 0 )))) . (( pr2 InvPairFunc ) . 0 )) by Def10;

        then (( vol (M,( On Cvr))) . 0 ) <= ( SUM ( vol (M,(Cvr . (( pr1 InvPairFunc ) . 0 ))))) by Th4, MEASURE6: 3;

        then (( Partial_Sums ( vol (M,( On Cvr)))) . 0 ) = (( vol (M,( On Cvr))) . 0 ) & (( vol (M,( On Cvr))) . 0 ) <= (( Volume (M,Cvr)) . (( pr1 InvPairFunc ) . 0 )) by Def6, MESFUNC9:def 1;

        hence thesis by A60, XXREAL_0: 2;

      end;

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

    end;

    theorem :: MEASURE8:7

    

     Th7: ( inf ( Svc (M,( union ( rng Sets))))) <= ( SUM ( Volume (M,Cvr)))

    proof

      set Q = ( SUM ( vol (M,( On Cvr))));

      for x be ExtReal st x in ( rng ( Ser ( vol (M,( On Cvr))))) holds ex y be ExtReal st y in ( rng ( Ser ( Volume (M,Cvr)))) & x <= y

      proof

        let x be ExtReal;

        assume x in ( rng ( Ser ( vol (M,( On Cvr)))));

        then

        consider n be Element of NAT such that

         A1: x = (( Ser ( vol (M,( On Cvr)))) . n) by FUNCT_2: 113;

        consider m be Nat such that

         A2: for Sets be SetSequence of X holds for G be Covering of Sets, F holds (( Partial_Sums ( vol (M,( On G)))) . n) <= (( Partial_Sums ( Volume (M,G))) . m) by Th6;

        take (( Ser ( Volume (M,Cvr))) . m);

        

         A3: for Sets be SetSequence of X, G be Covering of Sets, F holds (( Ser ( vol (M,( On G)))) . n) <= (( Ser ( Volume (M,G))) . m)

        proof

          let Sets be SetSequence of X;

          let G be Covering of Sets, F;

          (( Partial_Sums ( vol (M,( On G)))) . n) <= (( Partial_Sums ( Volume (M,G))) . m) by A2;

          then (( Ser ( vol (M,( On G)))) . n) <= (( Partial_Sums ( Volume (M,G))) . m) by Th1;

          hence (( Ser ( vol (M,( On G)))) . n) <= (( Ser ( Volume (M,G))) . m) by Th1;

        end;

        m in NAT by ORDINAL1:def 12;

        hence thesis by A1, A3, FUNCT_2: 4;

      end;

      then

       A4: ( SUM ( vol (M,( On Cvr)))) <= ( SUM ( Volume (M,Cvr))) by XXREAL_2: 63;

      Q in ( Svc (M,( union ( rng Sets)))) by Def7;

      then ( inf ( Svc (M,( union ( rng Sets))))) <= Q by XXREAL_2: 3;

      hence thesis by A4, XXREAL_0: 2;

    end;

    theorem :: MEASURE8:8

    

     Th8: A in F implies ((A,( {} X)) followed_by ( {} X)) is Covering of A, F

    proof

      reconsider Sets = ((A,( {} X)) followed_by ( {} X)) as SetSequence of X;

      

       A1: (Sets . 0 ) = A by FUNCT_7: 122;

      

       A2: (Sets . 1) = ( {} X) by FUNCT_7: 123;

      assume

       A3: A in F;

      for n be Nat holds (Sets . n) in F

      proof

        let n be Nat;

        per cases by NAT_1: 25;

          suppose n = 0 ;

          hence (Sets . n) in F by A3, FUNCT_7: 122;

        end;

          suppose n = 1;

          hence (Sets . n) in F by A2, PROB_1: 4;

        end;

          suppose n > 1;

          then (Sets . n) = {} by FUNCT_7: 124;

          hence (Sets . n) in F by PROB_1: 4;

        end;

      end;

      then

      reconsider Sets as Set_Sequence of F by Def2;

      A c= ( union ( rng Sets))

      proof

        let x be object;

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

        then

         A4: (Sets . 0 ) in ( rng Sets) by FUNCT_1: 3;

        assume x in A;

        hence x in ( union ( rng Sets)) by A1, A4, TARSKI:def 4;

      end;

      hence ((A,( {} X)) followed_by ( {} X)) is Covering of A, F by Def3;

    end;

    theorem :: MEASURE8:9

    

     Th9: for X be set, F be Field_Subset of X, M be Measure of F, A be set st A in F holds (( C_Meas M) . A) <= (M . A)

    proof

      let X be set;

      let F be Field_Subset of X;

      let M be Measure of F;

      let A9 be set;

      assume

       A1: A9 in F;

      then

      reconsider A = A9 as Subset of X;

      reconsider Aseq = ((A,( {} X)) followed_by ( {} X)) as Set_Sequence of F by A1, Th8;

      

       A2: (Aseq . 1) = ( {} X) by FUNCT_7: 123;

      

       A3: (Aseq . 0 ) = A by FUNCT_7: 122;

      A c= ( union ( rng Aseq))

      proof

        let x be object;

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

        then

         A4: (Aseq . 0 ) in ( rng Aseq) by FUNCT_1: 3;

        assume x in A;

        hence x in ( union ( rng Aseq)) by A3, A4, TARSKI:def 4;

      end;

      then

      reconsider Aseq as Covering of A, F by Def3;

      

       A5: for n be Element of NAT st n <> 0 holds (( vol (M,Aseq)) . n) = 0

      proof

        let n be Element of NAT ;

        assume n <> 0 ;

        then (Aseq . n) = {} by A2, FUNCT_7: 124, NAT_1: 25;

        then (( vol (M,Aseq)) . n) = (M . {} ) by Def5;

        hence (( vol (M,Aseq)) . n) = 0 by VALUED_0:def 19;

      end;

      then for n be Element of NAT st 1 <= n holds (( vol (M,Aseq)) . n) = 0 ;

      

      then ( SUM ( vol (M,Aseq))) = (( Ser ( vol (M,Aseq))) . 1) by Th4, SUPINF_2: 48

      .= (( vol (M,Aseq)) . 0 ) by A5, MEASURE7: 9;

      then ( SUM ( vol (M,Aseq))) = (M . (Aseq . 0 )) by Def5;

      then

       A6: (M . A) in ( Svc (M,A)) by A3, Def7;

      (( C_Meas M) . A) = ( inf ( Svc (M,A))) by Def8;

      hence (( C_Meas M) . A9) <= (M . A9) by A6, XXREAL_2: 3;

    end;

    theorem :: MEASURE8:10

    

     Th10: ( C_Meas M) is nonnegative

    proof

      for r be ExtReal st r in ( rng ( C_Meas M)) holds 0 <= r

      proof

        let r be ExtReal;

        assume r in ( rng ( C_Meas M));

        then

        consider A be object such that

         A1: A in ( bool X) and

         A2: (( C_Meas M) . A) = r by FUNCT_2: 11;

        reconsider A as Subset of X by A1;

        now

          let p be ExtReal;

          assume p in ( Svc (M,A));

          then ex G be Covering of A, F st p = ( SUM ( vol (M,G))) by Def7;

          hence 0 <= p by Th4, MEASURE6: 2;

        end;

        then 0 is LowerBound of ( Svc (M,A)) by XXREAL_2:def 2;

        then 0 <= ( inf ( Svc (M,A))) by XXREAL_2:def 4;

        hence 0 <= r by A2, Def8;

      end;

      then for r be ExtReal holds r in ( rng ( C_Meas M)) implies 0 <= r;

      then ( rng ( C_Meas M)) is nonnegative;

      hence ( C_Meas M) is nonnegative;

    end;

    theorem :: MEASURE8:11

    

     Th11: (( C_Meas M) . {} ) = 0

    proof

      (( C_Meas M) . {} ) <= (M . {} ) by Th9, PROB_1: 4;

      then

       A1: (( C_Meas M) . {} ) <= 0 by VALUED_0:def 19;

      ( {} X) in ( bool X);

      then {} in ( dom ( C_Meas M)) by FUNCT_2:def 1;

      then

       A2: (( C_Meas M) . {} ) in ( rng ( C_Meas M)) by FUNCT_1: 3;

      ( C_Meas M) is nonnegative by Th10;

      then ( rng ( C_Meas M)) is nonnegative;

      hence (( C_Meas M) . {} ) = 0. by A1, A2;

    end;

    theorem :: MEASURE8:12

    

     Th12: A c= B implies (( C_Meas M) . A) <= (( C_Meas M) . B)

    proof

      assume

       A1: A c= B;

      now

        let r be object;

        assume r in ( Svc (M,B));

        then

        consider G be Covering of B, F such that

         A2: ( SUM ( vol (M,G))) = r by Def7;

        B c= ( union ( rng G)) by Def3;

        then A c= ( union ( rng G)) by A1;

        then

        reconsider G1 = G as Covering of A, F by Def3;

        ( SUM ( vol (M,G))) = ( SUM ( vol (M,G1)));

        hence r in ( Svc (M,A)) by A2, Def7;

      end;

      then

       A3: ( Svc (M,B)) c= ( Svc (M,A));

      (( C_Meas M) . A) = ( inf ( Svc (M,A))) & (( C_Meas M) . B) = ( inf ( Svc (M,B))) by Def8;

      hence (( C_Meas M) . A) <= (( C_Meas M) . B) by A3, XXREAL_2: 60;

    end;

    

     Lm2: (ex n be Nat st (( C_Meas M) . (Sets . n)) = +infty ) implies (( C_Meas M) . ( union ( rng Sets))) <= ( SUM (( C_Meas M) * Sets))

    proof

      assume ex n be Nat st (( C_Meas M) . (Sets . n)) = +infty ;

      then

      consider N be Nat such that

       A1: (( C_Meas M) . (Sets . N)) = +infty ;

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

      

       A2: (( C_Meas M) * Sets) is nonnegative by Th10, MEASURE1: 25;

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

      then ((( C_Meas M) * Sets) . N) = (( C_Meas M) . (Sets . N)) by FUNCT_1: 13;

      then ( SUM (( C_Meas M) * Sets)) = +infty by A1, A2, SUPINF_2: 45;

      hence (( C_Meas M) . ( union ( rng Sets))) <= ( SUM (( C_Meas M) * Sets)) by XXREAL_0: 3;

    end;

    theorem :: MEASURE8:13

    

     Th13: (( C_Meas M) . ( union ( rng Sets))) <= ( SUM (( C_Meas M) * Sets))

    proof

       A1:

      now

        assume

         A2: for n be Element of NAT holds ( Svc (M,(Sets . n))) <> { +infty };

        ( inf ( Svc (M,( union ( rng Sets))))) <= ( sup ( rng ( Ser (( C_Meas M) * Sets))))

        proof

          set y = ( inf ( Svc (M,( union ( rng Sets))))), x = ( sup ( rng ( Ser (( C_Meas M) * Sets))));

          

           A3: (( Ser (( C_Meas M) * Sets)) . 0 ) <= x by FUNCT_2: 4, XXREAL_2: 4;

          

           A4: (( C_Meas M) * Sets) is nonnegative by Th10, MEASURE1: 25;

          then 0 <= ((( C_Meas M) * Sets) . 0 ) by SUPINF_2: 39;

          then

           A5: 0 <= (( Ser (( C_Meas M) * Sets)) . 0 ) by SUPINF_2:def 11;

          assume not ( inf ( Svc (M,( union ( rng Sets))))) <= ( sup ( rng ( Ser (( C_Meas M) * Sets))));

          then

          consider eps be Real such that

           A6: 0 < eps and

           A7: (x + eps) < y by A5, A3, XXREAL_3: 49;

          consider E be sequence of ExtREAL such that

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

           A9: ( SUM E) < eps by A6, MEASURE6: 4;

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

          then

           A10: E is nonnegative by SUPINF_2: 39;

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

          

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

          proof

            let n be Element of NAT ;

            ( C_Meas M) is nonnegative & (( C_Meas M) . (Sets . n)) = ( inf ( Svc (M,(Sets . n)))) by Def8, Th10;

            then

             A12: 0 in REAL & 0. <= ( inf ( Svc (M,(Sets . n)))) by SUPINF_2: 51, XREAL_0:def 1;

            ( Svc (M,(Sets . n))) <> { +infty } by A2;

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

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

            then

            consider x be object such that

             A13: x in (( Svc (M,(Sets . n))) \ { +infty }) by XBOOLE_0:def 1;

            reconsider x as R_eal by A13;

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

            then

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

            x in ( Svc (M,(Sets . n))) by A13, XBOOLE_0:def 5;

            then ( inf ( Svc (M,(Sets . n)))) <= x by XXREAL_2: 3;

            then ( inf ( Svc (M,(Sets . n)))) < +infty by A14, XXREAL_0: 2, XXREAL_0: 4;

            then ( inf ( Svc (M,(Sets . n)))) is Element of REAL by A12, XXREAL_0: 46;

            then

            consider S1 be ExtReal such that

             A15: S1 in ( Svc (M,(Sets . n))) and

             A16: S1 < (( inf ( Svc (M,(Sets . n)))) + (E . n)) by A8, MEASURE6: 5;

            consider FS be Covering of (Sets . n), F such that

             A17: S1 = ( SUM ( vol (M,FS))) by A15, Def7;

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

            take FS;

            thus thesis by A16, A17;

          end;

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

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

          

           A19: for n be Nat holds (FF . n) is Covering of (Sets . n), F

          proof

            let n be Nat;

            n in NAT by ORDINAL1:def 12;

            then ex F0 be Covering of (Sets . n), F st F0 = (FF . n) & ( SUM ( vol (M,F0))) < (( inf ( Svc (M,(Sets . n)))) + (E . n)) by A18;

            hence thesis;

          end;

          deffunc F( Element of NAT ) = (((( C_Meas M) * Sets) . $1) + (E . $1));

          

           A20: for x be Element of NAT holds F(x) is Element of ExtREAL by XXREAL_0:def 1;

          consider G0 be sequence of ExtREAL such that

           A21: for n be Element of NAT holds (G0 . n) = F(n) from FUNCT_2:sch 9( A20);

          reconsider FF as Covering of Sets, F by A19, Def4;

          for n be Element of NAT holds (( Volume (M,FF)) . n) <= (G0 . n)

          proof

            let n be Element of NAT ;

            (ex F0 be Covering of (Sets . n), F st F0 = (FF . n) & ( SUM ( vol (M,F0))) < (( inf ( Svc (M,(Sets . n)))) + (E . n))) & ((( C_Meas M) * Sets) . n) = (( C_Meas M) . (Sets . n)) by A18, FUNCT_2: 15;

            then ( SUM ( vol (M,(FF . n)))) < (((( C_Meas M) * Sets) . n) + (E . n)) by Def8;

            then (( Volume (M,FF)) . n) < (((( C_Meas M) * Sets) . n) + (E . n)) by Def6;

            hence thesis by A21;

          end;

          then

           A22: ( SUM ( Volume (M,FF))) <= ( SUM G0) by SUPINF_2: 43;

           A23:

          now

            let n be Nat;

            n is Element of NAT by ORDINAL1:def 12;

            hence (G0 . n) = (((( C_Meas M) * Sets) . n) + (E . n)) by A21;

          end;

          (( SUM (( C_Meas M) * Sets)) + ( SUM E)) <= (( SUM (( C_Meas M) * Sets)) + eps) by A9, XXREAL_3: 36;

          then ( SUM G0) <= (( SUM (( C_Meas M) * Sets)) + eps) by A4, A10, A23, Th3;

          then

           A24: ( SUM ( Volume (M,FF))) <= (( SUM (( C_Meas M) * Sets)) + eps) by A22, XXREAL_0: 2;

          y <= ( SUM ( Volume (M,FF))) by Th7;

          hence thesis by A7, A24, XXREAL_0: 2;

        end;

        hence thesis by Def8;

      end;

      now

        assume ex n be Element of NAT st ( Svc (M,(Sets . n))) = { +infty };

        then

        consider n be Element of NAT such that

         A25: ( Svc (M,(Sets . n))) = { +infty };

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

        then (( C_Meas M) . (Sets . n)) = +infty by A25, Def8;

        hence thesis by Lm2;

      end;

      hence thesis by A1;

    end;

    theorem :: MEASURE8:14

    

     Th14: ( C_Meas M) is C_Measure of X

    proof

      (( C_Meas M) . {} ) = 0. by Th11;

      then

       A1: ( C_Meas M) is zeroed by VALUED_0:def 19;

      ( C_Meas M) is nonnegative & for A,B be Subset of X st A c= B holds (( C_Meas M) . A) <= (( C_Meas M) . B) & for F be sequence of ( bool X) holds (( C_Meas M) . ( union ( rng F))) <= ( SUM (( C_Meas M) * F)) by Th10, Th12, Th13;

      hence thesis by A1, MEASURE4:def 1;

    end;

    definition

      let X be set;

      let F be Field_Subset of X;

      let M be Measure of F;

      :: original: C_Meas

      redefine

      func C_Meas M -> C_Measure of X ;

      correctness by Th14;

    end

    begin

    definition

      let X be set;

      let F be Field_Subset of X;

      let M be Measure of F;

      :: MEASURE8:def11

      attr M is completely-additive means for FSets be Sep_Sequence of F st ( union ( rng FSets)) in F holds ( SUM (M * FSets)) = (M . ( union ( rng FSets)));

    end

    theorem :: MEASURE8:15

    

     Th15: ( Partial_Union FSets) is Set_Sequence of F

    proof

      defpred P[ Nat] means (( Partial_Union FSets) . $1) in F;

      

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

      proof

        let k be Nat;

        

         A2: (( Partial_Union FSets) . (k + 1)) = ((( Partial_Union FSets) . k) \/ (FSets . (k + 1))) by PROB_3:def 2;

        assume P[k];

        hence P[(k + 1)] by A2, PROB_1: 3;

      end;

      (( Partial_Union FSets) . 0 ) = (FSets . 0 ) by PROB_3:def 2;

      then

       A3: P[ 0 ];

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

      hence thesis by Def2;

    end;

    theorem :: MEASURE8:16

    

     Th16: ( Partial_Diff_Union FSets) is Set_Sequence of F

    proof

      defpred P[ Nat] means (( Partial_Diff_Union FSets) . $1) in F;

      

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

      proof

        let k be Nat;

        assume P[k];

        ( Partial_Union FSets) is Set_Sequence of F by Th15;

        then

         A2: (( Partial_Union FSets) . k) in F by Def2;

        (( Partial_Diff_Union FSets) . (k + 1)) = ((FSets . (k + 1)) \ (( Partial_Union FSets) . k)) by PROB_3:def 3;

        hence P[(k + 1)] by A2, PROB_1: 6;

      end;

      (( Partial_Diff_Union FSets) . 0 ) = (FSets . 0 ) by PROB_3:def 3;

      then

       A3: P[ 0 ];

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

      hence thesis by Def2;

    end;

    theorem :: MEASURE8:17

    

     Th17: A in F implies ex FSets be Sep_Sequence of F st A = ( union ( rng FSets)) & for n be Nat holds (FSets . n) c= (CA . n)

    proof

      deffunc F( Element of NAT ) = ((( Partial_Diff_Union CA) . $1) /\ A);

      consider FSets be sequence of ( bool X) such that

       A1: for n be Element of NAT holds (FSets . n) = F(n) from FUNCT_2:sch 4;

      reconsider FSets as SetSequence of X;

      assume

       A2: A in F;

      now

        let y be object;

        assume y in ( rng FSets);

        then

        consider x be object such that

         A3: x in NAT and

         A4: (FSets . x) = y by FUNCT_2: 11;

        reconsider n = x as Element of NAT by A3;

        

         A5: (FSets . n) = ((( Partial_Diff_Union CA) . n) /\ A) by A1;

        ( Partial_Diff_Union CA) is Set_Sequence of F by Th16;

        then (( Partial_Diff_Union CA) . n) in F by Def2;

        hence y in F by A2, A4, A5, FINSUB_1:def 2;

      end;

      then ( rng FSets) c= F;

      then

      reconsider FSets as sequence of F by FUNCT_2: 6;

      for m,n be Nat st m <> n holds (FSets . m) misses (FSets . n)

      proof

        let m,n be Nat;

        n in NAT by ORDINAL1:def 12;

        then (FSets . n) = ((( Partial_Diff_Union CA) . n) /\ A) by A1;

        then

         A6: (FSets . n) c= (( Partial_Diff_Union CA) . n) by XBOOLE_1: 17;

        m in NAT by ORDINAL1:def 12;

        then (FSets . m) = ((( Partial_Diff_Union CA) . m) /\ A) by A1;

        then

         A7: (FSets . m) c= (( Partial_Diff_Union CA) . m) by XBOOLE_1: 17;

        assume m <> n;

        then (( Partial_Diff_Union CA) . m) misses (( Partial_Diff_Union CA) . n) by PROB_3:def 4;

        hence thesis by A7, A6, XBOOLE_1: 64;

      end;

      then

      reconsider FSets as Sep_Sequence of F by PROB_3:def 4;

      now

        let x be object;

        assume

         A8: x in A;

        A c= ( union ( rng CA)) by Def3;

        then x in ( union ( rng CA)) by A8;

        then x in ( Union CA) by CARD_3:def 4;

        then x in ( Union ( Partial_Diff_Union CA)) by PROB_3: 20;

        then x in ( union ( rng ( Partial_Diff_Union CA))) by CARD_3:def 4;

        then

        consider E be set such that

         A9: x in E and

         A10: E in ( rng ( Partial_Diff_Union CA)) by TARSKI:def 4;

        consider n be object such that

         A11: n in NAT and

         A12: (( Partial_Diff_Union CA) . n) = E by A10, FUNCT_2: 11;

        reconsider n as Element of NAT by A11;

        x in ((( Partial_Diff_Union CA) . n) /\ A) by A8, A9, A12, XBOOLE_0:def 4;

        then

         A13: x in (FSets . n) by A1;

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

        hence x in ( union ( rng FSets)) by A13, TARSKI:def 4;

      end;

      then

       A14: A c= ( union ( rng FSets));

      take FSets;

      now

        let x be object;

        assume x in ( union ( rng FSets));

        then

        consider E be set such that

         A15: x in E and

         A16: E in ( rng FSets) by TARSKI:def 4;

        consider n be object such that

         A17: n in NAT and

         A18: (FSets . n) = E by A16, FUNCT_2: 11;

        reconsider n as Element of NAT by A17;

        x in ((( Partial_Diff_Union CA) . n) /\ A) by A1, A15, A18;

        hence x in A by XBOOLE_0:def 4;

      end;

      then ( union ( rng FSets)) c= A;

      hence A = ( union ( rng FSets)) by A14, XBOOLE_0:def 10;

      hereby

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        then (FSets . n) = ((( Partial_Diff_Union CA) . n) /\ A) by A1;

        then

         A19: (FSets . n) c= (( Partial_Diff_Union CA) . n) by XBOOLE_1: 17;

        (( Partial_Diff_Union CA) . n) c= (CA . n) by PROB_3: 17;

        hence (FSets . n) c= (CA . n) by A19;

      end;

    end;

    theorem :: MEASURE8:18

    

     Th18: M is completely-additive implies for A be set st A in F holds (M . A) = (( C_Meas M) . A)

    proof

      assume

       A1: M is completely-additive;

      let A be set;

      assume

       A2: A in F;

      then

      reconsider A9 = A as Subset of X;

      for x be ExtReal st x in ( Svc (M,A9)) holds (M . A) <= x

      proof

        let x be ExtReal;

        assume x in ( Svc (M,A9));

        then

        consider Aseq be Covering of A9, F such that

         A3: x = ( SUM ( vol (M,Aseq))) by Def7;

        consider Bseq be Sep_Sequence of F such that

         A4: A = ( union ( rng Bseq)) and

         A5: for n be Nat holds (Bseq . n) c= (Aseq . n) by A2, Th17;

        for n be Element of NAT holds ((M * Bseq) . n) <= (( vol (M,Aseq)) . n)

        proof

          let n be Element of NAT ;

          (M . (Bseq . n)) <= (M . (Aseq . n)) by A5, MEASURE1: 8;

          then ((M * Bseq) . n) <= (M . (Aseq . n)) by FUNCT_2: 15;

          hence thesis by Def5;

        end;

        then ( SUM (M * Bseq)) <= ( SUM ( vol (M,Aseq))) by SUPINF_2: 43;

        hence (M . A) <= x by A1, A2, A3, A4;

      end;

      then (M . A) is LowerBound of ( Svc (M,A9)) by XXREAL_2:def 2;

      then (M . A) <= ( inf ( Svc (M,A9))) by XXREAL_2:def 4;

      then

       A6: (M . A) <= (( C_Meas M) . A9) by Def8;

      (( C_Meas M) . A) <= (M . A) by A2, Th9;

      hence (M . A) = (( C_Meas M) . A) by A6, XXREAL_0: 1;

    end;

    reserve C for C_Measure of X;

    theorem :: MEASURE8:19

    

     Th19: (for B be Subset of X holds ((C . (B /\ A)) + (C . (B /\ (X \ A)))) <= (C . B)) implies A in ( sigma_Field C)

    proof

      assume

       A1: for B be Subset of X holds ((C . (B /\ A)) + (C . (B /\ (X \ A)))) <= (C . B);

      for W,Z be Subset of X holds (W c= A & Z c= (X \ A) implies ((C . W) + (C . Z)) <= (C . (W \/ Z)))

      proof

        let W,Z be Subset of X;

        assume that

         A2: W c= A and

         A3: Z c= (X \ A);

        set Y = (W \/ Z);

        

         A4: Z misses A by A3, XBOOLE_1: 106;

        

         A5: (Y /\ (X \ A)) = ((Y /\ X) \ A) by XBOOLE_1: 49

        .= (((X /\ W) \/ (X /\ Z)) \ A) by XBOOLE_1: 23

        .= ((W \/ (X /\ Z)) \ A) by XBOOLE_1: 28

        .= ((W \/ Z) \ A) by XBOOLE_1: 28

        .= ((W \ A) \/ (Z \ A)) by XBOOLE_1: 42

        .= ( {} \/ (Z \ A)) by A2, XBOOLE_1: 37

        .= ( {} \/ Z) by A4, XBOOLE_1: 83;

        (Y /\ A) = ((A /\ W) \/ (A /\ Z)) by XBOOLE_1: 23

        .= (W \/ (A /\ Z)) by A2, XBOOLE_1: 28

        .= (W \/ {} ) by A4, XBOOLE_0:def 7;

        hence thesis by A1, A5;

      end;

      hence A in ( sigma_Field C) by MEASURE4:def 2;

    end;

    theorem :: MEASURE8:20

    

     Th20: F c= ( sigma_Field ( C_Meas M))

    proof

      set C = ( C_Meas M);

      let E be object;

      assume

       A1: E in F;

      then

      reconsider E9 = E as Subset of X;

      for A be Subset of X holds ((C . (A /\ E9)) + (C . (A /\ (X \ E9)))) <= (C . A)

      proof

        let A be Subset of X;

        set CA = ((( C_Meas M) . (A /\ E9)) + (( C_Meas M) . (A /\ (X \ E9))));

        

         A2: for seq be Covering of A, F holds ((( C_Meas M) . (A /\ E9)) + (( C_Meas M) . (A /\ (X \ E9)))) <= ( SUM ( vol (M,seq)))

        proof

          let seq be Covering of A, F;

          deffunc F1( Element of NAT ) = ((seq . $1) /\ E9);

          consider Bseq be sequence of ( bool X) such that

           A3: for n be Element of NAT holds (Bseq . n) = F1(n) from FUNCT_2:sch 4;

          reconsider Bseq as SetSequence of X;

          for n be Nat holds (Bseq . n) in F

          proof

            let n be Nat;

            n in NAT by ORDINAL1:def 12;

            then (Bseq . n) = ((seq . n) /\ E9) by A3;

            hence (Bseq . n) in F by A1, FINSUB_1:def 2;

          end;

          then

          reconsider Bseq as Set_Sequence of F by Def2;

          

           A4: for x be set st x in A holds ex n be Element of NAT st x in (seq . n)

          proof

            let x be set;

            assume

             A5: x in A;

            A c= ( union ( rng seq)) by Def3;

            then

            consider B be set such that

             A6: x in B and

             A7: B in ( rng seq) by A5, TARSKI:def 4;

            ex n be Element of NAT st B = (seq . n) by A7, FUNCT_2: 113;

            hence thesis by A6;

          end;

          now

            let x be object;

            assume

             A8: x in (A /\ E9);

            then x in A by XBOOLE_0:def 4;

            then

            consider n be Element of NAT such that

             A9: x in (seq . n) by A4;

            x in E9 by A8, XBOOLE_0:def 4;

            then x in ((seq . n) /\ E9) by A9, XBOOLE_0:def 4;

            then

             A10: x in (Bseq . n) by A3;

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

            hence x in ( union ( rng Bseq)) by A10, TARSKI:def 4;

          end;

          then (A /\ E9) c= ( union ( rng Bseq));

          then

          reconsider Bseq as Covering of (A /\ E9), F by Def3;

          deffunc F2( Element of NAT ) = ((seq . $1) /\ (X \ E9));

          consider Cseq be sequence of ( bool X) such that

           A11: for n be Element of NAT holds (Cseq . n) = F2(n) from FUNCT_2:sch 4;

          reconsider Cseq as SetSequence of X;

          for n be Nat holds (Cseq . n) in F

          proof

            let n be Nat;

            X in F by PROB_1: 5;

            then

             A12: (X \ E9) in F by A1, PROB_1: 6;

            n in NAT by ORDINAL1:def 12;

            then (Cseq . n) = ((seq . n) /\ (X \ E9)) by A11;

            hence (Cseq . n) in F by A12, FINSUB_1:def 2;

          end;

          then

          reconsider Cseq as Set_Sequence of F by Def2;

          now

            let x be object;

            assume

             A13: x in (A /\ (X \ E9));

            then x in A by XBOOLE_0:def 4;

            then

            consider n be Element of NAT such that

             A14: x in (seq . n) by A4;

            x in (X \ E9) by A13, XBOOLE_0:def 4;

            then x in ((seq . n) /\ (X \ E9)) by A14, XBOOLE_0:def 4;

            then

             A15: x in (Cseq . n) by A11;

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

            hence x in ( union ( rng Cseq)) by A15, TARSKI:def 4;

          end;

          then (A /\ (X \ E9)) c= ( union ( rng Cseq));

          then

          reconsider Cseq as Covering of (A /\ (X \ E9)), F by Def3;

          

           A16: for n be Nat holds (( vol (M,seq)) . n) = ((( vol (M,Bseq)) . n) + (( vol (M,Cseq)) . n))

          proof

            let n be Nat;

            

             A17: (M . (seq . n)) = (( vol (M,seq)) . n) & (M . (Bseq . n)) = (( vol (M,Bseq)) . n) by Def5;

            

             A18: (M . (Cseq . n)) = (( vol (M,Cseq)) . n) by Def5;

            n is Element of NAT by ORDINAL1:def 12;

            then

             A19: (Bseq . n) = ((seq . n) /\ E9) & (Cseq . n) = ((seq . n) /\ (X \ E9)) by A3, A11;

            then ((Bseq . n) \/ (Cseq . n)) = ((seq . n) /\ (E9 \/ (X \ E9))) by XBOOLE_1: 23;

            then ((Bseq . n) \/ (Cseq . n)) = ((seq . n) /\ (E9 \/ X)) by XBOOLE_1: 39;

            then ((Bseq . n) \/ (Cseq . n)) = ((seq . n) /\ X) by XBOOLE_1: 12;

            then

             A20: ((Bseq . n) \/ (Cseq . n)) = (seq . n) by XBOOLE_1: 28;

            (Bseq . n) misses (Cseq . n) by A19, XBOOLE_1: 76, XBOOLE_1: 79;

            hence (( vol (M,seq)) . n) = ((( vol (M,Bseq)) . n) + (( vol (M,Cseq)) . n)) by A20, A17, A18, MEASURE1:def 3;

          end;

          (( C_Meas M) . (A /\ (X \ E9))) = ( inf ( Svc (M,(A /\ (X \ E9))))) & ( SUM ( vol (M,Cseq))) in ( Svc (M,(A /\ (X \ E9)))) by Def7, Def8;

          then

           A21: (( C_Meas M) . (A /\ (X \ E9))) <= ( SUM ( vol (M,Cseq))) by XXREAL_2: 3;

          (( C_Meas M) . (A /\ E9)) = ( inf ( Svc (M,(A /\ E9)))) & ( SUM ( vol (M,Bseq))) in ( Svc (M,(A /\ E9))) by Def7, Def8;

          then

           A22: (( C_Meas M) . (A /\ E9)) <= ( SUM ( vol (M,Bseq))) by XXREAL_2: 3;

          ( vol (M,Bseq)) is nonnegative & ( vol (M,Cseq)) is nonnegative by Th4;

          then ( SUM ( vol (M,seq))) = (( SUM ( vol (M,Bseq))) + ( SUM ( vol (M,Cseq)))) by A16, Th3;

          hence ((( C_Meas M) . (A /\ E9)) + (( C_Meas M) . (A /\ (X \ E9)))) <= ( SUM ( vol (M,seq))) by A22, A21, XXREAL_3: 36;

        end;

        for r be ExtReal holds r in ( Svc (M,A)) implies CA <= r

        proof

          let r be ExtReal;

          assume r in ( Svc (M,A));

          then ex G be Covering of A, F st r = ( SUM ( vol (M,G))) by Def7;

          hence thesis by A2;

        end;

        then CA is LowerBound of ( Svc (M,A)) by XXREAL_2:def 2;

        then CA <= ( inf ( Svc (M,A))) by XXREAL_2:def 4;

        hence CA <= (( C_Meas M) . A) by Def8;

      end;

      hence E in ( sigma_Field ( C_Meas M)) by Th19;

    end;

    theorem :: MEASURE8:21

    

     Th21: for X be set, F be Field_Subset of X, FSets be Set_Sequence of F, M be Function of F, ExtREAL holds (M * FSets) is ExtREAL_sequence

    proof

      let X be set;

      let F be Field_Subset of X;

      let FSets be Set_Sequence of F;

      let M be Function of F, ExtREAL ;

      now

        let y be object;

        assume y in ( rng FSets);

        then ex x be object st x in NAT & (FSets . x) = y by FUNCT_2: 11;

        hence y in F by Def2;

      end;

      then ( rng FSets) c= F;

      then ( rng FSets) c= ( dom M) by FUNCT_2:def 1;

      then ( dom (M * FSets)) = ( dom FSets) by RELAT_1: 27;

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

      hence thesis by FUNCT_2:def 1;

    end;

    definition

      let X be set;

      let F be Field_Subset of X;

      let FSets be Set_Sequence of F;

      let g be Function of F, ExtREAL ;

      :: original: *

      redefine

      func g * FSets -> ExtREAL_sequence ;

      correctness by Th21;

    end

    theorem :: MEASURE8:22

    

     Th22: for X be set, S be SigmaField of X, SSets be SetSequence of S, M be Function of S, ExtREAL holds (M * SSets) is ExtREAL_sequence

    proof

      let X be set;

      let S be SigmaField of X;

      let SSets be SetSequence of S;

      let M be Function of S, ExtREAL ;

      ( rng SSets) c= S;

      then ( rng SSets) c= ( dom M) by FUNCT_2:def 1;

      then ( dom (M * SSets)) = ( dom SSets) by RELAT_1: 27;

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

      hence thesis by FUNCT_2:def 1;

    end;

    definition

      let X be set;

      let S be SigmaField of X;

      let SSets be SetSequence of S;

      let g be Function of S, ExtREAL ;

      :: original: *

      redefine

      func g * SSets -> ExtREAL_sequence ;

      correctness by Th22;

    end

    theorem :: MEASURE8:23

    

     Th23: for F,G be sequence of ExtREAL , n be Nat st (for m be Nat st m <= n holds (F . m) <= (G . m)) holds (( Ser F) . n) <= (( Ser G) . n)

    proof

      let F,G be sequence of ExtREAL ;

      let n be Nat;

      assume

       A1: for m be Nat st m <= n holds (F . m) <= (G . m);

      defpred P[ Nat] means (for m be Nat st m <= $1 holds (F . m) <= (G . m)) implies (( Ser F) . $1) <= (( Ser G) . $1);

      

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

      proof

        let k be Nat;

        assume

         A3: P[k];

        now

          assume

           A4: for m be Nat st m <= (k + 1) holds (F . m) <= (G . m);

           A5:

          now

            let m be Nat;

            assume m <= k;

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

            hence (F . m) <= (G . m) by A4;

          end;

          (F . (k + 1)) <= (G . (k + 1)) by A4;

          then ((( Ser F) . k) + (F . (k + 1))) <= ((( Ser G) . k) + (G . (k + 1))) by A3, A5, XXREAL_3: 36;

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

          hence (( Ser F) . (k + 1)) <= (( Ser G) . (k + 1)) by SUPINF_2:def 11;

        end;

        hence P[(k + 1)];

      end;

      now

        

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

        assume for m be Nat st m <= 0 holds (F . m) <= (G . m);

        hence (( Ser F) . 0 ) <= (( Ser G) . 0 ) by A6;

      end;

      then

       A7: P[ 0 ];

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

      hence thesis by A1;

    end;

    theorem :: MEASURE8:24

    

     Th24: for X, C holds for seq be Sep_Sequence of ( sigma_Field C) holds ( union ( rng seq)) in ( sigma_Field C) & (C . ( union ( rng seq))) = ( Sum (C * seq))

    proof

      let X, C;

      let seq be Sep_Sequence of ( sigma_Field C);

      

       A1: ( rng seq) c= ( sigma_Field C) by RELAT_1:def 19;

      then

      reconsider seq1 = seq as sequence of ( bool X) by FUNCT_2: 6;

      

       A2: for A be Subset of X, n be Element of NAT holds ((( Ser (C * (A (/\) seq1))) . n) + (C . (A /\ (X \ ( union ( rng seq)))))) <= (C . A)

      proof

        defpred P[ Nat] means for A be Subset of X holds (C . A) >= ((( Ser (C * (A (/\) seq1))) . $1) + (C . (A /\ (X \ ( union ( rng seq))))));

        let A be Subset of X, n be Element of NAT ;

        

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

        proof

          let k be Nat;

          assume

           A4: P[k];

           A5:

          now

            let A be Subset of X;

            

             A6: (C . (A /\ (X \ (seq1 . (k + 1))))) >= ((( Ser (C * ((A /\ (X \ (seq1 . (k + 1)))) (/\) seq1))) . k) + (C . ((A /\ (X \ (seq1 . (k + 1)))) /\ (X \ ( union ( rng seq)))))) by A4;

            for m be Nat st m <= k holds ((C * (A (/\) seq1)) . m) <= ((C * ((A /\ (X \ (seq1 . (k + 1)))) (/\) seq1)) . m)

            proof

              let m be Nat;

              reconsider m1 = m as Element of NAT by ORDINAL1:def 12;

              assume m <= k;

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

              then (seq1 . m) misses (seq1 . (k + 1)) by PROB_2:def 2;

              then

               A7: ((seq1 . m) /\ (X \ (seq1 . (k + 1)))) = (seq1 . m) by XBOOLE_1: 28, XBOOLE_1: 86;

              (((A /\ (X \ (seq1 . (k + 1)))) (/\) seq1) . m) = ((A /\ (X \ (seq1 . (k + 1)))) /\ (seq1 . m1)) by SETLIM_2:def 5

              .= (A /\ ((seq1 . m) /\ (X \ (seq1 . (k + 1))))) by XBOOLE_1: 16;

              then (((A /\ (X \ (seq1 . (k + 1)))) (/\) seq1) . m) = ((A (/\) seq1) . m1) by A7, SETLIM_2:def 5;

              then ((C * ((A /\ (X \ (seq1 . (k + 1)))) (/\) seq1)) . m1) = (C . ((A (/\) seq1) . m1)) by FUNCT_2: 15;

              hence thesis by FUNCT_2: 15;

            end;

            then

             A8: (( Ser (C * (A (/\) seq1))) . k) <= (( Ser (C * ((A /\ (X \ (seq1 . (k + 1)))) (/\) seq1))) . k) by Th23;

            (seq1 . (k + 1)) c= ( union ( rng seq)) by FUNCT_2: 4, ZFMISC_1: 74;

            then ((X \ (seq1 . (k + 1))) /\ (X \ ( union ( rng seq)))) = (X \ ( union ( rng seq))) by XBOOLE_1: 28, XBOOLE_1: 34;

            then ((A /\ (X \ (seq1 . (k + 1)))) /\ (X \ ( union ( rng seq)))) = (A /\ (X \ ( union ( rng seq)))) by XBOOLE_1: 16;

            then ((( Ser (C * ((A /\ (X \ (seq1 . (k + 1)))) (/\) seq1))) . k) + (C . ((A /\ (X \ (seq1 . (k + 1)))) /\ (X \ ( union ( rng seq)))))) >= ((( Ser (C * (A (/\) seq1))) . k) + (C . (A /\ (X \ ( union ( rng seq)))))) by A8, XXREAL_3: 36;

            hence (C . (A /\ (X \ (seq1 . (k + 1))))) >= ((( Ser (C * (A (/\) seq1))) . k) + (C . (A /\ (X \ ( union ( rng seq)))))) by A6, XXREAL_0: 2;

          end;

          let A be Subset of X;

          (A /\ (X \ (seq1 . (k + 1)))) = ((A /\ X) \ (seq1 . (k + 1))) by XBOOLE_1: 49

          .= (A \ (seq1 . (k + 1))) by XBOOLE_1: 28;

          then

           A9: (C . (A \ (seq1 . (k + 1)))) >= ((( Ser (C * (A (/\) seq1))) . k) + (C . (A /\ (X \ ( union ( rng seq)))))) by A5;

          

           A10: (A \ (seq1 . (k + 1))) c= (X \ (seq1 . (k + 1))) by XBOOLE_1: 33;

          

           A11: (A \/ (A \ (seq1 . (k + 1)))) = A by XBOOLE_1: 12, XBOOLE_1: 36;

          (seq1 . (k + 1)) in ( rng seq) & (A /\ (seq1 . (k + 1))) c= (seq1 . (k + 1)) by FUNCT_2: 4, XBOOLE_1: 17;

          

          then ((C . (A /\ (seq1 . (k + 1)))) + (C . (A \ (seq1 . (k + 1))))) = (C . ((A /\ (seq1 . (k + 1))) \/ (A \ (seq1 . (k + 1))))) by A1, A10, MEASURE4: 5

          .= (C . ((A \/ (A \ (seq1 . (k + 1)))) /\ ((seq1 . (k + 1)) \/ (A \ (seq1 . (k + 1)))))) by XBOOLE_1: 24

          .= (C . ((A \/ (A \ (seq1 . (k + 1)))) /\ ((seq1 . (k + 1)) \/ A))) by XBOOLE_1: 39;

          then ((C . (A /\ (seq1 . (k + 1)))) + (C . (A \ (seq1 . (k + 1))))) = (C . A) by A11, XBOOLE_1: 7, XBOOLE_1: 28;

          then

           A12: (C . A) >= (((( Ser (C * (A (/\) seq1))) . k) + (C . (A /\ (X \ ( union ( rng seq)))))) + (C . (A /\ (seq1 . (k + 1))))) by A9, XXREAL_3: 36;

          

           A13: ((( Ser (C * (A (/\) seq1))) . k) + (C . (A /\ (seq1 . (k + 1))))) = ((( Ser (C * (A (/\) seq1))) . k) + (C . ((A (/\) seq1) . (k + 1)))) by SETLIM_2:def 5

          .= ((( Ser (C * (A (/\) seq1))) . k) + ((C * (A (/\) seq1)) . (k + 1))) by FUNCT_2: 15

          .= (( Ser (C * (A (/\) seq1))) . (k + 1)) by SUPINF_2:def 11;

          

           A14: C is nonnegative by MEASURE4:def 1;

          then

           A15: (C * (A (/\) seq1)) is nonnegative by MEASURE1: 25;

          then ((C * (A (/\) seq1)) . k) >= 0 by SUPINF_2: 51;

          then

           A16: (( Ser (C * (A (/\) seq1))) . k) > -infty by A15, MEASURE7: 2;

          (C . (A /\ (X \ ( union ( rng seq))))) > -infty & (C . (A /\ (seq1 . (k + 1)))) > -infty by A14, SUPINF_2: 51;

          hence (C . A) >= ((( Ser (C * (A (/\) seq1))) . (k + 1)) + (C . (A /\ (X \ ( union ( rng seq)))))) by A16, A12, A13, XXREAL_3: 29;

        end;

        

         A17: (seq . 0 ) in ( sigma_Field C);

        now

          let A be Subset of X;

          (A /\ (seq1 . 0 )) c= (seq1 . 0 ) & (A /\ (X \ (seq1 . 0 ))) c= (X \ (seq1 . 0 )) by XBOOLE_1: 17;

          

          then

           A18: ((C . (A /\ (seq1 . 0 ))) + (C . (A /\ (X \ (seq1 . 0 ))))) = (C . ((A /\ (seq1 . 0 )) \/ (A /\ (X \ (seq1 . 0 ))))) by A17, MEASURE4: 5

          .= (C . ((A /\ (seq1 . 0 )) \/ ((A /\ X) \ (seq1 . 0 )))) by XBOOLE_1: 49

          .= (C . ((A /\ (seq1 . 0 )) \/ (A \ (seq1 . 0 )))) by XBOOLE_1: 28

          .= (C . A) by XBOOLE_1: 51;

          (seq1 . 0 ) c= ( Union seq1) by ABCMIZ_1: 1;

          then (seq . 0 ) c= ( union ( rng seq)) by CARD_3:def 4;

          then (X \ ( union ( rng seq))) c= (X \ (seq . 0 )) by XBOOLE_1: 34;

          then (A /\ (X \ ( union ( rng seq)))) c= (A /\ (X \ (seq . 0 ))) by XBOOLE_1: 26;

          then

           A19: (C . (A /\ (X \ ( union ( rng seq))))) <= (C . (A /\ (X \ (seq . 0 )))) by MEASURE4:def 1;

          (( Ser (C * (A (/\) seq1))) . 0 ) = ((C * (A (/\) seq1)) . 0 ) by SUPINF_2:def 11

          .= (C . ((A (/\) seq1) . 0 )) by FUNCT_2: 15

          .= (C . (A /\ (seq1 . 0 ))) by SETLIM_2:def 5;

          hence (C . A) >= ((( Ser (C * (A (/\) seq1))) . 0 ) + (C . (A /\ (X \ ( union ( rng seq)))))) by A18, A19, XXREAL_3: 36;

        end;

        then

         A20: P[ 0 ];

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

        hence thesis;

      end;

      

       A21: for A be Subset of X holds (( SUM (C * (A (/\) seq1))) + (C . (A /\ (X \ ( union ( rng seq)))))) <= (C . A) & (C . (A /\ ( Union seq1))) <= ( SUM (C * (A (/\) seq1)))

      proof

        let A be Subset of X;

        

         A22: C is nonnegative by MEASURE4:def 1;

        then

         A23: (C * (A (/\) seq1)) is nonnegative by MEASURE1: 25;

        

         A24: (C . (A /\ (X \ ( union ( rng seq))))) > -infty by A22, SUPINF_2: 51;

         not ((C . A) = +infty & (C . (A /\ (X \ ( union ( rng seq))))) = +infty ) implies (( SUM (C * (A (/\) seq1))) + (C . (A /\ (X \ ( union ( rng seq)))))) <= (C . A)

        proof

          assume

           A25: not ((C . A) = +infty & (C . (A /\ (X \ ( union ( rng seq))))) = +infty );

          for x be ExtReal holds x in ( rng ( Ser (C * (A (/\) seq1)))) implies x <= ((C . A) - (C . (A /\ (X \ ( union ( rng seq))))))

          proof

            let x be ExtReal;

            assume x in ( rng ( Ser (C * (A (/\) seq1))));

            then

            consider i be object such that

             A26: i in NAT and

             A27: (( Ser (C * (A (/\) seq1))) . i) = x by FUNCT_2: 11;

            reconsider i as Element of NAT by A26;

            ((C * (A (/\) seq1)) . i) >= 0 by A23, SUPINF_2: 51;

            then

             A28: x > -infty by A23, A27, MEASURE7: 2;

            (C . (A /\ (X \ ( union ( rng seq))))) > -infty & ((( Ser (C * (A (/\) seq1))) . i) + (C . (A /\ (X \ ( union ( rng seq)))))) <= (C . A) by A2, A22, SUPINF_2: 51;

            hence x <= ((C . A) - (C . (A /\ (X \ ( union ( rng seq)))))) by A25, A27, A28, XXREAL_3: 56;

          end;

          then ((C . A) - (C . (A /\ (X \ ( union ( rng seq)))))) is UpperBound of ( rng ( Ser (C * (A (/\) seq1)))) by XXREAL_2:def 1;

          then

           A29: ( SUM (C * (A (/\) seq1))) <= ((C . A) - (C . (A /\ (X \ ( union ( rng seq)))))) by XXREAL_2:def 3;

          ( SUM (C * (A (/\) seq1))) >= 0 by A23, MEASURE6: 2;

          hence (( SUM (C * (A (/\) seq1))) + (C . (A /\ (X \ ( union ( rng seq)))))) <= (C . A) by A24, A29, XXREAL_3: 55;

        end;

        hence (( SUM (C * (A (/\) seq1))) + (C . (A /\ (X \ ( union ( rng seq)))))) <= (C . A) by XXREAL_0: 3;

        (C . ( union ( rng (A (/\) seq1)))) <= ( SUM (C * (A (/\) seq1))) by MEASURE4:def 1;

        then (C . ( Union (A (/\) seq1))) <= ( SUM (C * (A (/\) seq1))) by CARD_3:def 4;

        hence (C . (A /\ ( Union seq1))) <= ( SUM (C * (A (/\) seq1))) by SETLIM_2: 38;

      end;

      then

       A30: (C . (( union ( rng seq)) /\ ( Union seq1))) <= ( SUM (C * (( union ( rng seq)) (/\) seq1)));

      for W,Z be Subset of X holds (W c= ( Union seq1) & Z c= (X \ ( Union seq1)) implies ((C . W) + (C . Z)) <= (C . (W \/ Z)))

      proof

        let W,Z be Subset of X;

        assume that

         A31: W c= ( Union seq1) and

         A32: Z c= (X \ ( Union seq1));

        set A = (W \/ Z);

        

         A33: (A /\ (X \ ( Union seq1))) = (Z \/ (W /\ (X \ ( Union seq1)))) by A32, XBOOLE_1: 30;

        (X \ ( Union seq1)) misses ( Union seq1) by XBOOLE_1: 79;

        then

         A34: ((X \ ( Union seq1)) /\ ( Union seq1)) = {} by XBOOLE_0:def 7;

        (W /\ (X \ ( Union seq1))) c= (( Union seq1) /\ (X \ ( Union seq1))) by A31, XBOOLE_1: 26;

        then (W /\ (X \ ( Union seq1))) = {} by A34;

        then

         A35: (C . Z) = (C . (A /\ (X \ ( union ( rng seq))))) by A33, CARD_3:def 4;

        (Z /\ ( Union seq1)) c= ((X \ ( Union seq1)) /\ ( Union seq1)) by A32, XBOOLE_1: 26;

        then

         A36: (Z /\ ( Union seq1)) = {} by A34;

        (A /\ ( Union seq1)) = (W \/ (Z /\ ( Union seq1))) by A31, XBOOLE_1: 30;

        then (C . W) <= ( SUM (C * (A (/\) seq1))) by A21, A36;

        then

         A37: ((C . W) + (C . Z)) <= (( SUM (C * (A (/\) seq1))) + (C . (A /\ (X \ ( union ( rng seq)))))) by A35, XXREAL_3: 36;

        (( SUM (C * (A (/\) seq1))) + (C . (A /\ (X \ ( union ( rng seq)))))) <= (C . A) by A21;

        hence ((C . W) + (C . Z)) <= (C . (W \/ Z)) by A37, XXREAL_0: 2;

      end;

      then ( Union seq1) in ( sigma_Field C) by MEASURE4:def 2;

      hence ( union ( rng seq)) in ( sigma_Field C) by CARD_3:def 4;

      set Sseq = ( Ser (C * seq1));

      ( union ( rng seq)) misses (X \ ( union ( rng seq))) by XBOOLE_1: 79;

      then

       A38: (( union ( rng seq)) /\ (X \ ( union ( rng seq)))) = {} by XBOOLE_0:def 7;

      C is zeroed by MEASURE4:def 1;

      then

       A39: (C . (( union ( rng seq)) /\ (X \ ( union ( rng seq))))) = 0 by A38, VALUED_0:def 19;

      for n be object st n in NAT holds ((( union ( rng seq)) (/\) seq1) . n) = (seq . n)

      proof

        let n be object;

        assume n in NAT ;

        then

        reconsider n1 = n as Element of NAT ;

        (seq1 . n1) c= ( union ( rng seq)) by FUNCT_2: 4, ZFMISC_1: 74;

        then (( union ( rng seq)) /\ (seq1 . n1)) = (seq . n) by XBOOLE_1: 28;

        hence thesis by SETLIM_2:def 5;

      end;

      then

       A40: ( SUM (C * (( union ( rng seq)) (/\) seq1))) = ( sup ( Ser (C * seq1))) by FUNCT_2: 12;

      C is nonnegative by MEASURE4:def 1;

      then (C * seq1) is nonnegative by MEASURE1: 25;

      then for m,n be ExtReal st m in ( dom Sseq) & n in ( dom Sseq) & m <= n holds (Sseq . m) <= (Sseq . n) by MEASURE7: 8;

      then Sseq is non-decreasing by VALUED_0:def 15;

      then ( SUM (C * (( union ( rng seq)) (/\) seq1))) = ( lim ( Ser (C * seq1))) by A40, RINFSUP2: 37;

      then

       A41: ( SUM (C * (( union ( rng seq)) (/\) seq1))) = ( lim ( Partial_Sums (C * seq1))) by Th1;

      (( SUM (C * (( union ( rng seq)) (/\) seq1))) + (C . (( union ( rng seq)) /\ (X \ ( union ( rng seq)))))) <= (C . ( union ( rng seq))) by A21;

      then ( union ( rng seq)) = ( Union seq1) & (C . ( union ( rng seq))) >= ( Sum (C * seq)) by A39, A41, CARD_3:def 4, XXREAL_3: 4;

      hence (C . ( union ( rng seq))) = ( Sum (C * seq)) by A30, A41, XXREAL_0: 1;

    end;

    theorem :: MEASURE8:25

    for X, C holds for seq be SetSequence of ( sigma_Field C) holds ( Union seq) in ( sigma_Field C)

    proof

      let X, C;

      let seq be SetSequence of ( sigma_Field C);

      set Aseq = ( Partial_Diff_Union seq);

      ( rng Aseq) c= ( sigma_Field C) by RELAT_1:def 19;

      then

      reconsider Aseq9 = Aseq as sequence of ( sigma_Field C) by FUNCT_2: 6;

      reconsider Aseq9 as Sep_Sequence of ( sigma_Field C);

      ( union ( rng Aseq9)) in ( sigma_Field C) by Th24;

      then ( Union Aseq) in ( sigma_Field C) by CARD_3:def 4;

      hence ( Union seq) in ( sigma_Field C) by PROB_3: 36;

    end;

    theorem :: MEASURE8:26

    

     Th26: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, SSets be SetSequence of S st SSets is non-descending holds ( lim (M * SSets)) = (M . ( lim SSets))

    proof

      let X be non empty set;

      let S be SigmaField of X;

      let M be sigma_Measure of S;

      let SSets be SetSequence of S;

      assume

       A1: SSets is non-descending;

      then

       A2: ( Partial_Union SSets) = SSets by PROB_4: 19;

      ( rng ( Partial_Diff_Union SSets)) c= S;

      then

      reconsider Bseq = ( Partial_Diff_Union SSets) as Sep_Sequence of S by FUNCT_2: 6;

      for n be object st n in NAT holds (( Ser (M * Bseq)) . n) = ((M * ( Partial_Union SSets)) . n)

      proof

        defpred P[ Nat] means (( Ser (M * Bseq)) . $1) = ((M * ( Partial_Union SSets)) . $1);

        let n be object;

        

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

        proof

          let k be Nat;

          assume

           A4: P[k];

          

           A5: (( Partial_Union ( Partial_Diff_Union SSets)) . k) = (( Partial_Union SSets) . k) & (( Partial_Diff_Union SSets) . (k + 1)) = ((SSets . (k + 1)) \ (( Partial_Union SSets) . k)) by PROB_3: 35, PROB_3:def 3;

          

           A6: k in NAT by ORDINAL1:def 12;

          (( Ser (M * Bseq)) . (k + 1)) = ((( Ser (M * Bseq)) . k) + ((M * Bseq) . (k + 1))) by SUPINF_2:def 11

          .= (((M * ( Partial_Union SSets)) . k) + (M . (( Partial_Diff_Union SSets) . (k + 1)))) by A4, FUNCT_2: 15

          .= ((M . (( Partial_Union SSets) . k)) + (M . (( Partial_Diff_Union SSets) . (k + 1)))) by FUNCT_2: 15, A6

          .= ((M . (( Partial_Union ( Partial_Diff_Union SSets)) . k)) + (M . (( Partial_Diff_Union SSets) . (k + 1)))) by PROB_3: 35;

          

          then (( Ser (M * Bseq)) . (k + 1)) = (M . ((( Partial_Union ( Partial_Diff_Union SSets)) . k) \/ (( Partial_Diff_Union SSets) . (k + 1)))) by A5, MEASURE1: 30, XBOOLE_1: 79

          .= (M . (( Partial_Union ( Partial_Diff_Union SSets)) . (k + 1))) by PROB_3:def 2

          .= (M . (( Partial_Union SSets) . (k + 1))) by PROB_3: 35;

          hence (( Ser (M * Bseq)) . (k + 1)) = ((M * ( Partial_Union SSets)) . (k + 1)) by FUNCT_2: 15;

        end;

        assume n in NAT ;

        then

        reconsider n1 = n as Element of NAT ;

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

        .= (M . (( Partial_Diff_Union SSets) . 0 )) by FUNCT_2: 15

        .= (M . (SSets . 0 )) by PROB_3: 31

        .= (M . (( Partial_Union SSets) . 0 )) by PROB_3: 22;

        then

         A7: P[ 0 ] by FUNCT_2: 15;

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

        then (( Ser (M * Bseq)) . n1) = ((M * ( Partial_Union SSets)) . n1);

        hence thesis;

      end;

      then

       A8: ( Ser (M * Bseq)) = (M * SSets) by A2, FUNCT_2: 12;

      reconsider Gseq = ( Ser (M * Bseq)) as ExtREAL_sequence;

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

      then for m,n be ExtReal st m in ( dom Gseq) & n in ( dom Gseq) & m <= n holds (Gseq . m) <= (Gseq . n) by MEASURE7: 8;

      then Gseq is non-decreasing by VALUED_0:def 15;

      then

       A9: ( SUM (M * Bseq)) = (M . ( union ( rng Bseq))) & ( lim Gseq) = ( sup Gseq) by MEASURE1:def 6, RINFSUP2: 37;

      ( Partial_Union ( Partial_Diff_Union SSets)) = SSets by A2, PROB_3: 35;

      then ( Union SSets) = ( Union ( Partial_Diff_Union SSets)) by PROB_3: 30;

      then ( lim Gseq) = (M . ( Union SSets)) by A9, CARD_3:def 4;

      hence thesis by A1, A8, SETLIM_1: 63;

    end;

    theorem :: MEASURE8:27

    FSets is non-descending implies (M * FSets) is non-decreasing

    proof

      

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

      assume

       A2: FSets is non-descending;

      now

        let n,m be Nat;

        

         A3: n in NAT & m in NAT by ORDINAL1:def 12;

        assume n <= m;

        then

         A4: (FSets . n) c= (FSets . m) by A2, PROB_1:def 5;

        ((M * FSets) . n) = (M . (FSets . n)) & ((M * FSets) . m) = (M . (FSets . m)) by A1, FUNCT_1: 12, A3;

        hence ((M * FSets) . n) <= ((M * FSets) . m) by A4, MEASURE1: 8;

      end;

      then for n,m be Nat st m <= n holds ((M * FSets) . m) <= ((M * FSets) . n);

      hence (M * FSets) is non-decreasing by RINFSUP2: 7;

    end;

    theorem :: MEASURE8:28

    FSets is non-ascending implies (M * FSets) is non-increasing

    proof

      

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

      assume

       A2: FSets is non-ascending;

      now

        let n,m be Nat;

        

         A3: n in NAT & m in NAT by ORDINAL1:def 12;

        assume m <= n;

        then

         A4: (FSets . n) c= (FSets . m) by A2, PROB_1:def 4;

        ((M * FSets) . n) = (M . (FSets . n)) & ((M * FSets) . m) = (M . (FSets . m)) by A1, FUNCT_1: 12, A3;

        hence ((M * FSets) . n) <= ((M * FSets) . m) by A4, MEASURE1: 8;

      end;

      hence (M * FSets) is non-increasing by RINFSUP2: 7;

    end;

    theorem :: MEASURE8:29

    

     Th29: for X be set, S be SigmaField of X, M be sigma_Measure of S, SSets be SetSequence of S st SSets is non-descending holds (M * SSets) is non-decreasing

    proof

      let X be set;

      let S be SigmaField of X;

      let M be sigma_Measure of S;

      let SSets be SetSequence of S;

      

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

      assume

       A2: SSets is non-descending;

      now

        let n,m be Nat;

        

         A3: n in NAT & m in NAT by ORDINAL1:def 12;

        

         A4: ((M * SSets) . m) = (M . (SSets . m)) by A1, FUNCT_1: 12, A3;

        assume n <= m;

        then

         A5: (SSets . n) c= (SSets . m) by A2, PROB_1:def 5;

        ( rng SSets) c= S & ((M * SSets) . n) = (M . (SSets . n)) by A1, FUNCT_1: 12, A3;

        hence ((M * SSets) . n) <= ((M * SSets) . m) by A5, A4, MEASURE1: 31;

      end;

      then for n,m be Nat st m <= n holds ((M * SSets) . m) <= ((M * SSets) . n);

      hence (M * SSets) is non-decreasing by RINFSUP2: 7;

    end;

    theorem :: MEASURE8:30

    

     Th30: for X be set, S be SigmaField of X, M be sigma_Measure of S, SSets be SetSequence of S st SSets is non-ascending holds (M * SSets) is non-increasing

    proof

      let X be set;

      let S be SigmaField of X;

      let M be sigma_Measure of S;

      let SSets be SetSequence of S;

      

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

      assume

       A2: SSets is non-ascending;

      now

        let n,m be Nat;

        

         A3: n in NAT & m in NAT by ORDINAL1:def 12;

        

         A4: ((M * SSets) . m) = (M . (SSets . m)) by A1, FUNCT_1: 12, A3;

        assume m <= n;

        then

         A5: (SSets . n) c= (SSets . m) by A2, PROB_1:def 4;

        ( rng SSets) c= S & ((M * SSets) . n) = (M . (SSets . n)) by A1, FUNCT_1: 12, A3;

        hence ((M * SSets) . n) <= ((M * SSets) . m) by A5, A4, MEASURE1: 31;

      end;

      hence (M * SSets) is non-increasing by RINFSUP2: 7;

    end;

    theorem :: MEASURE8:31

    for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, SSets be SetSequence of S st SSets is non-ascending & (M . (SSets . 0 )) < +infty holds ( lim (M * SSets)) = (M . ( lim SSets))

    proof

      let X be non empty set;

      let S be SigmaField of X;

      let M be sigma_Measure of S;

      let SSets be SetSequence of S;

      assume that

       A1: SSets is non-ascending and

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

      

       A3: (M . ((SSets . 0 ) \ ( lim SSets))) >= 0 by SUPINF_2: 51;

      now

        let y be object;

        assume y in ( rng ((SSets . 0 ) (\) SSets));

        then

        consider x be object such that

         A4: x in NAT and

         A5: (((SSets . 0 ) (\) SSets) . x) = y by FUNCT_2: 11;

        reconsider x as Element of NAT by A4;

        ((SSets . 0 ) \ (SSets . x)) in S;

        hence y in S by A5, SETLIM_2:def 7;

      end;

      then ( rng ((SSets . 0 ) (\) SSets)) c= S;

      then

      reconsider Bseq = ((SSets . 0 ) (\) SSets) as SetSequence of S by RELAT_1:def 19;

      deffunc F1( Element of NAT ) = ((M * SSets) . 0 );

      consider seq1 be sequence of ExtREAL such that

       A6: for n be Element of NAT holds (seq1 . n) = F1(n) from FUNCT_2:sch 4;

       A7:

      now

        let k be Nat;

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

        

         A8: k is Element of NAT by ORDINAL1:def 12;

        ((SSets . k) \/ ((SSets . 0 ) \ (SSets . k))) = ((SSets . 0 ) \/ (SSets . k)) & (SSets . k) c= (SSets . 0 ) by A1, PROB_1:def 4, XBOOLE_1: 39;

        then ((SSets . k) \/ ((SSets . 0 ) \ (SSets . k))) = (SSets . 0 ) by XBOOLE_1: 12;

        then

         A9: ((SSets . k) \/ (Bseq . k)) = (SSets . 0 ) by SETLIM_2:def 7;

        (SSets . k) misses ((SSets . 0 ) \ (SSets . k)) by XBOOLE_1: 79;

        then (SSets . k) misses (Bseq . k) by SETLIM_2:def 7;

        then (M . (SSets . 0 )) = ((M . (SSets . k)) + (M . (Bseq . k))) by A9, MEASURE1: 30;

        then ((M * SSets) . 0 ) = ((M . (SSets . k)) + (M . (Bseq . k))) by FUNCT_2: 15;

        then (seq1 . k) = ((M . (SSets . k)) + (M . (Bseq . k))) by A6, A8;

        then (seq1 . k) = (((M * SSets) . k) + (M . (Bseq . k))) by A8, FUNCT_2: 15;

        hence (seq1 . k) = (((M * SSets) . k) + ((M * Bseq) . k)) by A8, FUNCT_2: 15;

      end;

      (M * SSets) is non-increasing by A1, Th30;

      then

       A10: (M * SSets) is convergent by RINFSUP2: 36;

      ( rng Bseq) c= S;

      then Bseq is sequence of S by FUNCT_2: 6;

      then

       A11: (M * Bseq) is nonnegative by MEASURE2: 1;

      

       A12: for n be Nat holds (seq1 . n) = ((M * SSets) . 0 )

      proof

        let n be Nat;

        n is Element of NAT by ORDINAL1:def 12;

        hence (seq1 . n) = ((M * SSets) . 0 ) by A6;

      end;

      

       A13: ( rng SSets) c= S;

      then SSets is sequence of S by FUNCT_2: 6;

      then

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

      then

       A15: -infty < ((M * SSets) . 0 ) by SUPINF_2: 51;

      (( inferior_setsequence SSets) . ( 0 + 1)) c= (SSets . 0 ) by A1, SETLIM_1: 50;

      then ( Intersection SSets) c= (SSets . 0 ) by A1, SETLIM_1: 52;

      then ( lim SSets) c= (SSets . 0 ) by A1, SETLIM_1: 61;

      then

       A16: ((SSets . 0 ) \/ ( lim SSets)) = (SSets . 0 ) by XBOOLE_1: 12;

      ( Intersection SSets) in S by A13, PROB_1:def 6;

      then

       A17: ( lim SSets) in S by A1, SETLIM_1: 61;

      then

       A18: ((SSets . 0 ) \ ( lim SSets)) is Element of S by PROB_1: 6;

      then (M . (((SSets . 0 ) \ ( lim SSets)) \/ ( lim SSets))) = ((M . ((SSets . 0 ) \ ( lim SSets))) + (M . ( lim SSets))) by A17, MEASURE1: 30, XBOOLE_1: 79;

      then

       A19: (M . ((SSets . 0 ) \/ ( lim SSets))) = ((M . ((SSets . 0 ) \ ( lim SSets))) + (M . ( lim SSets))) by XBOOLE_1: 39;

      ((M * SSets) . 0 ) < +infty by A2, FUNCT_2: 15;

      then

       A20: ((M * SSets) . 0 ) in REAL by A15, XXREAL_0: 14;

      for n,m be Nat st n <= m holds (Bseq . n) c= (Bseq . m)

      proof

        let n,m be Nat;

        assume n <= m;

        then (SSets . m) c= (SSets . n) by A1, PROB_1:def 4;

        then ((SSets . 0 ) \ (SSets . n)) c= ((SSets . 0 ) \ (SSets . m)) by XBOOLE_1: 34;

        then (Bseq . n) c= ((SSets . 0 ) \ (SSets . m)) by SETLIM_2:def 7;

        hence (Bseq . n) c= (Bseq . m) by SETLIM_2:def 7;

      end;

      then

       A21: Bseq is non-descending by PROB_1:def 5;

      then (M * Bseq) is non-decreasing by Th29;

      then (M * Bseq) is convergent by RINFSUP2: 37;

      then ( lim seq1) = (( lim (M * Bseq)) + ( lim (M * SSets))) by A10, A11, A14, A7, MESFUNC9: 11;

      then

       A22: ((M * SSets) . 0 ) = (( lim (M * Bseq)) + ( lim (M * SSets))) by A20, A12, MESFUNC5: 52;

      ( lim (M * Bseq)) = (M . ( lim Bseq)) by A21, Th26

      .= (M . ((SSets . 0 ) \ ( lim SSets))) by A1, SETLIM_1: 64, SETLIM_2: 86;

      then

       A23: ((M . ((SSets . 0 ) \ ( lim SSets))) + (M . ( lim SSets))) = (( lim (M * SSets)) + (M . ((SSets . 0 ) \ ( lim SSets)))) by A19, A16, A22, FUNCT_2: 15;

      

       A24: (M . ((SSets . 0 ) \ ( lim SSets))) <= (M . (SSets . 0 )) by A18, MEASURE1: 31, XBOOLE_1: 36;

      then (M . ((SSets . 0 ) \ ( lim SSets))) < +infty by A2, XXREAL_0: 2;

      then

       A25: (M . ( lim SSets)) = ((( lim (M * SSets)) + (M . ((SSets . 0 ) \ ( lim SSets)))) - (M . ((SSets . 0 ) \ ( lim SSets)))) by A3, A23, XXREAL_3: 28;

      (M . ((SSets . 0 ) \ ( lim SSets))) in REAL by A2, A24, A3, XXREAL_0: 14;

      hence (M . ( lim SSets)) = ( lim (M * SSets)) by A25, XXREAL_3: 22;

    end;

    definition

      let X be set;

      let F be Field_Subset of X;

      let S be SigmaField of X;

      let m be Measure of F;

      let M be sigma_Measure of S;

      :: MEASURE8:def12

      pred M is_extension_of m means for A be set st A in F holds (M . A) = (m . A);

    end

    theorem :: MEASURE8:32

    for X be non empty set, F be Field_Subset of X, m be Measure of F st (ex M be sigma_Measure of ( sigma F) st M is_extension_of m) holds m is completely-additive

    proof

      let X be non empty set, F be Field_Subset of X, m be Measure of F;

      given M be sigma_Measure of ( sigma F) such that

       A1: M is_extension_of m;

      

       A2: F c= ( sigma F) by PROB_1:def 9;

      for Aseq be Sep_Sequence of F st ( union ( rng Aseq)) in F holds ( SUM (m * Aseq)) = (m . ( union ( rng Aseq)))

      proof

        let Aseq be Sep_Sequence of F;

        reconsider Bseq = Aseq as sequence of ( sigma F) by A2, FUNCT_2: 7;

        reconsider Bseq as Sep_Sequence of ( sigma F);

         A3:

        now

          let n be object;

          assume n in NAT ;

          then

          reconsider n9 = n as Element of NAT ;

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

          then ((M * Bseq) . n) = (m . (Aseq . n9)) by A1;

          hence ((M * Bseq) . n) = ((m * Aseq) . n) by FUNCT_2: 15;

        end;

        assume ( union ( rng Aseq)) in F;

        then (m . ( union ( rng Aseq))) = (M . ( union ( rng Aseq))) by A1;

        then (m . ( union ( rng Aseq))) = ( SUM (M * Bseq)) by MEASURE1:def 6;

        hence thesis by A3, FUNCT_2: 12;

      end;

      hence m is completely-additive;

    end;

    theorem :: MEASURE8:33

    

     Th33: for X be non empty set, F be Field_Subset of X, m be Measure of F st m is completely-additive holds ex M be sigma_Measure of ( sigma F) st M is_extension_of m & M = (( sigma_Meas ( C_Meas m)) | ( sigma F))

    proof

      let X be non empty set, F be Field_Subset of X, m be Measure of F;

      assume

       A1: m is completely-additive;

      set M = (( sigma_Meas ( C_Meas m)) | ( sigma F));

      

       A2: F c= ( sigma_Field ( C_Meas m)) by Th20;

      then

       A3: ( sigma F) c= ( sigma_Field ( C_Meas m)) by PROB_1:def 9;

      then

      reconsider M as Function of ( sigma F), ExtREAL by FUNCT_2: 32;

      

       A4: for SS be Sep_Sequence of ( sigma F) holds ( SUM (M * SS)) = (M . ( union ( rng SS)))

      proof

        let SS be Sep_Sequence of ( sigma F);

        reconsider SS9 = SS as Sep_Sequence of ( sigma_Field ( C_Meas m)) by A3, FUNCT_2: 7;

        

         A5: ( rng SS) c= ( sigma F) by RELAT_1:def 19;

        (M * SS) = (( sigma_Meas ( C_Meas m)) * (( sigma F) |` SS)) by MONOID_1: 1

        .= (( sigma_Meas ( C_Meas m)) * SS9) by A5, RELAT_1: 94;

        then

         A6: ( SUM (M * SS)) = (( sigma_Meas ( C_Meas m)) . ( union ( rng SS9))) by MEASURE1:def 6;

        ( union ( rng SS)) is Element of ( sigma F) by MEASURE1: 24;

        hence ( SUM (M * SS)) = (M . ( union ( rng SS))) by A6, FUNCT_1: 49;

      end;

      (M . {} ) = (( sigma_Meas ( C_Meas m)) . {} ) by FUNCT_1: 49, PROB_1: 4

      .= 0 by VALUED_0:def 19;

      then

      reconsider M as sigma_Measure of ( sigma F) by A4, MEASURE1:def 6, MESFUNC5: 15, VALUED_0:def 19;

      take M;

      

       A7: F c= ( sigma F) by PROB_1:def 9;

      for A be set st A in F holds (M . A) = (m . A)

      proof

        let A be set;

        assume

         A8: A in F;

        then

        reconsider A9 = A as Subset of X;

        (M . A) = (( sigma_Meas ( C_Meas m)) . A) by A7, A8, FUNCT_1: 49

        .= (( C_Meas m) . A9) by A2, A8, MEASURE4:def 3;

        hence (M . A) = (m . A) by A1, A8, Th18;

      end;

      hence M is_extension_of m & M = (( sigma_Meas ( C_Meas m)) | ( sigma F));

    end;

    theorem :: MEASURE8:34

    

     Th34: (for n holds (M . (FSets . n)) < +infty ) implies (M . (( Partial_Union FSets) . k)) < +infty

    proof

      defpred P[ Nat] means (M . (( Partial_Union FSets) . $1)) < +infty ;

      assume

       A1: for n holds (M . (FSets . n)) < +infty ;

       A2:

      now

        let k be Nat;

        

         A3: ( In ( 0 , REAL )) <= (M . (( Partial_Union FSets) . k)) by SUPINF_2: 51;

        (M . (FSets . (k + 1))) < +infty & ( In ( 0 , REAL )) <= (M . (FSets . (k + 1))) by A1, SUPINF_2: 51;

        then

         A4: (M . (FSets . (k + 1))) in REAL by XXREAL_0: 10;

        assume P[k];

        then (M . (( Partial_Union FSets) . k)) in REAL by A3, XXREAL_0: 10;

        then

         A5: ((M . (( Partial_Union FSets) . k)) + (M . (FSets . (k + 1)))) in REAL by A4, XREAL_0:def 1;

        ( Partial_Union FSets) is Set_Sequence of F by Th15;

        then

         A6: (( Partial_Union FSets) . k) in F by Def2;

        (( Partial_Union FSets) . (k + 1)) = ((( Partial_Union FSets) . k) \/ (FSets . (k + 1))) by PROB_3:def 2;

        then (M . (( Partial_Union FSets) . (k + 1))) <= ((M . (( Partial_Union FSets) . k)) + (M . (FSets . (k + 1)))) by A6, MEASURE1: 10;

        hence P[(k + 1)] by A5, XXREAL_0: 9, XXREAL_0: 13;

      end;

      (( Partial_Union FSets) . 0 ) = (FSets . 0 ) by PROB_3:def 2;

      then

       A7: P[ 0 ] by A1;

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

      hence thesis;

    end;

    theorem :: MEASURE8:35

    for X be non empty set, F be Field_Subset of X, m be Measure of F st m is completely-additive & (ex Aseq be Set_Sequence of F st (for n be Nat holds (m . (Aseq . n)) < +infty ) & X = ( union ( rng Aseq))) holds for M be sigma_Measure of ( sigma F) st M is_extension_of m holds M = (( sigma_Meas ( C_Meas m)) | ( sigma F))

    proof

      let X be non empty set, F be Field_Subset of X, m be Measure of F;

      

       A1: F c= ( sigma F) by PROB_1:def 9;

      assume m is completely-additive;

      then

      consider M1 be sigma_Measure of ( sigma F) such that

       A2: M1 is_extension_of m and

       A3: M1 = (( sigma_Meas ( C_Meas m)) | ( sigma F)) by Th33;

      assume ex Aseq be Set_Sequence of F st (for n be Nat holds (m . (Aseq . n)) < +infty ) & X = ( union ( rng Aseq));

      then

      consider Aseq be Set_Sequence of F such that

       A4: for n be Nat holds (m . (Aseq . n)) < +infty and

       A5: X = ( union ( rng Aseq));

      let M be sigma_Measure of ( sigma F);

      reconsider Bseq = ( Partial_Union Aseq) as Set_Sequence of F by Th15;

      assume

       A6: M is_extension_of m;

      F c= ( sigma_Field ( C_Meas m)) by Th20;

      then

       A7: ( sigma F) c= ( sigma_Field ( C_Meas m)) by PROB_1:def 9;

      

       A8: for B be Subset of X st B in ( sigma F) holds (M . B) <= (M1 . B)

      proof

        let B be Subset of X;

        assume

         A9: B in ( sigma F);

        

         A10: for seq be Covering of B, F holds (M . B) <= ( SUM ( vol (m,seq)))

        proof

          let seq be Covering of B, F;

          

           A11: for n be Element of NAT holds (seq . n) in ( sigma F) by A1;

          now

            let y be object;

            assume y in ( rng seq);

            then

            consider x be object such that

             A12: x in NAT and

             A13: (seq . x) = y by FUNCT_2: 11;

            thus y in ( sigma F) by A11, A12, A13;

          end;

          then ( rng seq) c= ( sigma F);

          then

          reconsider seq1 = seq as SetSequence of ( sigma F) by RELAT_1:def 19;

          

           A14: ( rng seq1) c= ( sigma F);

          then

          reconsider Fseq = seq1 as sequence of ( sigma F) by FUNCT_2: 6;

          B c= ( union ( rng seq1)) by Def3;

          then ( Union seq1) in ( sigma F) & B c= ( Union seq1) by CARD_3:def 4, PROB_1: 17;

          then

           A15: (M . B) <= (M . ( Union seq1)) by A9, MEASURE1: 31;

          for n be object st n in NAT holds ((M * Fseq) . n) = (( vol (m,seq)) . n)

          proof

            let n be object;

            assume

             A16: n in NAT ;

            then

            reconsider n1 = n as Element of NAT ;

            n1 in ( dom Fseq) by A16, FUNCT_2:def 1;

            

            then ((M * Fseq) . n) = (M . (Fseq . n1)) by FUNCT_1: 13

            .= (m . (seq . n1)) by A6;

            hence ((M * Fseq) . n) = (( vol (m,seq)) . n) by Def5;

          end;

          then

           A17: ( SUM (M * Fseq)) = ( SUM ( vol (m,seq))) by FUNCT_2: 12;

          ( rng Fseq) is N_Sub_set_fam of X by MEASURE1: 23;

          then ( rng Fseq) is N_Measure_fam of ( sigma F) by A14, MEASURE2:def 1;

          then (M . ( union ( rng Fseq))) <= ( SUM (M * Fseq)) by MEASURE2: 11;

          then (M . ( Union seq1)) <= ( SUM ( vol (m,seq))) by A17, CARD_3:def 4;

          hence (M . B) <= ( SUM ( vol (m,seq))) by A15, XXREAL_0: 2;

        end;

        for r be ExtReal st r in ( Svc (m,B)) holds (M . B) <= r

        proof

          let r be ExtReal;

          assume r in ( Svc (m,B));

          then ex seq be Covering of B, F st r = ( SUM ( vol (m,seq))) by Def7;

          hence (M . B) <= r by A10;

        end;

        then (M . B) is LowerBound of ( Svc (m,B)) by XXREAL_2:def 2;

        then (M . B) <= ( inf ( Svc (m,B))) by XXREAL_2:def 4;

        then (M . B) <= (( C_Meas m) . B) by Def8;

        then (M . B) <= (( sigma_Meas ( C_Meas m)) . B) by A7, A9, MEASURE4:def 3;

        hence (M . B) <= (M1 . B) by A3, A9, FUNCT_1: 49;

      end;

      

       A18: for B be set st (ex k be Element of NAT st B c= (Bseq . k)) & B in ( sigma F) holds (M . B) = (M1 . B)

      proof

        let B be set;

        assume ex k be Element of NAT st B c= (Bseq . k);

        then

        consider k be Element of NAT such that

         A19: B c= (Bseq . k);

        

         A20: (M . (Bseq . k)) = (m . (Bseq . k)) by A6;

        assume

         A21: B in ( sigma F);

        then

        reconsider B9 = B as Subset of X;

        

         A22: F c= ( sigma F) & (Bseq . k) in F by PROB_1:def 9;

        then

         A23: ((Bseq . k) \ B) is Element of ( sigma F) by A21, PROB_1: 6;

        then (M . ((Bseq . k) \ B)) <= (M . (Bseq . k)) by A22, MEASURE1: 31, XBOOLE_1: 36;

        then

         A24: (M . ((Bseq . k) \ B)) < +infty by A4, A20, Th34, XXREAL_0: 2;

        ((M . B) + (M . ((Bseq . k) \ B))) = (M . (B \/ ((Bseq . k) \ B))) by A21, A23, MEASURE1: 30, XBOOLE_1: 79;

        then ((M . B) + (M . ((Bseq . k) \ B))) = (M . ((Bseq . k) \/ B)) by XBOOLE_1: 39;

        then

         A25: ((M . B) + (M . ((Bseq . k) \ B))) = (M . (Bseq . k)) by A19, XBOOLE_1: 12;

         0 <= (M . ((Bseq . k) \ B)) by SUPINF_2: 51;

        then

         A26: (M . B) = ((M . (Bseq . k)) - (M . ((Bseq . k) \ B))) by A25, A24, XXREAL_3: 28;

        

         A27: (M1 . (Bseq . k)) = (m . (Bseq . k)) by A2;

        ((M1 . B) + (M1 . ((Bseq . k) \ B))) = (M1 . (B \/ ((Bseq . k) \ B))) by A21, A23, MEASURE1: 30, XBOOLE_1: 79;

        then ((M1 . B) + (M1 . ((Bseq . k) \ B))) = (M1 . ((Bseq . k) \/ B)) by XBOOLE_1: 39;

        then

         A28: ((M1 . B) + (M1 . ((Bseq . k) \ B))) = (M1 . (Bseq . k)) by A19, XBOOLE_1: 12;

        (M1 . ((Bseq . k) \ B)) <= (M1 . (Bseq . k)) by A22, A23, MEASURE1: 31, XBOOLE_1: 36;

        then

         A29: (M1 . ((Bseq . k) \ B)) < +infty by A4, A27, Th34, XXREAL_0: 2;

         0 <= (M1 . ((Bseq . k) \ B)) by SUPINF_2: 51;

        then

         A30: (M1 . B) = ((M1 . (Bseq . k)) - (M1 . ((Bseq . k) \ B))) by A28, A29, XXREAL_3: 28;

        (M . ((Bseq . k) \ B)) <= (M1 . ((Bseq . k) \ B)) by A8, A21, A22, PROB_1: 6;

        then

         A31: ((M1 . (Bseq . k)) - (M1 . ((Bseq . k) \ B))) <= ((M . (Bseq . k)) - (M . ((Bseq . k) \ B))) by A27, A20, XXREAL_3: 37;

        (M . B9) <= (M1 . B9) by A8, A21;

        hence (M . B) = (M1 . B) by A26, A30, A31, XXREAL_0: 1;

      end;

      for B be object st B in ( sigma F) holds (M . B) = (M1 . B)

      proof

        let B be object;

        assume

         A32: B in ( sigma F);

        then

        reconsider B9 = B as Subset of X;

        deffunc F1( object) = (B9 /\ (Bseq . $1));

        

         A33: for n be object st n in NAT holds F1(n) in ( bool X);

        consider Cseq be sequence of ( bool X) such that

         A34: for n be object st n in NAT holds (Cseq . n) = F1(n) from FUNCT_2:sch 2( A33);

        reconsider Cseq as SetSequence of X;

        for n,m be Nat st n <= m holds (Cseq . n) c= (Cseq . m)

        proof

          let n,m be Nat;

          

           A35: n in NAT & m in NAT by ORDINAL1:def 12;

          

           A36: Bseq is non-descending by PROB_3: 11;

          assume n <= m;

          then (Bseq . n) c= (Bseq . m) by A36, PROB_1:def 5;

          then (B9 /\ (Bseq . n)) c= (B9 /\ (Bseq . m)) by XBOOLE_1: 26;

          then (Cseq . n) c= (B9 /\ (Bseq . m)) by A34, A35;

          hence (Cseq . n) c= (Cseq . m) by A34, A35;

        end;

        then

         A37: Cseq is non-descending by PROB_1:def 5;

        now

          let y be object;

          assume y in ( rng Cseq);

          then

          consider x be object such that

           A38: x in NAT and

           A39: (Cseq . x) = y by FUNCT_2: 11;

          reconsider x as Element of NAT by A38;

          (Bseq . x) in F;

          then ((Bseq . x) /\ B9) in ( sigma F) by A1, A32, MEASURE1: 34;

          hence y in ( sigma F) by A34, A39;

        end;

        then ( rng Cseq) c= ( sigma F);

        then

        reconsider Cseq as SetSequence of ( sigma F) by RELAT_1:def 19;

        for n be object st n in NAT holds ((M1 * ( Partial_Union Cseq)) . n) = ((M * ( Partial_Union Cseq)) . n)

        proof

          let n be object;

          assume

           A40: n in NAT ;

          then

          reconsider n1 = n as Nat;

           A41:

          now

            let x be set;

            assume x in (( Partial_Union Cseq) . n1);

            then

            consider k be Nat such that

             A42: k <= n1 and

             A43: x in (Cseq qua SetSequence of X . k) by PROB_3: 13;

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

            take k;

            x in (B9 /\ (Bseq . k)) by A34, A43;

            hence k <= n1 & x in (Bseq . k) by A42, XBOOLE_0:def 4;

          end;

          

           A44: (( Partial_Union Cseq) . n1) c= (Bseq . n1)

          proof

            let x be object;

            assume x in (( Partial_Union Cseq) . n1);

            then

            consider k be Element of NAT such that

             A45: k <= n1 and

             A46: x in (Bseq . k) by A41;

            Bseq is non-descending by PROB_3: 11;

            then (Bseq . k) c= (Bseq . n1) by A45, PROB_1:def 5;

            hence x in (Bseq . n1) by A46;

          end;

          

           A47: ((M1 * ( Partial_Union Cseq)) . n) = (M1 . (( Partial_Union Cseq) . n1)) by FUNCT_2: 15, A40;

          

           A48: ( rng ( Partial_Union Cseq)) c= ( sigma F) by RELAT_1:def 19;

          ( dom ( Partial_Union Cseq)) = NAT by PARTFUN1:def 2;

          then (( Partial_Union Cseq) . n1) in ( rng ( Partial_Union Cseq)) by FUNCT_1: 3, A40;

          then ((M1 * ( Partial_Union Cseq)) . n) = (M . (( Partial_Union Cseq) . n1)) by A47, A18, A44, A48, A40;

          hence ((M1 * ( Partial_Union Cseq)) . n) = ((M * ( Partial_Union Cseq)) . n) by FUNCT_2: 15, A40;

        end;

        then

         A49: (M1 * ( Partial_Union Cseq)) = (M * ( Partial_Union Cseq)) by FUNCT_2: 12;

        for n be Nat holds (Cseq . n) = (B9 /\ (Bseq . n)) by ORDINAL1:def 12, A34;

        then Cseq = (B9 (/\) Bseq) by SETLIM_2:def 5;

        then ( Union Cseq) = (B9 /\ ( Union Bseq)) by SETLIM_2: 38;

        then ( Union Cseq) = (B9 /\ ( Union Aseq)) by PROB_3: 15;

        then ( Union Cseq) = (B9 /\ X) by A5, CARD_3:def 4;

        then

         A50: B9 = ( Union Cseq) by XBOOLE_1: 28;

        then B9 = ( lim Cseq) by A37, SETLIM_1: 63;

        then (M1 . B) = ( lim (M1 * Cseq)) by A37, Th26;

        then (M1 . B) = ( lim (M * ( Partial_Union Cseq))) by A37, A49, PROB_4: 19;

        then (M1 . B) = ( lim (M * Cseq)) by A37, PROB_4: 19;

        then (M1 . B) = (M . ( lim Cseq)) by A37, Th26;

        hence (M1 . B) = (M . B) by A37, A50, SETLIM_1: 63;

      end;

      hence thesis by A3, FUNCT_2: 12;

    end;