measure4.miz

    begin

    reserve A,B,X for set,

S for SigmaField of X;

    theorem :: MEASURE4:1



     Th1: for S be non empty Subset-Family of X, F,G be sequence of S, A be Element of S st for n be Element of NAT holds (G . n) = (A /\ (F . n)) holds ( union ( rng G)) = (A /\ ( union ( rng F)))

    proof

      let S be non empty Subset-Family of X;

      let F,G be sequence of S, A be Element of S;

      assume

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

      thus ( union ( rng G)) c= (A /\ ( union ( rng F)))

      proof

        let r be object;

        assume r in ( union ( rng G));

        then

        consider E be set such that

         A2: r in E and

         A3: E in ( rng G) by TARSKI:def 4;

        consider s be object such that

         A4: s in ( dom G) and

         A5: E = (G . s) by A3, FUNCT_1:def 3;

        reconsider s as Element of NAT by A4;



         A6: r in (A /\ (F . s)) by A1, A2, A5;

        then

         A7: r in A by XBOOLE_0:def 4;



         A8: (F . s) in ( rng F) by FUNCT_2: 4;

        r in (F . s) by A6, XBOOLE_0:def 4;

        then r in ( union ( rng F)) by A8, TARSKI:def 4;

        hence thesis by A7, XBOOLE_0:def 4;

      end;

      let r be object;

      assume

       A9: r in (A /\ ( union ( rng F)));

      then

       A10: r in A by XBOOLE_0:def 4;

      r in ( union ( rng F)) by A9, XBOOLE_0:def 4;

      then

      consider E be set such that

       A11: r in E and

       A12: E in ( rng F) by TARSKI:def 4;

      consider s be object such that

       A13: s in ( dom F) and

       A14: E = (F . s) by A12, FUNCT_1:def 3;

      reconsider s as Element of NAT by A13;



       A15: (G . s) in ( rng G) by FUNCT_2: 4;

      (A /\ E) = (G . s) by A1, A14;

      then r in (G . s) by A10, A11, XBOOLE_0:def 4;

      hence thesis by A15, TARSKI:def 4;

    end;

    theorem :: MEASURE4:2



     Th2: for S be non empty Subset-Family of X holds for F,G be sequence of S st ((G . 0 ) = (F . 0 ) & for n be Nat holds (G . (n + 1)) = ((F . (n + 1)) \/ (G . n))) holds for H be sequence of S st ((H . 0 ) = (F . 0 ) & for n be Nat holds (H . (n + 1)) = ((F . (n + 1)) \ (G . n))) holds ( union ( rng F)) = ( union ( rng H))

    proof

      let S be non empty Subset-Family of X;

      let F,G be sequence of S;

      assume that

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

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

      let H be sequence of S;

      assume that

       A3: (H . 0 ) = (F . 0 ) and

       A4: for n be Nat holds (H . (n + 1)) = ((F . (n + 1)) \ (G . n));

      thus ( union ( rng F)) c= ( union ( rng H))

      proof

        let r be object;

        assume r in ( union ( rng F));

        then

        consider E be set such that

         A5: r in E and

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



         A7: ex s be object st s in ( dom F) & E = (F . s) by A6, FUNCT_1:def 3;

        ex s1 be Element of NAT st r in (H . s1)

        proof

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



           A8: ex k be Nat st P[k] by A5, A7;

          ex k be Nat st P[k] & for n be Nat st P[n] holds k <= n from NAT_1:sch 5( A8);

          then

          consider k be Nat such that

           A9: r in (F . k) and

           A10: for n be Nat st r in (F . n) holds k <= n;



           A11: (ex l be Nat st k = (l + 1)) implies ex s1 be Element of NAT st r in (H . s1)

          proof

            given l be Nat such that

             A12: k = (l + 1);

            take k;

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



             A13: not r in (G . l)

            proof

              assume r in (G . l);

              then

              consider i be Nat such that

               A14: i <= l and

               A15: r in (F . i) by A1, A2, MEASURE2: 5;

              k <= i by A10, A15;

              hence thesis by A12, A14, NAT_1: 13;

            end;

            (H . (l + 1)) = ((F . (l + 1)) \ (G . l)) by A4;

            hence thesis by A9, A12, A13, XBOOLE_0:def 5;

          end;

          k = 0 implies ex s1 be Element of NAT st r in (H . s1) by A3, A9;

          hence thesis by A11, NAT_1: 6;

        end;

        then

        consider s1 be Element of NAT such that

         A16: r in (H . s1);

        (H . s1) in ( rng H) by FUNCT_2: 4;

        hence thesis by A16, TARSKI:def 4;

      end;



       A17: for n be Element of NAT holds (H . n) c= (F . n)

      proof

        let n be Element of NAT ;



         A18: (ex k be Nat st n = (k + 1)) implies (H . n) c= (F . n)

        proof

          given k be Nat such that

           A19: n = (k + 1);

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

          (H . n) = ((F . n) \ (G . k)) by A4, A19;

          hence thesis;

        end;

        n = 0 implies (H . n) c= (F . n) by A3;

        hence thesis by A18, NAT_1: 6;

      end;

      ( union ( rng H)) c= ( union ( rng F))

      proof

        let r be object;

        assume r in ( union ( rng H));

        then

        consider E be set such that

         A20: r in E and

         A21: E in ( rng H) by TARSKI:def 4;

        consider s be object such that

         A22: s in ( dom H) and

         A23: E = (H . s) by A21, FUNCT_1:def 3;

        reconsider s as Element of NAT by A22;



         A24: (F . s) in ( rng F) by FUNCT_2: 4;

        E c= (F . s) by A17, A23;

        hence thesis by A20, A24, TARSKI:def 4;

      end;

      hence thesis;

    end;

    theorem :: MEASURE4:3



     Th3: ( bool X) is SigmaField of X

    proof



       A1: for M be N_Sub_set_fam of X st M c= ( bool X) holds ( union M) in ( bool X);

      reconsider Y = ( bool X) as Subset-Family of X;

      for A be set holds A in ( bool X) implies (X \ A) in ( bool X);

      then

      reconsider Y as non empty compl-closed sigma-additive Subset-Family of X by A1, MEASURE1:def 1, MEASURE1:def 5;

      Y is SigmaField of X;

      hence thesis;

    end;

    definition

      let X be set;

      :: MEASURE4:def1

      mode C_Measure of X -> Function of ( bool X), ExtREAL means

      : Def1: it is nonnegative zeroed & for A,B be Subset of X st A c= B holds (it . A) <= (it . B) & for F be sequence of ( bool X) holds (it . ( union ( rng F))) <= ( SUM (it * F));

      existence

      proof

        set M = (( bool X) --> 0. );

        take M;



         A1: for A be Subset of X holds 0. <= (M . A);

        then

         A2: M is nonnegative by MEASURE1:def 2;



         A3: for F be sequence of ( bool X) holds (M . ( union ( rng F))) <= ( SUM (M * F))

        proof

          let F be sequence of ( bool X);



           A4: (M . ( union ( rng F))) = 0. by FUNCOP_1: 7;



           A5: for r be Element of NAT st 0 <= r holds ((M * F) . r) = 0.

          proof

            let r be Element of NAT ;

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

            then ((M * F) . r) = (M . (F . r)) by FUNCT_1: 12;

            hence thesis by FUNCOP_1: 7;

          end;



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

          (M * F) is nonnegative by A2, MEASURE1: 25;

          hence thesis by A4, A5, A6, SUPINF_2: 48;

        end;

         {} c= X;

        then (M . {} ) = 0. by FUNCOP_1: 7;

        hence thesis by A1, A3, FUNCOP_1: 7, MEASURE1:def 2, VALUED_0:def 19;

      end;

    end

    reserve C for C_Measure of X;

    definition

      let X be set;

      let C be C_Measure of X;

      :: MEASURE4:def2

      func sigma_Field (C) -> non empty Subset-Family of X means

      : Def2: for A be Subset of X holds (A in it iff for W,Z be Subset of X holds (W c= A & Z c= (X \ A) implies ((C . W) + (C . Z)) <= (C . (W \/ Z))));

      existence

      proof

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

        defpred P[ set] means for A be set holds (A = $1 implies for W,Z be Subset of X holds (W c= A & Z c= (X \ A) implies ((C . W) + (C . Z)) <= (C . (W \/ Z))));

        consider D be set such that

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



         A2: for A be set holds (A in D iff A in ( bool X) & 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 A be set;

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

          hence thesis by A1;

        end;

        then

         A3: for A be object holds A in D implies A in ( bool X);

        now

          let W,Z be Subset of X;

          assume that

           A4: W c= A and Z c= (X \ A);



           A5: W = {} by A4;

          C is zeroed by Def1;

          then (C . W) = 0 by A5, VALUED_0:def 19;

          hence ((C . W) + (C . Z)) <= (C . (W \/ Z)) by A5, XXREAL_3: 4;

        end;

        then

        reconsider D as non empty Subset-Family of X by A2, A3, TARSKI:def 3;

        take D;

        thus thesis by A2;

      end;

      uniqueness

      proof

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

         A6: for A be Subset of X holds (A in D1 iff for W,Z be Subset of X holds (W c= A & Z c= (X \ A) implies ((C . W) + (C . Z)) <= (C . (W \/ Z)))) and

         A7: for A be Subset of X holds (A in D2 iff for W,Z be Subset of X holds (W c= A & Z c= (X \ A) implies ((C . W) + (C . Z)) <= (C . (W \/ Z))));

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

        proof

          let A be object;

          reconsider AA = A as set by TARSKI: 1;

          hereby

            assume

             A8: A in D1;

            then

            reconsider A9 = A as Subset of X;

            for W,Z be Subset of X holds (W c= AA & Z c= (X \ A9) implies ((C . W) + (C . Z)) <= (C . (W \/ Z))) by A6, A8;

            hence A in D2 by A7;

          end;

          assume

           A9: A in D2;

          then

          reconsider A as Subset of X;

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

          hence thesis by A6;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    theorem :: MEASURE4:4



     Th4: for W,Z be Subset of X holds (C . (W \/ Z)) <= ((C . W) + (C . Z))

    proof

      let W,Z be Subset of X;

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

      consider F be sequence of ( bool X) such that

       A1: ( rng F) = {W, Z, P} and

       A2: (F . 0 ) = W and

       A3: (F . 1) = Z and

       A4: for n be Element of NAT st 1 < n holds (F . n) = P by MEASURE1: 17;



       A5: ((C * F) . 1) = (C . Z) by A3, FUNCT_2: 15;

      set G = (C * F);



       A6: ( union {W, Z, P}) = (W \/ Z)

      proof

        thus ( union {W, Z, P}) c= (W \/ Z)

        proof

          let x be object;

          assume x in ( union {W, Z, P});

          then ex Y be set st x in Y & Y in {W, Z, P} by TARSKI:def 4;

          then x in W or x in Z or x in P by ENUMSET1:def 1;

          hence thesis by XBOOLE_0:def 3;

        end;

        let x be object;

        assume

         A7: x in (W \/ Z);

        now

          per cases by A7, XBOOLE_0:def 3;

            suppose

             A8: x in W;

            take Y = W;

            thus x in Y & Y in {W, Z, P} by A8, ENUMSET1:def 1;

          end;

            suppose

             A9: x in Z;

            take Y = Z;

            thus x in Y & Y in {W, Z, P} by A9, ENUMSET1:def 1;

          end;

        end;

        hence thesis by TARSKI:def 4;

      end;



       A10: C is zeroed by Def1;



       A11: for r be Element of NAT st 2 <= r holds ((C * F) . r) = 0.

      proof

        let r be Element of NAT ;

        assume 2 <= r;

        then (1 + 1) <= r;

        then 1 < r by NAT_1: 13;

        then

         A12: (F . r) = {} by A4;

        C is zeroed by Def1;

        then (C . (F . r)) = 0. by A12, VALUED_0:def 19;

        hence thesis by FUNCT_2: 15;

      end;

      C is nonnegative by Def1;

      then

       A13: (C * F) is nonnegative by MEASURE1: 25;

      (F . 2) = P by A4;

      then

       A14: ((C * F) . 2) = (C . P) by FUNCT_2: 15;



       A15: ((C * F) . 0 ) = (C . W) by A2, FUNCT_2: 15;

      consider y1,y2 be R_eal such that

       A16: y1 = (( Ser G) . 1) and

       A17: y2 = (( Ser G) . 0 );

      (( Ser G) . 2) = (y1 + (G . (1 + 1))) by A16, SUPINF_2:def 11

      .= ((( Ser G) . 1) + 0. ) by A14, A16, A10, VALUED_0:def 19

      .= (( Ser G) . 1) by XXREAL_3: 4

      .= (y2 + (G . ( 0 + 1))) by A17, SUPINF_2:def 11

      .= ((C . W) + (C . Z)) by A5, A15, A17, SUPINF_2:def 11;

      then ( SUM (C * F)) = ((C . W) + (C . Z)) by A13, A11, SUPINF_2: 48;

      hence thesis by A1, A6, Def1;

    end;

    theorem :: MEASURE4:5



     Th5: for A be Subset of X holds (A in ( sigma_Field C) iff 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 A be Subset of X;

      hereby

        assume

         A1: A in ( sigma_Field C);

        let W,Z be Subset of X;

        assume that

         A2: W c= A and

         A3: Z c= (X \ A);



         A4: (C . (W \/ Z)) <= ((C . W) + (C . Z)) by Th4;

        ((C . W) + (C . Z)) <= (C . (W \/ Z)) by A1, A2, A3, Def2;

        hence ((C . W) + (C . Z)) = (C . (W \/ Z)) by A4, XXREAL_0: 1;

      end;

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

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

      hence thesis by Def2;

    end;

    theorem :: MEASURE4:6



     Th6: for W,Z be Subset of X holds W in ( sigma_Field C) & Z misses W implies (C . (W \/ Z)) = ((C . W) + (C . Z))

    proof

      let W,Z be Subset of X;

      assume that

       A1: W in ( sigma_Field C) and

       A2: Z misses W;

      (Z \ W) c= (X \ W) by XBOOLE_1: 33;

      then Z c= (X \ W) by A2, XBOOLE_1: 83;

      hence thesis by A1, Th5;

    end;

    theorem :: MEASURE4:7



     Th7: A in ( sigma_Field C) implies (X \ A) in ( sigma_Field C)

    proof

      assume

       A1: A in ( sigma_Field C);

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

      proof

        let W,Z be Subset of X;

        assume that

         A2: W c= (X \ A) and

         A3: Z c= (X \ (X \ A));

        (X \ (X \ A)) = (X /\ A) by XBOOLE_1: 48;

        then Z c= A by A1, A3, XBOOLE_1: 28;

        hence thesis by A1, A2, Def2;

      end;

      hence thesis by Def2;

    end;

    theorem :: MEASURE4:8



     Th8: A in ( sigma_Field C) & B in ( sigma_Field C) implies (A \/ B) in ( sigma_Field C)

    proof

      assume that

       A1: A in ( sigma_Field C) and

       A2: B in ( sigma_Field C);

      reconsider A, B as Subset of X by A1, A2;

      set D = (A \/ B);

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

      proof

        let W,Z be Subset of X;

        assume that

         A3: W c= D and

         A4: Z c= (X \ D);

        set W2 = (W \ A);

        set Z1 = (W2 \/ Z);



         A5: ((X \ A) /\ (X \ B)) c= (X \ B) by XBOOLE_1: 17;

        set W1 = (W /\ A);



         A6: W1 c= A by XBOOLE_1: 17;

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

        then

         A7: (X \ (A \/ B)) c= (X \ A) by XBOOLE_1: 53;

        Z c= ((X \ A) /\ (X \ B)) by A4, XBOOLE_1: 53;

        then

         A8: Z c= (X \ B) by A5;

        W = (W1 \/ W2) by XBOOLE_1: 51;

        then (C . W) <= ((C . W1) + (C . W2)) by Th4;

        then

         A9: ((C . W) + (C . Z)) <= (((C . W1) + (C . W2)) + (C . Z)) by XXREAL_3: 36;

        (W \ A) c= ((B \/ A) \ A) by A3, XBOOLE_1: 33;

        then

         A10: (W \ A) c= (B \ A) by XBOOLE_1: 40;

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

        then W2 c= B by A10;

        then

         A11: ((C . W2) + (C . Z)) <= (C . Z1) by A2, A8, Def2;

        C is nonnegative by Def1;

        then

         A12: 0. <= (C . W1) by MEASURE1:def 2;

        (W \ A) c= (X \ A) by XBOOLE_1: 33;

        then (W2 \/ Z) c= ((X \ A) \/ Z) by XBOOLE_1: 9;

        then

         A13: Z1 c= (X \ A) by A4, A7, XBOOLE_1: 1, XBOOLE_1: 12;

        (C . (W \/ Z)) = (C . ((W1 \/ W2) \/ Z)) by XBOOLE_1: 51

        .= (C . (W1 \/ Z1)) by XBOOLE_1: 4

        .= ((C . W1) + (C . Z1)) by A1, A6, A13, Th5;

        then

         A14: ((C . W1) + ((C . W2) + (C . Z))) <= (C . (W \/ Z)) by A11, XXREAL_3: 36;



         A15: C is nonnegative by Def1;

        then

         A16: 0. <= (C . Z) by MEASURE1:def 2;

         0. <= (C . W2) by A15, MEASURE1:def 2;

        then (((C . W1) + (C . W2)) + (C . Z)) <= (C . (W \/ Z)) by A16, A12, A14, XXREAL_3: 44;

        then

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

        (C . (W \/ Z)) <= ((C . W) + (C . Z)) by Th4;

        hence thesis by A17, XXREAL_0: 1;

      end;

      hence thesis by Th5;

    end;

    theorem :: MEASURE4:9



     Th9: A in ( sigma_Field C) & B in ( sigma_Field C) implies (A /\ B) in ( sigma_Field C)

    proof

      assume that

       A1: A in ( sigma_Field C) and

       A2: B in ( sigma_Field C);



       A3: (X \ B) in ( sigma_Field C) by A2, Th7;

      (A /\ B) c= (X /\ X) by A1, A2, XBOOLE_1: 27;



      then

       A4: (A /\ B) = (X /\ (A /\ B)) by XBOOLE_1: 28

      .= (X \ (X \ (A /\ B))) by XBOOLE_1: 48

      .= (X \ ((X \ A) \/ (X \ B))) by XBOOLE_1: 54;

      (X \ A) in ( sigma_Field C) by A1, Th7;

      then ((X \ A) \/ (X \ B)) in ( sigma_Field C) by A3, Th8;

      hence thesis by A4, Th7;

    end;

    theorem :: MEASURE4:10



     Th10: A in ( sigma_Field C) & B in ( sigma_Field C) implies (A \ B) in ( sigma_Field C)

    proof

      assume that

       A1: A in ( sigma_Field C) and

       A2: B in ( sigma_Field C);

      for x be object holds x in (A \ B) iff x in (A /\ (X \ B))

      proof

        let x be object;

        hereby

          assume

           A3: x in (A \ B);

          then

           A4: not x in B by XBOOLE_0:def 5;

          x in A by A3;

          then x in (X \ B) by A1, A4, XBOOLE_0:def 5;

          hence x in (A /\ (X \ B)) by A3, XBOOLE_0:def 4;

        end;

        assume

         A5: x in (A /\ (X \ B));

        then x in (X \ B) by XBOOLE_0:def 4;

        then

         A6: not x in B by XBOOLE_0:def 5;

        x in A by A5, XBOOLE_0:def 4;

        hence thesis by A6, XBOOLE_0:def 5;

      end;

      then

       A7: (A \ B) = (A /\ (X \ B)) by TARSKI: 2;

      (X \ B) in ( sigma_Field C) by A2, Th7;

      hence thesis by A1, A7, Th9;

    end;

    theorem :: MEASURE4:11



     Th11: for N be sequence of S holds for A be Element of S holds ex F be sequence of S st for n be Element of NAT holds (F . n) = (A /\ (N . n))

    proof

      let N be sequence of S;

      let A be Element of S;

      defpred P[ object, object] means ($1 in NAT implies $2 = (A /\ (N . $1)));



       A1: for x be object st x in NAT holds ex y be object st y in S & P[x, y]

      proof

        let x be object;

        assume x in NAT ;

        then

        reconsider x as Element of NAT ;

        consider y be set such that

         A2: y = (A /\ (N . x));

        take y;

        thus thesis by A2;

      end;

      ex F be sequence of S st for x be object st x in NAT holds P[x, (F . x)] from FUNCT_2:sch 1( A1);

      then

      consider F be sequence of S such that

       A3: for x be object st x in NAT holds P[x, (F . x)];

      take F;

      thus thesis by A3;

    end;

    theorem :: MEASURE4:12



     Th12: ( sigma_Field C) is SigmaField of X

    proof



       A1: C is nonnegative by Def1;



       A2: for M be N_Sub_set_fam of X holds M c= ( sigma_Field C) implies ( union M) in ( sigma_Field C)

      proof

        let M be N_Sub_set_fam of X;

        assume

         A3: M c= ( sigma_Field C);

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

        proof

          reconsider S = ( bool X) as SigmaField of X by Th3;

          let W,Z be Subset of X;

          assume that

           A4: W c= ( union M) and

           A5: Z c= (X \ ( union M));

          consider F be sequence of ( bool X) such that

           A6: ( rng F) = M by SUPINF_2:def 8;

          consider G be sequence of S such that

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

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

          consider B be sequence of S such that

           A9: (B . 0 ) = (F . 0 ) and

           A10: for n be Nat holds (B . (n + 1)) = ((F . (n + 1)) \ (G . n)) by MEASURE2: 8;



           A11: ( union ( rng F)) = ( union ( rng B)) by A7, A8, A9, A10, Th2;

          defpred P[ Nat] means (G . $1) in ( sigma_Field C);



           A12: for n be Element of NAT holds (F . n) in ( sigma_Field C)

          proof

            let n be Element of NAT ;

            (F . n) in M by A6, FUNCT_2: 4;

            hence thesis by A3;

          end;



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

          proof

            let k be Nat;

            assume

             A14: (G . k) in ( sigma_Field C);



             A15: (F . (k + 1)) in ( sigma_Field C) by A12;

            (G . (k + 1)) = ((F . (k + 1)) \/ (G . k)) by A8;

            hence thesis by A14, A15, Th8;

          end;



           A16: P[ 0 ] by A12, A7;



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

          consider Q be sequence of S such that

           A18: for n be Element of NAT holds (Q . n) = (W /\ (B . n)) by Th11;



           A19: ( union ( rng Q)) = (W /\ ( union ( rng B))) by A18, Th1;

          consider QQ be sequence of S such that

           A20: (QQ . 0 ) = (Q . 0 ) and

           A21: for n be Nat holds (QQ . (n + 1)) = ((Q . (n + 1)) \/ (QQ . n)) by MEASURE2: 4;

          reconsider Q, QQ, F, G as sequence of ( bool X);



           A22: (F . 0 ) in ( sigma_Field C) by A12;

          defpred P[ Nat] means (C . (Z \/ (QQ . $1))) = ((C . Z) + (( Ser (C * Q)) . $1));



           A23: (C * Q) is nonnegative by A1, MEASURE1: 25;



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

          proof

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

            let k be Nat;



             A25: ((F . (k + 1)) \ (G . k)) c= (F . (k + 1)) by XBOOLE_1: 36;



             A26: (QQ . (k + 1)) = ((QQ . k) \/ (Q . (k + 1))) by A21;



             A27: (G . k) in ( sigma_Field C) by A17;

            (F . (k + 1)) in ( sigma_Field C) by A12;

            then

             A28: ((F . (k + 1)) \ (G . k)) in ( sigma_Field C) by A27, Th10;



             A29: 0. <= ((C * Q) . (k + 1)) by A23, SUPINF_2: 39;



             A30: 0. <= (( Ser (C * Q)) . k) by A23, SUPINF_2: 40;

            (QQ . 0 ) = (W /\ (F . 0 )) by A9, A18, A20;

            then

             A31: P[ 0 ] by A7, XBOOLE_1: 17;

            for n be Nat holds (QQ . n) misses ((F . (n + 1)) \ (G . n))

            proof

              let n be Nat;



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

              proof

                let n be Nat;

                assume

                 A33: (QQ . n) c= (G . n);



                 A34: (W /\ (F . (n + 1))) c= (F . (n + 1)) by XBOOLE_1: 17;

                (W /\ ((F . (n + 1)) \ (G . n))) c= (W /\ (F . (n + 1))) by XBOOLE_1: 26, XBOOLE_1: 36;

                then

                 A35: (W /\ ((F . (n + 1)) \ (G . n))) c= (F . (n + 1)) by A34;

                (QQ . (n + 1)) = ((Q . (n + 1)) \/ (QQ . n)) by A21

                .= ((W /\ (B . (n + 1))) \/ (QQ . n)) by A18

                .= ((W /\ ((F . (n + 1)) \ (G . n))) \/ (QQ . n)) by A10;

                then (QQ . (n + 1)) c= ((F . (n + 1)) \/ (G . n)) by A33, A35, XBOOLE_1: 13;

                hence thesis by A8;

              end;



               A36: for n be Nat holds P[n] from NAT_1:sch 2( A31, A32);

              (G . n) misses ((F . (n + 1)) \ (G . n)) by XBOOLE_1: 79;

              hence thesis by A36, XBOOLE_1: 63;

            end;

            then (QQ . k) misses ((F . (k + 1)) \ (G . k));

            then

             A37: ((QQ . k) /\ ((F . (k + 1)) \ (G . k))) = {} ;



             A38: (QQ . k) c= (X \ ((F . (k + 1)) \ (G . k)))

            proof

              let z be object;

              assume

               A39: z in (QQ . k);

              then not z in ((F . (k + 1)) \ (G . k)) by A37, XBOOLE_0:def 4;

              hence thesis by A39, XBOOLE_0:def 5;

            end;

            (Q . (k + 1)) = (W /\ (B . (k + 1))) by A18

            .= (W /\ ((F . (k + 1)) \ (G . k))) by A10;

            then

             A40: (Q . (k + 1)) c= ((F . (k + 1)) \ (G . k)) by XBOOLE_1: 17;

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

            then ((F . (k + 1)) \ (G . k)) c= ( union ( rng F)) by A25;

            then (X \ ( union ( rng F))) c= (X \ ((F . (k + 1)) \ (G . k))) by XBOOLE_1: 34;

            then Z c= (X \ ((F . (k + 1)) \ (G . k))) by A5, A6;

            then (Z \/ (QQ . k)) c= (X \ ((F . (k + 1)) \ (G . k))) by A38, XBOOLE_1: 8;



            then

             A41: ((C . (Q . (k + 1))) + (C . (Z \/ (QQ . k)))) = (C . ((Z \/ (QQ . k)) \/ (Q . (k + 1)))) by A40, A28, Th5

            .= (C . (Z \/ (QQ . (k + 1)))) by A26, XBOOLE_1: 4;



             A42: 0. <= (C . Z) by A1, SUPINF_2: 39;

            assume (C . (Z \/ (QQ . k))) = ((C . Z) + (( Ser (C * Q)) . k));



            then (C . (Z \/ (QQ . (k + 1)))) = (((C . Z) + (( Ser (C * Q)) . k)) + ((C * Q) . (k + 1))) by A41, FUNCT_2: 15

            .= ((C . Z) + ((( Ser (C * Q)) . k) + ((C * Q) . (k + 1)))) by A42, A30, A29, XXREAL_3: 44

            .= ((C . Z) + (( Ser (C * Q)) . (k + 1))) by SUPINF_2:def 11;

            hence thesis;

          end;

          (QQ . 0 ) = (W /\ (F . 0 )) by A9, A18, A20;

          then

           A43: (QQ . 0 ) c= (F . 0 ) by XBOOLE_1: 17;



           A44: (( Ser (C * Q)) . 0 ) = ((C * Q) . 0 ) by SUPINF_2:def 11

          .= (C . (QQ . 0 )) by A20, FUNCT_2: 15;

          (F . 0 ) in ( rng F) by FUNCT_2: 4;

          then (X \ ( union ( rng F))) c= (X \ (F . 0 )) by XBOOLE_1: 34, ZFMISC_1: 74;

          then Z c= (X \ (F . 0 )) by A5, A6;

          then

           A45: P[ 0 ] by A22, A43, A44, Th5;



           A46: for n be Nat holds P[n] from NAT_1:sch 2( A45, A24);

          defpred Q[ Nat] means (QQ . $1) c= W;



           A47: for n be Nat st Q[n] holds Q[(n + 1)]

          proof

            let n be Nat;

            assume

             A48: (QQ . n) c= W;



             A49: (W /\ (B . (n + 1))) c= W by XBOOLE_1: 17;

            (QQ . (n + 1)) = ((Q . (n + 1)) \/ (QQ . n)) by A21

            .= ((W /\ (B . (n + 1))) \/ (QQ . n)) by A18;

            then (QQ . (n + 1)) c= (W \/ W) by A48, A49, XBOOLE_1: 13;

            hence thesis;

          end;

          (QQ . 0 ) = (W /\ (B . 0 )) by A18, A20;

          then

           A50: Q[ 0 ] by XBOOLE_1: 17;



           A51: for n be Nat holds Q[n] from NAT_1:sch 2( A50, A47);



           A52: ( union ( rng Q)) = W by A4, A6, A11, A19, XBOOLE_1: 28;



           A53: (C . Z) is real implies ((C . W) + (C . Z)) <= (C . (W \/ Z))

          proof

            defpred P[ object, object] means ($1 = 0 implies $2 = ((C . (Z \/ W)) - (C . Z))) & ($1 <> 0 implies $2 = 0. );



             A54: for x be object st x in NAT holds ex y be object st y in ExtREAL & P[x, y]

            proof

              let x be object;

              assume x in NAT ;

              then

              reconsider x as Element of NAT ;

              x <> 0 implies ex y be set st y in ExtREAL & P[x, y];

              hence thesis;

            end;

            consider R be sequence of ExtREAL such that

             A55: for x be object st x in NAT holds P[x, (R . x)] from FUNCT_2:sch 1( A54);

            assume

             A56: (C . Z) is real;

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

            proof

              let n be Element of NAT ;

              (C . Z) in REAL or (C . Z) in { -infty , +infty } by XBOOLE_0:def 3, XXREAL_0:def 4;

              then

              consider y be Element of REAL such that

               A57: y = (C . Z) by A56, TARSKI:def 2;

              Z c= (Z \/ W) by XBOOLE_1: 7;

              then (C . Z) <= (C . (Z \/ W)) by Def1;

              then

               A58: ((C . Z) - (C . Z)) <= ((C . (Z \/ W)) - (C . Z)) by XXREAL_3: 37;

              ((C . Z) - (C . Z)) = (y - y) by A57, SUPINF_2: 3;

              hence thesis by A55, A58;

            end;

            then

             A59: R is nonnegative by SUPINF_2: 39;



             A60: for n be Element of NAT holds (( Ser (C * Q)) . n) <= ((C . (Z \/ W)) - (C . Z))

            proof

              let n be Element of NAT ;



               A61: (Z \/ (QQ . n)) c= (Z \/ W) by A51, XBOOLE_1: 9;

              ((( Ser (C * Q)) . n) + (C . Z)) = (C . (Z \/ (QQ . n))) by A46;

              then ((( Ser (C * Q)) . n) + (C . Z)) <= (C . (Z \/ W)) by A61, Def1;

              hence thesis by A56, XXREAL_3: 45;

            end;



             A62: for n be Element of NAT holds (( Ser (C * Q)) . n) <= (( Ser R) . n)

            proof

              let n be Element of NAT ;

              defpred P[ Nat] means (( Ser R) . $1) = ((C . (Z \/ W)) - (C . Z));



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

              proof

                let k be Nat;

                assume

                 A64: (( Ser R) . k) = ((C . (Z \/ W)) - (C . Z));

                set y = (( Ser R) . k);



                thus (( Ser R) . (k + 1)) = (y + (R . (k + 1))) by SUPINF_2:def 11

                .= (y + 0. ) by A55

                .= ((C . (Z \/ W)) - (C . Z)) by A64, XXREAL_3: 4;

              end;

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

              then

               A65: P[ 0 ] by A55;

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

              then (( Ser R) . n) = ((C . (Z \/ W)) - (C . Z));

              hence thesis by A60;

            end;

            set y = (( Ser R) . 0 );

            y = (R . 0 ) by SUPINF_2:def 11;

            then

             A66: y = ((C . (Z \/ W)) - (C . Z)) by A55;



             A67: (C . W) <= ( SUM (C * Q)) by A52, Def1;

            for k be Element of NAT st 1 <= k holds (R . k) = 0. by A55;

            then

             A68: ( SUM R) = (( Ser R) . 1) by A59, SUPINF_2: 48;

            (( Ser R) . 1) = (y + (R . ( 0 + 1))) by SUPINF_2:def 11

            .= (y + 0. ) by A55

            .= ((C . (Z \/ W)) - (C . Z)) by A66, XXREAL_3: 4;

            then ( SUM (C * Q)) <= ((C . (Z \/ W)) - (C . Z)) by A62, A68, MEASURE3: 1;

            then (C . W) <= ((C . (Z \/ W)) - (C . Z)) by A67, XXREAL_0: 2;

            hence thesis by A56, XXREAL_3: 45;

          end;



           A69: (C . Z) = +infty implies ((C . W) + (C . Z)) <= (C . (W \/ Z))

          proof



             A70: Z c= (W \/ Z) by XBOOLE_1: 7;

            assume

             A71: (C . Z) = +infty ;

             0. <= (C . W) by A1, MEASURE1:def 2;

            then ((C . W) + (C . Z)) = +infty by A71, XXREAL_3:def 2;

            hence thesis by A71, A70, Def1;

          end;

           0 <= (C . Z) by A1, MEASURE1:def 2;

          then (C . Z) is Element of REAL or (C . Z) = +infty by XXREAL_0: 14;

          hence thesis by A69, A53;

        end;

        hence thesis by Def2;

      end;

      for A be set holds A in ( sigma_Field C) implies (X \ A) in ( sigma_Field C) by Th7;

      then

      reconsider Y = ( sigma_Field C) as non empty compl-closed sigma-additive Subset-Family of X by A2, MEASURE1:def 1, MEASURE1:def 5;

      Y is SigmaField of X;

      hence thesis;

    end;

    registration

      let X be set;

      let C be C_Measure of X;

      cluster ( sigma_Field C) -> sigma-additive compl-closed non empty;

      coherence by Th12;

    end

    definition

      let X be set;

      let S be SigmaField of X;

      let A be N_Measure_fam of S;

      :: original: union

      redefine

      func union A -> Element of S ;

      coherence by MEASURE2:def 1, MEASURE1:def 5;

    end

    definition

      let X be set;

      let C be C_Measure of X;

      :: MEASURE4:def3

      func sigma_Meas (C) -> Function of ( sigma_Field C), ExtREAL means

      : Def3: for A be Subset of X st A in ( sigma_Field C) holds (it . A) = (C . A);

      existence

      proof

        ex D be Function of ( sigma_Field C), ExtREAL st for A be Subset of X holds A in ( sigma_Field C) implies (D . A) = (C . A)

        proof

          deffunc F( object) = (C . $1);



           A1: for S be object st S in ( sigma_Field C) holds F(S) in ExtREAL

          proof

            let S be object;

            assume S in ( sigma_Field C);

            reconsider S as set by TARSKI: 1;

            (C . S) in ExtREAL ;

            hence thesis;

          end;

          consider D be Function of ( sigma_Field C), ExtREAL such that

           A2: for S be object st S in ( sigma_Field C) holds (D . S) = F(S) from FUNCT_2:sch 2( A1);

          take D;

          thus thesis by A2;

        end;

        then

        consider D be Function of ( sigma_Field C), ExtREAL such that

         A3: for A be Subset of X st A in ( sigma_Field C) holds (D . A) = (C . A);

        take D;

        thus thesis by A3;

      end;

      uniqueness

      proof

        let D1,D2 be Function of ( sigma_Field C), ExtREAL such that

         A4: for A be Subset of X holds A in ( sigma_Field C) implies (D1 . A) = (C . A) and

         A5: for A be Subset of X holds A in ( sigma_Field C) implies (D2 . A) = (C . A);



         A6: for A be object st A in ( sigma_Field C) holds (D1 . A) = (D2 . A)

        proof

          let A be object;

          assume

           A7: A in ( sigma_Field C);

          then

          reconsider A as Subset of X;

          (D1 . A) = (C . A) by A4, A7

          .= (D2 . A) by A5, A7;

          hence thesis;

        end;



         A8: ( sigma_Field C) = ( dom D2) by FUNCT_2:def 1;

        ( sigma_Field C) = ( dom D1) by FUNCT_2:def 1;

        hence thesis by A8, A6, FUNCT_1: 2;

      end;

    end

    theorem :: MEASURE4:13



     Th13: ( sigma_Meas C) is Measure of ( sigma_Field C)

    proof

       A1:

      now

        let A be Element of ( sigma_Field C);

        reconsider A9 = A as Subset of X;



         A2: C is nonnegative by Def1;

        (( sigma_Meas C) . A9) = (C . A9) by Def3;

        hence 0. <= (( sigma_Meas C) . A) by A2, MEASURE1:def 2;

      end;

       {} in ( sigma_Field C) by PROB_1: 4;

      then

       A3: (( sigma_Meas C) . {} ) = (C . {} ) by Def3;

       A4:

      now

        let A,B be Element of ( sigma_Field C);

        reconsider A9 = A, B9 = B as Subset of X;



         A5: (( sigma_Meas C) . B9) = (C . B9) by Def3;

        assume A misses B;

        then

         A6: (C . (A9 \/ B9)) = ((C . A9) + (C . B9)) by Th6;

        (( sigma_Meas C) . A9) = (C . A9) by Def3;

        hence (( sigma_Meas C) . (A \/ B)) = ((( sigma_Meas C) . A) + (( sigma_Meas C) . B)) by A5, A6, Def3;

      end;

      C is zeroed by Def1;

      then (( sigma_Meas C) . {} ) = 0. by A3, VALUED_0:def 19;

      hence thesis by A1, A4, MEASURE1:def 2, MEASURE1:def 8, VALUED_0:def 19;

    end;

    ::$Notion-Name

    theorem :: MEASURE4:14



     Th14: ( sigma_Meas C) is sigma_Measure of ( sigma_Field C)

    proof

      reconsider M = ( sigma_Meas C) as Measure of ( sigma_Field C) by Th13;

      for F be Sep_Sequence of ( sigma_Field C) holds (M . ( union ( rng F))) <= ( SUM (M * F))

      proof

        let F be Sep_Sequence of ( sigma_Field C);

        consider A be Subset of X such that

         A1: A = ( union ( rng F));



         A2: for k be object st k in NAT holds ((M * F) . k) = ((C * F) . k)

        proof

          let k be object;

          assume

           A3: k in NAT ;

          then

           A4: ((M * F) . k) = (M . (F . k)) by FUNCT_2: 15;



           A5: (F . k) in ( sigma_Field C) by A3, FUNCT_2: 5;

          reconsider F as sequence of ( bool X) by FUNCT_2: 7;

          ((C * F) . k) = (C . (F . k)) by A3, FUNCT_2: 15;

          hence thesis by A4, A5, Def3;

        end;

        reconsider F9 = F as sequence of ( bool X) by FUNCT_2: 7;

        consider a,b be R_eal such that a = (M . A) and

         A6: b = (C . A);

        (C * F9) is sequence of ExtREAL ;

        then

         A7: (M * F) = (C * F) by A2, FUNCT_2: 12;

        reconsider F as sequence of ( bool X) by FUNCT_2: 7;

        b <= ( SUM (C * F)) by A1, A6, Def1;

        hence thesis by A1, A6, A7, Def3;

      end;

      hence thesis by MEASURE3: 14;

    end;

    registration

      let X be set;

      let C be C_Measure of X;

      cluster ( sigma_Meas C) -> nonnegative sigma-additive zeroed;

      coherence by Th14;

    end

    theorem :: MEASURE4:15



     Th15: for A be Subset of X holds (C . A) = 0. implies A in ( sigma_Field C)

    proof

      let A be Subset of X;

      assume

       A1: (C . A) = 0. ;

      now

        let W,Z be Subset of X;

        assume that

         A2: W c= A and Z c= (X \ A);

        Z c= (W \/ Z) by XBOOLE_1: 7;

        then

         A3: (C . Z) <= (C . (W \/ Z)) by Def1;

        C is nonnegative by Def1;

        then 0. <= (C . W) by MEASURE1:def 2;

        then (C . W) = 0. by A1, A2, Def1;

        hence ((C . W) + (C . Z)) <= (C . (W \/ Z)) by A3, XXREAL_3: 4;

      end;

      hence thesis by Def2;

    end;

    theorem :: MEASURE4:16

    ( sigma_Meas C) is complete

    proof

      let A be Subset of X;

      let B;

      assume that

       A1: B in ( sigma_Field C) and

       A2: A c= B and

       A3: (( sigma_Meas C) . B) = 0. ;

      reconsider B as Subset of X by A1;

      C is nonnegative by Def1;

      then

       A4: 0. <= (C . A) by MEASURE1:def 2;

      (C . B) = 0. by A1, A3, Def3;

      then (C . A) = 0. by A2, A4, Def1;

      hence thesis by Th15;

    end;