prob_4.miz



    begin

    reserve n,m,k for Element of NAT ,

x,X for set,

A1 for SetSequence of X,

Si for SigmaField of X,

XSeq for SetSequence of Si;

    reserve Omega for non empty set,

Sigma for SigmaField of Omega,

ASeq for SetSequence of Sigma,

P for Probability of Sigma;

    

     Lm1: for A,B,C be set holds C c= B implies (A \ C) = ((A \ B) \/ (A /\ (B \ C)))

    proof

      let A,B,C be set;

      assume

       A1: C c= B;

      thus (A \ C) c= ((A \ B) \/ (A /\ (B \ C)))

      proof

        let x be object;

        assume x in (A \ C);

        then x in A & not x in B or x in A & x in B & not x in C by XBOOLE_0:def 5;

        then x in (A \ B) or x in A & x in (B \ C) by XBOOLE_0:def 5;

        then x in (A \ B) or x in (A /\ (B \ C)) by XBOOLE_0:def 4;

        hence thesis by XBOOLE_0:def 3;

      end;

      let x be object;

      assume x in ((A \ B) \/ (A /\ (B \ C)));

      then x in (A \ B) or x in (A /\ (B \ C)) by XBOOLE_0:def 3;

      then

       A2: x in (A \ B) or x in A & x in (B \ C) by XBOOLE_0:def 4;

      then not x in C by A1, XBOOLE_0:def 5;

      hence thesis by A2, XBOOLE_0:def 5;

    end;

    definition

      let X, Si, XSeq, n;

      :: original: .

      redefine

      func XSeq . n -> Element of Si ;

      coherence

      proof

        thus (XSeq . n) is Element of Si;

      end;

    end

    theorem :: PROB_4:1

    

     Th1: ( rng XSeq) c= Si

    proof

      let x be object;

      assume x in ( rng XSeq);

      then ex n be Nat st x = (XSeq . n) by SETLIM_1: 4;

      hence thesis;

    end;

    theorem :: PROB_4:2

    

     Th2: for f be Function holds f is SetSequence of Si iff f is sequence of Si

    proof

      let f be Function;

      thus f is SetSequence of Si implies f is sequence of Si

      proof

        assume f is SetSequence of Si;

        then

        reconsider f as SetSequence of Si;

        ( rng f) c= Si & ( dom f) = NAT by Th1, FUNCT_2:def 1;

        hence thesis by FUNCT_2: 2;

      end;

      assume

       A1: f is sequence of Si;

      then

      reconsider f as SetSequence of X by FUNCT_2: 7;

      f is SetSequence of Si by A1;

      hence thesis;

    end;

    scheme :: PROB_4:sch1

    LambdaSigmaSSeq { X() -> set , Si() -> SigmaField of X() , F( set) -> Element of Si() } :

ex f be SetSequence of Si() st for n holds (f . n) = F(n);

      ex f be SetSequence of X() st for n holds (f . n) = F(n) from FUNCT_2:sch 4;

      then

      consider f be SetSequence of X() such that

       A1: for n holds (f . n) = F(n);

      for n be Nat holds (f . n) in Si()

      proof

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        then (f . n) = F(n) by A1;

        hence thesis;

      end;

      then ( rng f) c= Si() by NAT_1: 52;

      then

      reconsider f as SetSequence of Si() by RELAT_1:def 19;

      take f;

      thus thesis by A1;

    end;

    registration

      let X;

      cluster disjoint_valued for SetSequence of X;

      existence

      proof

        take A1 = ( NAT --> ( {} X));

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

        proof

          let m,n be Nat;

          m in NAT by ORDINAL1:def 12;

          then (A1 . m) = {} by FUNCOP_1: 7;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    registration

      let X, Si;

      cluster disjoint_valued for SetSequence of Si;

      existence

      proof

        reconsider MSi = Si as SigmaField of X;

        set f = the disjoint_valued sequence of MSi;

        reconsider f as SetSequence of Si by Th2;

        take f;

        thus thesis;

      end;

    end

    theorem :: PROB_4:3

    

     Th3: for A,B be Subset of X st A misses B holds ((A,B) followed_by {} ) is disjoint_valued

    proof

      let A,B be Subset of X;

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

      assume

       A1: A misses B;

      A1 is disjoint_valued

      proof

        

         A2: (A1 . 1) = B by FUNCT_7: 123;

        let m,n be Nat such that

         A3: m <> n;

        

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

        per cases ;

          suppose

           A5: m = 0 ;

          then n >= 1 by A3, NAT_1: 14;

          then

           A6: (n + 1) > 1 by NAT_1: 13;

          per cases by A6, NAT_1: 22;

            suppose n > 1;

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

            hence thesis;

          end;

            suppose n = 1;

            hence thesis by A1, A4, A5, FUNCT_7: 123;

          end;

        end;

          suppose

           A7: m <> 0 & m = 1;

          n >= 1 or n <= 1;

          then

           A8: (n + 1) > 1 or n < (1 + 1) by NAT_1: 13;

          per cases by A3, A7, A8, NAT_1: 14, NAT_1: 22;

            suppose n > 1;

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

            hence thesis;

          end;

            suppose n = 0 ;

            hence thesis by A1, A4, A2, A7;

          end;

        end;

          suppose

           A9: m <> 0 & m <> 1;

          then m >= 1 by NAT_1: 14;

          then (m + 1) > 1 by NAT_1: 13;

          then (A1 . m) = {} by A9, FUNCT_7: 124, NAT_1: 22;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: PROB_4:4

    

     Th4: for S be non empty set holds S is SigmaField of X iff S c= ( bool X) & (for A1 be SetSequence of X st ( rng A1) c= S holds ( Union A1) in S) & for A be Subset of X st A in S holds (A ` ) in S

    proof

      let S be non empty set;

      thus S is SigmaField of X implies S c= ( bool X) & (for A1 be SetSequence of X st ( rng A1) c= S holds ( Union A1) in S) & for A be Subset of X st A in S holds (A ` ) in S

      proof

        assume S is SigmaField of X;

        then

        reconsider S as SigmaField of X;

        for A1 be SetSequence of X st ( rng A1) c= S holds ( Union A1) in S

        proof

          let A1 be SetSequence of X;

          assume ( rng A1) c= S;

          then

          reconsider A1 as SetSequence of S by RELAT_1:def 19;

          ( Union A1) in S by PROB_1: 17;

          hence thesis;

        end;

        hence thesis by PROB_1: 15;

      end;

      assume that

       A1: S c= ( bool X) and

       A2: for A1 be SetSequence of X st ( rng A1) c= S holds ( Union A1) in S and

       A3: for A be Subset of X st A in S holds (A ` ) in S;

      for A1 be SetSequence of X st ( rng A1) c= S holds ( Intersection A1) in S

      proof

        let A1 be SetSequence of X such that

         A4: ( rng A1) c= S;

        for n be Nat holds (( Complement A1) . n) in S

        proof

          let n be Nat;

          reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

          (A1 . n) in ( rng A1) by NAT_1: 51;

          then ((A1 . n1) ` ) in S by A3, A4;

          hence thesis by PROB_1:def 2;

        end;

        then ( rng ( Complement A1)) c= S by NAT_1: 52;

        then (( Union ( Complement A1)) ` ) in S by A2, A3;

        hence thesis by PROB_1:def 3;

      end;

      hence thesis by A1, A3, PROB_1: 15;

    end;

    theorem :: PROB_4:5

    

     Th5: for A,B be Event of Sigma holds (P . (A \ B)) = ((P . (A \/ B)) - (P . B))

    proof

      let A,B be Event of Sigma;

      ((P . (A \/ B)) - (P . B)) = (((P . B) + (P . (A \ B))) - (P . B)) by PROB_1: 36;

      hence thesis;

    end;

    theorem :: PROB_4:6

    

     Th6: for A,B be Event of Sigma st A c= B & (P . B) = 0 holds (P . A) = 0

    proof

      let A,B be Event of Sigma;

      assume A c= B & (P . B) = 0 ;

      then (P . A) <= 0 by PROB_1: 34;

      hence thesis by PROB_1:def 8;

    end;

    theorem :: PROB_4:7

    

     Th7: (for n holds (P . (ASeq . n)) = 0 ) iff (P . ( Union ASeq)) = 0

    proof

      hereby

        assume

         A1: for n holds (P . (ASeq . n)) = 0 ;

        for n be Nat holds (( Partial_Sums (P * ASeq)) . n) = 0

        proof

          defpred P[ Nat] means (( Partial_Sums (P * ASeq)) . $1) = 0 ;

          

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

          proof

            let k be Nat such that

             A3: P[k];

            

            thus (( Partial_Sums (P * ASeq)) . (k + 1)) = ((( Partial_Sums (P * ASeq)) . k) + ((P * ASeq) . (k + 1))) by SERIES_1:def 1

            .= ( 0 + (P . (ASeq . (k + 1)))) by A3, FUNCT_2: 15

            .= 0 by A1;

          end;

          (( Partial_Sums (P * ASeq)) . 0 ) = ((P * ASeq) . 0 ) by SERIES_1:def 1

          .= (P . (ASeq . 0 )) by FUNCT_2: 15

          .= 0 by A1;

          then

           A4: P[ 0 ];

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

        end;

        then for n be Nat st 0 <= n holds (( Partial_Sums (P * ASeq)) . n) = 0 ;

        then

         A5: ( Partial_Sums (P * ASeq)) is convergent & ( lim ( Partial_Sums (P * ASeq))) = 0 by PROB_1: 1;

        now

          let n be Nat;

          (( Partial_Diff_Union ASeq) . n) c= (ASeq . n) by PROB_3: 33;

          hence ((P * ( Partial_Diff_Union ASeq)) . n) <= ((P * ASeq) . n) by PROB_3: 5;

        end;

        then

         A6: for n be Nat holds (( Partial_Sums (P * ( Partial_Diff_Union ASeq))) . n) <= (( Partial_Sums (P * ASeq)) . n) by SERIES_1: 14;

        ( Partial_Sums (P * ( Partial_Diff_Union ASeq))) is convergent by PROB_3: 45;

        then ( Sum (P * ( Partial_Diff_Union ASeq))) <= 0 by A5, A6, SEQ_2: 18;

        then (P . ( Union ( Partial_Diff_Union ASeq))) <= 0 by PROB_3: 46;

        then

         A7: (P . ( Union ASeq)) <= 0 by PROB_3: 36;

        ( Union ASeq) is Event of Sigma by PROB_1: 26;

        hence (P . ( Union ASeq)) = 0 by A7, PROB_1:def 8;

      end;

      assume

       A8: (P . ( Union ASeq)) = 0 ;

      hereby

        reconsider Y2 = ( Union ASeq) as Event of Sigma by PROB_1: 26;

        let n;

        reconsider Y1 = (ASeq . n) as Event of Sigma;

        (ASeq . n) in ( rng ASeq) by SETLIM_1: 4;

        then (ASeq . n) c= ( union ( rng ASeq)) by ZFMISC_1: 74;

        then Y1 c= Y2 by CARD_3:def 4;

        hence (P . (ASeq . n)) = 0 by A8, Th6;

      end;

    end;

    theorem :: PROB_4:8

    

     Th8: (for A be set st A in ( rng ASeq) holds (P . A) = 0 ) iff (P . ( union ( rng ASeq))) = 0

    proof

      hereby

        assume

         A1: for A be set st A in ( rng ASeq) holds (P . A) = 0 ;

        for n holds (P . (ASeq . n)) = 0 by SETLIM_1: 4, A1;

        then (P . ( Union ASeq)) = 0 by Th7;

        hence (P . ( union ( rng ASeq))) = 0 by CARD_3:def 4;

      end;

      assume (P . ( union ( rng ASeq))) = 0 ;

      then

       A2: (P . ( Union ASeq)) = 0 by CARD_3:def 4;

      hereby

        let A be set;

        assume A in ( rng ASeq);

        then

        consider n1 be Nat such that

         A3: A = (ASeq . n1) by SETLIM_1: 4;

        n1 in NAT by ORDINAL1:def 12;

        hence (P . A) = 0 by A2, Th7, A3;

      end;

    end;

    theorem :: PROB_4:9

    

     Th9: for seq be sequence of REAL , Eseq be sequence of ExtREAL st seq = Eseq holds ( Partial_Sums seq) = ( Ser Eseq)

    proof

      let seq be sequence of REAL , Eseq be sequence of ExtREAL such that

       A1: seq = Eseq;

      reconsider Ps = ( Partial_Sums seq) as sequence of ExtREAL by FUNCT_2: 7, NUMBERS: 31;

      defpred P[ Nat] means (Ps . $1) = (( Ser Eseq) . $1);

      

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

      proof

        let k be Nat such that

         A3: (Ps . k) = (( Ser Eseq) . k);

        reconsider Psk = (Ps . k) as Real;

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

        (Ps . (k + 1)) = (Psk + (seq . (k + 1))) & (( Ser Eseq) . (k + 1)) = ((( Ser Eseq) . kk) + (Eseq . (kk + 1))) by SERIES_1:def 1, SUPINF_2:def 11;

        hence thesis by A1, A3, SUPINF_2: 1;

      end;

      (Ps . 0 ) = (Eseq . 0 ) by A1, SERIES_1:def 1

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

      then

       A4: P[ 0 ];

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

      hence thesis;

    end;

    theorem :: PROB_4:10

    

     Th10: for seq be sequence of REAL , Eseq be sequence of ExtREAL st seq = Eseq & seq is bounded_above holds ( upper_bound seq) = ( sup ( rng Eseq))

    proof

      let seq be sequence of REAL , Eseq be sequence of ExtREAL such that

       A1: seq = Eseq and

       A2: seq is bounded_above;

      reconsider s = ( upper_bound seq) as R_eal by XXREAL_0:def 1;

      

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

      

       A4: ( rng Eseq) <> { -infty }

      proof

        assume ( rng Eseq) = { -infty };

        then

        reconsider k1 = -infty as Element of ( rng Eseq) by TARSKI:def 1;

        consider n1 be object such that

         A5: n1 in NAT and (Eseq . n1) = k1 by A3, FUNCT_1:def 3;

        reconsider n1 as Element of NAT by A5;

        (seq . n1) = k1 by A1;

        hence contradiction;

      end;

      for x be ExtReal holds x in ( rng Eseq) implies x <= s

      proof

        let x be ExtReal;

        assume x in ( rng Eseq);

        then ex n1 be object st n1 in NAT & (Eseq . n1) = x by A3, FUNCT_1:def 3;

        hence thesis by A1, A2, RINFSUP1: 7;

      end;

      then

       A6: s is UpperBound of ( rng Eseq) by XXREAL_2:def 1;

      then

       A7: ( rng Eseq) is bounded_above by XXREAL_2:def 10;

      

       A8: s <= ( sup ( rng Eseq))

      proof

        reconsider r1 = ( sup ( rng Eseq)) as Element of REAL by A7, A4, XXREAL_2: 57;

        

         A9: ( sup ( rng Eseq)) is UpperBound of ( rng Eseq) by XXREAL_2:def 3;

        for n be Nat holds (seq . n) <= r1

        proof

          let n be Nat;

          n in NAT by ORDINAL1:def 12;

          hence thesis by A1, A3, FUNCT_1: 3, XXREAL_2:def 1, A9;

        end;

        hence thesis by RINFSUP1: 9;

      end;

      ( sup ( rng Eseq)) <= s by A6, XXREAL_2:def 3;

      hence thesis by A8, XXREAL_0: 1;

    end;

    theorem :: PROB_4:11

    

     Th11: for seq be sequence of REAL , Eseq be sequence of ExtREAL st seq = Eseq & seq is bounded_below holds ( lower_bound seq) = ( inf ( rng Eseq))

    proof

      let seq be sequence of REAL , Eseq be sequence of ExtREAL such that

       A1: seq = Eseq and

       A2: seq is bounded_below;

      reconsider s = ( lower_bound seq) as R_eal by XXREAL_0:def 1;

      

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

      

       A4: ( rng Eseq) <> { +infty }

      proof

        assume ( rng Eseq) = { +infty };

        then

        reconsider k1 = +infty as Element of ( rng Eseq) by TARSKI:def 1;

        consider n1 be object such that

         A5: n1 in NAT and (Eseq . n1) = k1 by A3, FUNCT_1:def 3;

        reconsider n1 as Element of NAT by A5;

        (seq . n1) = k1 by A1;

        hence contradiction;

      end;

      for x be ExtReal holds x in ( rng Eseq) implies s <= x

      proof

        let x be ExtReal;

        assume x in ( rng Eseq);

        then ex n1 be object st n1 in NAT & (Eseq . n1) = x by A3, FUNCT_1:def 3;

        hence thesis by A1, A2, RINFSUP1: 8;

      end;

      then

       A6: s is LowerBound of ( rng Eseq) by XXREAL_2:def 2;

      then

       A7: ( rng Eseq) is bounded_below by XXREAL_2:def 9;

      

       A8: ( inf ( rng Eseq)) <= s

      proof

        reconsider r1 = ( inf ( rng Eseq)) as Element of REAL by A7, A4, XXREAL_2: 58;

        

         A9: ( inf ( rng Eseq)) is LowerBound of ( rng Eseq) by XXREAL_2:def 4;

        for n be Nat holds r1 <= (seq . n)

        proof

          let n be Nat;

          n in NAT by ORDINAL1:def 12;

          hence thesis by A1, A3, FUNCT_1: 3, XXREAL_2:def 2, A9;

        end;

        hence thesis by RINFSUP1: 10;

      end;

      s <= ( inf ( rng Eseq)) by A6, XXREAL_2:def 4;

      hence thesis by A8, XXREAL_0: 1;

    end;

    theorem :: PROB_4:12

    

     Th12: for seq be sequence of REAL , Eseq be sequence of ExtREAL st seq = Eseq & seq is nonnegative summable holds ( Sum seq) = ( SUM Eseq)

    proof

      let seq be sequence of REAL , Eseq be sequence of ExtREAL such that

       A1: seq = Eseq and

       A2: seq is nonnegative summable;

      

       A3: for n be Nat holds (seq . n) >= 0 by A2, RINFSUP1:def 3;

      ( Partial_Sums seq) is convergent by A2;

      then

       A4: ( Partial_Sums seq) is bounded;

      then ( upper_bound ( Partial_Sums seq)) = ( sup ( rng ( Ser Eseq))) by A1, Th9, Th10;

      then ( upper_bound ( Partial_Sums seq)) = ( SUM Eseq);

      hence thesis by A4, A3, RINFSUP1: 24, SERIES_1: 16;

    end;

    theorem :: PROB_4:13

    

     Th13: P is sigma_Measure of Sigma

    proof

      set Z = Sigma;

      reconsider P1 = P as Function of Z, ExtREAL by FUNCT_2: 7, NUMBERS: 31;

      for x be ExtReal holds x in ( rng P1) implies 0. <= x

      proof

        let x be ExtReal;

        assume

         A1: x in ( rng P1);

        ( dom P1) = Sigma by FUNCT_2:def 1;

        then

        consider y be object such that

         A2: y in Sigma and

         A3: (P1 . y) = x by A1, FUNCT_1:def 3;

        reconsider y1 = y as Event of Sigma by A2;

         0 <= (P . y1) by PROB_1:def 8;

        hence thesis by A3;

      end;

      then

       A4: ( rng P1) is nonnegative by SUPINF_2:def 9;

      for F be Sep_Sequence of Z holds ( SUM (P1 * F)) = (P1 . ( union ( rng F)))

      proof

        let F be Sep_Sequence of Z;

        reconsider F2 = F as disjoint_valued SetSequence of Sigma by Th2;

        for n be Nat holds ((P * F2) . n) >= 0 by PROB_3: 4;

        then

         A5: (P * F2) is nonnegative by RINFSUP1:def 3;

        ( Partial_Sums (P * F2)) is convergent by PROB_3: 45;

        then (P * F2) is summable;

        then (P . ( Union F2)) = ( Sum (P * F2)) & ( Sum (P * F2)) = ( SUM (P1 * F)) by A5, Th12, PROB_3: 46;

        hence thesis by CARD_3:def 4;

      end;

      hence thesis by A4, MEASURE1:def 6, SUPINF_2:def 12;

    end;

    definition

      let Omega, Sigma, P;

      :: PROB_4:def1

      func P2M (P) -> sigma_Measure of Sigma equals P;

      coherence by Th13;

    end

    theorem :: PROB_4:14

    

     Th14: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S st (M . X) = 1 holds M is Probability of S

    proof

      let X be non empty set, S be SigmaField of X, M be sigma_Measure of S such that

       A1: (M . X) = 1;

      

       A2: for A be Element of S holds (M . A) <= 1

      proof

        reconsider X as Element of S by PROB_1: 5;

        let A be Element of S;

        (M . A) <= (M . X) by MEASURE1: 31;

        hence thesis by A1;

      end;

      

       A3: for x be object st x in S holds (M . x) in REAL

      proof

        let x be object;

        assume x in S;

        then

        reconsider x as Element of S;

        

         A4: 1 in REAL & 0 in REAL by XREAL_0:def 1;

         0. <= (M . x) & (M . x) <= 1 by A2, MEASURE1:def 2;

        hence thesis by A4, XXREAL_0: 45;

      end;

      ( dom M) = S by FUNCT_2:def 1;

      then

      reconsider P1 = M as Function of S, REAL by A3, FUNCT_2: 3;

      reconsider P1 as Function of S, REAL ;

      

       A5: for ASeq be SetSequence of S st ASeq is non-ascending holds (P1 * ASeq) is convergent & ( lim (P1 * ASeq)) = (P1 . ( Intersection ASeq))

      proof

        let ASeq be SetSequence of S such that

         A6: ASeq is non-ascending;

        for n be Nat holds 0 <= ((P1 * ASeq) . n)

        proof

          let n be Nat;

          

           A7: n in NAT by ORDINAL1:def 12;

          reconsider A = (ASeq . n) as Event of S;

           0 <= (P1 . A) & ( dom (P1 * ASeq)) = NAT by MEASURE1:def 2, SEQ_1: 1;

          hence thesis by FUNCT_1: 12, A7;

        end;

        then

         A8: (P1 * ASeq) is bounded_below by RINFSUP1: 10;

        reconsider F = ASeq as sequence of S by Th2;

        

         A9: for n be Nat holds (F . (n + 1)) c= (F . n) by A6, PROB_2: 6;

        

         A10: (M . (F . 0 )) < +infty by A3, XXREAL_0: 9;

        now

          let n be Nat;

          reconsider nn = n as Element of NAT by ORDINAL1:def 12;

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

          then

           A11: ((M * F) . nn) = (M . (F . nn)) & ((M * F) . (nn + 1)) = (M . (F . (nn + 1))) by FUNCT_1: 12;

          (F . (n + 1)) c= (F . n) by A6, PROB_2: 6;

          hence ((P1 * ASeq) . (n + 1)) <= ((P1 * ASeq) . n) by A11, MEASURE1: 31;

        end;

        then

         A12: (P1 * ASeq) is non-increasing by SEQM_3:def 9;

        

        then ( lim (P1 * ASeq)) = ( lower_bound (P1 * ASeq)) by A8, RINFSUP1: 25

        .= ( inf ( rng (M * F))) by A8, Th11;

        

        then ( lim (P1 * ASeq)) = (M . ( meet ( rng F))) by A9, A10, MEASURE3: 12

        .= (P1 . ( Intersection ASeq)) by SETLIM_1: 8;

        hence thesis by A8, A12;

      end;

      

       A13: for A,B be Event of S st A misses B holds (P1 . (A \/ B)) = ((P1 . A) + (P1 . B))

      proof

        let A,B be Event of S such that

         A14: A misses B;

        reconsider A, B as Element of S;

        reconsider A2 = A, B2 = B as Element of S;

        (P1 . (A \/ B)) = ((M . A2) + (M . B2)) by A14, MEASURE1: 30

        .= ((P1 . A) + (P1 . B)) by SUPINF_2: 1;

        hence thesis;

      end;

      (for A be Event of S holds 0 <= (P1 . A)) & (P1 . X) = 1 by A1, MEASURE1:def 2;

      hence thesis by A13, A5, PROB_1:def 8;

    end;

    definition

      let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;

      assume

       A1: (M . X) = 1;

      :: PROB_4:def2

      func M2P (M) -> Probability of S equals M;

      coherence by A1, Th14;

    end

    

     Lm2: A1 is non-descending implies for n be Nat holds (( Partial_Union A1) . n) = (A1 . n)

    proof

      defpred P[ Nat] means (( Partial_Union A1) . $1) = (A1 . $1);

      assume

       A1: A1 is non-descending;

      

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

      proof

        let k be Nat such that

         A3: P[k];

        

         A4: (A1 . k) c= (A1 . (k + 1)) by A1, PROB_2: 7;

        

        thus (( Partial_Union A1) . (k + 1)) = ((A1 . k) \/ (A1 . (k + 1))) by A3, PROB_3:def 2

        .= (A1 . (k + 1)) by A4, XBOOLE_1: 12;

      end;

      

       A5: P[ 0 ] by PROB_3:def 2;

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

    end;

    theorem :: PROB_4:15

    

     Th15: A1 is non-descending implies ( Partial_Union A1) = A1 by Lm2;

    theorem :: PROB_4:16

    

     Th16: A1 is non-descending implies (( Partial_Diff_Union A1) . 0 ) = (A1 . 0 ) & for n be Nat holds (( Partial_Diff_Union A1) . (n + 1)) = ((A1 . (n + 1)) \ (A1 . n))

    proof

      assume

       A1: A1 is non-descending;

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

      let n be Nat;

      

      thus (( Partial_Diff_Union A1) . (n + 1)) = ((A1 . (n + 1)) \ (( Partial_Union A1) . n)) by PROB_3:def 3

      .= ((A1 . (n + 1)) \ (A1 . n)) by A1, Lm2;

    end;

    theorem :: PROB_4:17

    A1 is non-descending implies for n holds (A1 . (n + 1)) = ((( Partial_Diff_Union A1) . (n + 1)) \/ (A1 . n))

    proof

      assume

       A1: A1 is non-descending;

      thus for n holds (A1 . (n + 1)) = ((( Partial_Diff_Union A1) . (n + 1)) \/ (A1 . n))

      proof

        let n;

        

         A2: (A1 . n) c= (A1 . (n + 1)) by A1, PROB_2: 7;

        

        thus ((( Partial_Diff_Union A1) . (n + 1)) \/ (A1 . n)) = (((A1 . (n + 1)) \ (( Partial_Union A1) . n)) \/ (A1 . n)) by PROB_3:def 3

        .= (((A1 . (n + 1)) \ (A1 . n)) \/ (A1 . n)) by A1, Lm2

        .= ((A1 . (n + 1)) \/ (A1 . n)) by XBOOLE_1: 39

        .= (A1 . (n + 1)) by A2, XBOOLE_1: 12;

      end;

    end;

    theorem :: PROB_4:18

    

     Th18: A1 is non-descending implies for n be Nat holds (( Partial_Diff_Union A1) . (n + 1)) misses (A1 . n)

    proof

      assume

       A1: A1 is non-descending;

      let n be Nat;

      (( Partial_Diff_Union A1) . (n + 1)) = ((A1 . (n + 1)) \ (A1 . n)) by A1, Th16;

      hence thesis by XBOOLE_1: 79;

    end;

    theorem :: PROB_4:19

    XSeq is non-descending implies ( Partial_Union XSeq) = XSeq by Th15;

    theorem :: PROB_4:20

    XSeq is non-descending implies (( Partial_Diff_Union XSeq) . 0 ) = (XSeq . 0 ) & for n holds (( Partial_Diff_Union XSeq) . (n + 1)) = ((XSeq . (n + 1)) \ (XSeq . n)) by Th16;

    theorem :: PROB_4:21

    XSeq is non-descending implies for n holds (( Partial_Diff_Union XSeq) . (n + 1)) misses (XSeq . n) by Th18;

    definition

      let Omega, Sigma, P;

      :: PROB_4:def3

      attr P is complete means for A be Subset of Omega holds for B be set st B in Sigma holds (A c= B & (P . B) = 0 implies A in Sigma);

    end

    theorem :: PROB_4:22

    P is complete iff ( P2M P) is complete by MEASURE3:def 1;

    definition

      let Omega, Sigma, P;

      :: PROB_4:def4

      mode thin of P -> Subset of Omega means

      : Def4: ex A be set st A in Sigma & it c= A & (P . A) = 0 ;

      existence

      proof

        reconsider B = {} as Subset of Omega by XBOOLE_1: 2;

        take B;

        take A = {} ;

        thus A in Sigma by PROB_1: 4;

        thus B c= A;

        thus thesis by VALUED_0:def 19;

      end;

    end

    theorem :: PROB_4:23

    

     Th23: for Y be Subset of Omega holds Y is thin of P iff Y is thin of ( P2M P)

    proof

      let Y be Subset of Omega;

      hereby

        assume Y is thin of P;

        then ex A be set st A in Sigma & Y c= A & (P . A) = 0 by Def4;

        hence Y is thin of ( P2M P) by MEASURE3:def 2;

      end;

      assume Y is thin of ( P2M P);

      then ex B be set st B in Sigma & Y c= B & (( P2M P) . B) = 0. by MEASURE3:def 2;

      hence thesis by Def4;

    end;

    theorem :: PROB_4:24

    

     Th24: {} is thin of P

    proof

      (P . {} ) = 0 & {} in Sigma by PROB_1: 4, VALUED_0:def 19;

      hence thesis by Def4;

    end;

    theorem :: PROB_4:25

    

     Th25: for B1,B2 be set st B1 in Sigma & B2 in Sigma holds for C1,C2 be thin of P holds (B1 \/ C1) = (B2 \/ C2) implies (P . B1) = (P . B2)

    proof

      let B1,B2 be set;

      assume

       A1: B1 in Sigma & B2 in Sigma;

      let C1,C2 be thin of P;

      assume

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

      then

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

      

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

      consider D1 be set such that

       A5: D1 in Sigma and

       A6: C1 c= D1 and

       A7: (P . D1) = 0 by Def4;

      

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

      consider D2 be set such that

       A9: D2 in Sigma and

       A10: C2 c= D2 and

       A11: (P . D2) = 0 by Def4;

      

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

      reconsider B1, B2, D1, D2 as Event of Sigma by A1, A5, A9;

      

       A13: (P . (B1 \/ D1)) <= ((P . B1) + (P . D1)) by PROB_1: 39;

      (P . B2) <= (P . (B1 \/ D1)) by A4, A8, PROB_1: 34, XBOOLE_1: 1;

      then

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

      

       A15: (P . (B2 \/ D2)) <= ((P . B2) + (P . D2)) by PROB_1: 39;

      (P . B1) <= (P . (B2 \/ D2)) by A3, A12, PROB_1: 34, XBOOLE_1: 1;

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

      hence thesis by A14, XXREAL_0: 1;

    end;

    definition

      let Omega, Sigma, P;

      :: PROB_4:def5

      func COM (Sigma,P) -> non empty Subset-Family of Omega means

      : Def5: for A be set holds A in it iff ex B be set st B in Sigma & ex C be thin of P st A = (B \/ C);

      existence

      proof

        

         A1: {} is thin of P by Th24;

        

         A2: for A be set st A = {} holds ex B be set st B in Sigma & ex C be thin of P st A = (B \/ C)

        proof

          let A be set;

          consider B be set such that

           A3: B = {} and

           A4: B in Sigma by PROB_1: 4;

          consider C be thin of P such that

           A5: C = {} by A1;

          assume A = {} ;

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

          hence thesis by A4;

        end;

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

        consider D be set such that

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

        

         A7: for A be set holds (A in D iff ex B be set st (B in Sigma & ex C be thin of P st A = (B \/ C)))

        proof

          let A be set;

          

           A8: A in D iff (A in ( bool Omega) & for y be set holds (y = A implies ex B be set st (B in Sigma & ex C be thin of P st y = (B \/ C)))) by A6;

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

          proof

            assume

             A9: ex B be set st (B in Sigma & ex C be thin of P st A = (B \/ C));

            then A c= Omega by XBOOLE_1: 8;

            hence thesis by A8, A9;

          end;

          hence thesis by A6;

        end;

        

         A10: D c= ( bool Omega) by A6;

         {} c= Omega;

        then

        reconsider D as non empty Subset-Family of Omega by A6, A10, A2;

        take D;

        thus thesis by A7;

      end;

      uniqueness

      proof

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

         A11: for A be set holds (A in D1 iff ex B be set st (B in Sigma & ex C be thin of P st A = (B \/ C))) and

         A12: for A be set holds (A in D2 iff ex B be set st (B in Sigma & ex C be thin of P st A = (B \/ C)));

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

        proof

          let A be object;

          thus A in D1 implies A in D2

          proof

            assume A in D1;

            then ex B be set st (B in Sigma & ex C be thin of P st A = (B \/ C)) by A11;

            hence thesis by A12;

          end;

          assume A in D2;

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

          hence thesis by A11;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    theorem :: PROB_4:26

    

     Th26: for C be thin of P holds C in ( COM (Sigma,P))

    proof

      let C be thin of P;

      reconsider B = {} as Element of Sigma by PROB_1: 4;

      (B \/ C) in ( COM (Sigma,P)) by Def5;

      hence thesis;

    end;

    theorem :: PROB_4:27

    

     Th27: ( COM (Sigma,P)) = ( COM (Sigma,( P2M P)))

    proof

      

       A1: ( COM (Sigma,( P2M P))) c= ( COM (Sigma,P))

      proof

        let x be object;

        assume x in ( COM (Sigma,( P2M P)));

        then

        consider B be set such that

         A2: B in Sigma and

         A3: ex C be thin of ( P2M P) st x = (B \/ C) by MEASURE3:def 3;

        consider C be thin of ( P2M P) such that

         A4: x = (B \/ C) by A3;

        reconsider C1 = C as thin of P by Th23;

        x = (B \/ C1) by A4;

        hence thesis by A2, Def5;

      end;

      ( COM (Sigma,P)) c= ( COM (Sigma,( P2M P)))

      proof

        let x be object;

        assume x in ( COM (Sigma,P));

        then

        consider B be set such that

         A5: B in Sigma and

         A6: ex C be thin of P st x = (B \/ C) by Def5;

        consider C be thin of P such that

         A7: x = (B \/ C) by A6;

        reconsider C1 = C as thin of ( P2M P) by Th23;

        x = (B \/ C1) by A7;

        hence thesis by A5, MEASURE3:def 3;

      end;

      hence thesis by A1;

    end;

    definition

      let Omega, Sigma, P;

      let A be Element of ( COM (Sigma,P));

      :: PROB_4:def6

      func P_COM2M_COM (A) -> Element of ( COM (Sigma,( P2M P))) equals A;

      correctness by Th27;

    end

    theorem :: PROB_4:28

    

     Th28: Sigma c= ( COM (Sigma,P))

    proof

      reconsider C = {} as thin of P by Th24;

      let A be object such that

       A1: A in Sigma;

      reconsider AA = A as set by TARSKI: 1;

      A = (AA \/ C);

      hence thesis by A1, Def5;

    end;

    definition

      let Omega, Sigma, P;

      let A be Element of ( COM (Sigma,P));

      :: PROB_4:def7

      func ProbPart (A) -> non empty Subset-Family of Omega means

      : Def7: for B be set holds (B in it iff B in Sigma & B c= A & (A \ B) is thin of P);

      existence

      proof

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

        consider D be set such that

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

        

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

        proof

          let B be set;

          B in Sigma & B c= A & (A \ B) is thin of P implies B in D

          proof

            assume that

             A3: B in Sigma and

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

            for t be set holds t = B implies t in Sigma & t c= A & (A \ t) is thin of P by A3, A4;

            hence thesis by A1, A3;

          end;

          hence thesis by A1;

        end;

        

         A5: D c= ( bool Omega)

        proof

          let B be object;

          assume B in D;

          then B in Sigma by A2;

          hence thesis;

        end;

        D <> {}

        proof

          consider B be set such that

           A6: B in Sigma and

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

          consider C be thin of P such that

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

          consider E be set such that

           A9: E in Sigma and

           A10: C c= E and

           A11: (P . E) = 0 by Def4;

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

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

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

          then

           A12: (A \ B) is thin of P by A9, A11, Def4;

          B c= A by A8, XBOOLE_1: 7;

          hence thesis by A2, A6, A12;

        end;

        then

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

        take D;

        thus thesis by A2;

      end;

      uniqueness

      proof

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

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

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

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

        proof

          let B be object;

          reconsider BB = B as set by TARSKI: 1;

          thus B in D1 implies B in D2

          proof

            assume

             A15: B in D1;

            then

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

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

            hence thesis by A14, A16;

          end;

          assume

           A17: B in D2;

          then

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

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

          hence thesis by A13, A18;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    theorem :: PROB_4:29

    for A be Element of ( COM (Sigma,P)) holds ( ProbPart A) = ( MeasPart ( P_COM2M_COM A))

    proof

      let A be Element of ( COM (Sigma,P));

      

       A1: ( MeasPart ( P_COM2M_COM A)) c= ( ProbPart A)

      proof

        let x be object such that

         A2: x in ( MeasPart ( P_COM2M_COM A));

        reconsider xx = x as set by TARSKI: 1;

        (( P_COM2M_COM A) \ xx) is thin of ( P2M P) by A2, MEASURE3:def 4;

        then

         A3: (A \ xx) is thin of P by Th23;

        x in Sigma & xx c= ( P_COM2M_COM A) by A2, MEASURE3:def 4;

        hence thesis by A3, Def7;

      end;

      ( ProbPart A) c= ( MeasPart ( P_COM2M_COM A))

      proof

        let x be object such that

         A4: x in ( ProbPart A);

        reconsider xx = x as set by TARSKI: 1;

        (A \ xx) is thin of P by A4, Def7;

        then

         A5: (( P_COM2M_COM A) \ xx) is thin of ( P2M P) by Th23;

        x in Sigma & xx c= A by A4, Def7;

        hence thesis by A5, MEASURE3:def 4;

      end;

      hence thesis by A1;

    end;

    theorem :: PROB_4:30

    for A be Element of ( COM (Sigma,P)) holds for A1,A2 be set st A1 in ( ProbPart A) & A2 in ( ProbPart A) holds (P . A1) = (P . A2)

    proof

      let A be Element of ( COM (Sigma,P));

      let A1,A2 be set such that

       A1: A1 in ( ProbPart A) and

       A2: A2 in ( ProbPart A);

      reconsider C1 = (A \ A1), C2 = (A \ A2) as thin of P by A1, A2, Def7;

      

       A3: A2 c= A by A2, Def7;

      A1 c= A by A1, Def7;

      

      then

       A4: (A1 \/ C1) = A by XBOOLE_1: 45

      .= (A2 \/ C2) by A3, XBOOLE_1: 45;

      A1 in Sigma & A2 in Sigma by A1, A2, Def7;

      hence thesis by A4, Th25;

    end;

    theorem :: PROB_4:31

    

     Th31: for F be sequence of ( COM (Sigma,P)) holds ex BSeq be SetSequence of Sigma st for n holds (BSeq . n) in ( ProbPart (F . n))

    proof

      let F be sequence of ( COM (Sigma,P));

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

      

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

      proof

        let t be Element of NAT ;

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

        reconsider A as Element of Sigma by Def7;

        take A;

        thus thesis;

      end;

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

      then

      consider G be sequence of Sigma such that

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

      reconsider BSeq = G as SetSequence of Omega by FUNCT_2: 7;

      reconsider BSeq as SetSequence of Sigma;

      take BSeq;

      thus thesis by A2;

    end;

    theorem :: PROB_4:32

    

     Th32: for F be sequence of ( COM (Sigma,P)), BSeq be SetSequence of Sigma holds ex CSeq be SetSequence of Omega st for n holds (CSeq . n) = ((F . n) \ (BSeq . n))

    proof

      let F be sequence of ( COM (Sigma,P)), G be SetSequence of Sigma;

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

      

       A1: for t be Element of NAT holds ex A be Element of ( bool Omega) st P[t, A]

      proof

        let t be Element of NAT ;

        (F . t) is Element of ( COM (Sigma,P));

        then

        reconsider A = ((F . t) \ (G . t)) as Element of ( bool Omega) by XBOOLE_1: 1;

        take A;

        thus thesis;

      end;

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

      then

      consider H be sequence of ( bool Omega) such that

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

      take H;

      thus thesis by A2;

    end;

    theorem :: PROB_4:33

    

     Th33: for BSeq be SetSequence of Omega st (for n holds (BSeq . n) is thin of P) holds ex CSeq be SetSequence of Sigma st for n holds (BSeq . n) c= (CSeq . n) & (P . (CSeq . n)) = 0

    proof

      let BSeq be SetSequence of Omega;

      defpred P[ Element of NAT , set] means for n be Element of NAT holds for y be set holds (n = $1 & y = $2 implies y in Sigma & (BSeq . n) c= y & (P . y) = 0 );

      assume

       A1: for n holds (BSeq . n) is thin of P;

      

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

      proof

        let t be Element of NAT ;

        (BSeq . t) is thin of P by A1;

        then

        consider A be set such that

         A3: A in Sigma and

         A4: (BSeq . t) c= A & (P . A) = 0 by Def4;

        reconsider A as Element of Sigma by A3;

        take A;

        thus thesis by A4;

      end;

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

      then

      consider G be sequence of Sigma such that

       A5: for t be Element of NAT holds for n be Element of NAT holds for y be set holds (n = t & y = (G . t) implies y in Sigma & (BSeq . n) c= y & (P . y) = 0 );

      reconsider CSeq = G as SetSequence of Omega by FUNCT_2: 7;

      reconsider CSeq as SetSequence of Sigma;

      take CSeq;

      thus thesis by A5;

    end;

    theorem :: PROB_4:34

    

     Th34: for D be non empty Subset-Family of Omega holds (for A be set holds (A in D iff ex B be set st B in Sigma & ex C be thin of P st A = (B \/ C))) implies D is SigmaField of Omega

    proof

      let D be non empty Subset-Family of Omega;

      assume

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

      

       A2: for A1 be SetSequence of Omega st ( rng A1) c= D holds ( Union A1) in D

      proof

        let A1 be SetSequence of Omega;

        reconsider F = A1 as sequence of ( bool Omega);

        

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

        assume

         A4: ( rng A1) c= D;

        

         A5: for n holds ex B be set st B in Sigma & ex C be thin of P st (F . n) = (B \/ C)

        proof

          let n;

          (F . n) in ( rng F) by NAT_1: 51;

          hence thesis by A1, A4;

        end;

        for n holds (F . n) in ( COM (Sigma,P))

        proof

          let n;

          ex B be set st (B in Sigma & ex C be thin of P st (F . n) = (B \/ C)) by A5;

          hence thesis by Def5;

        end;

        then for n be object st n in NAT holds (F . n) in ( COM (Sigma,P));

        then

        reconsider F as sequence of ( COM (Sigma,P)) by A3, FUNCT_2: 3;

        consider BSeq be SetSequence of Sigma such that

         A6: for n holds (BSeq . n) in ( ProbPart (F . n)) by Th31;

        consider CSeq be SetSequence of Omega such that

         A7: for n holds (CSeq . n) = ((F . n) \ (BSeq . n)) by Th32;

        

         A8: for n be Element of NAT holds (BSeq . n) in Sigma & (BSeq . n) c= (F . n) & ((F . n) \ (BSeq . n)) is thin of P

        proof

          let n be Element of NAT ;

          (BSeq . n) in ( ProbPart (F . n)) by A6;

          hence thesis by Def7;

        end;

        for n holds (CSeq . n) is thin of P

        proof

          let n be Element of NAT ;

          ((F . n) \ (BSeq . n)) is thin of P by A8;

          hence thesis by A7;

        end;

        then

        consider DSeq be SetSequence of Sigma such that

         A9: for n holds (CSeq . n) c= (DSeq . n) & (P . (DSeq . n)) = 0 by Th33;

        

         A10: ( Union A1) = ( union ( rng A1)) by CARD_3:def 4;

        ex B be set st B in Sigma & ex C be thin of P st ( Union A1) = (B \/ C)

        proof

          set B = ( union ( rng BSeq));

          take B;

          

           A11: ( union ( rng BSeq)) c= ( union ( rng F))

          proof

            let x be object;

            assume x in ( union ( rng BSeq));

            then

            consider Z be set such that

             A12: x in Z and

             A13: Z in ( rng BSeq) by TARSKI:def 4;

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

            then

            consider n be object such that

             A14: n in NAT and

             A15: Z = (BSeq . n) by A13, FUNCT_1:def 3;

            reconsider n as Element of NAT by A14;

            set P = (F . n);

            

             A16: (BSeq . n) c= P by A8;

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

            proof

              take P;

              thus thesis by A3, A12, A15, A16, FUNCT_1:def 3;

            end;

            hence thesis by TARSKI:def 4;

          end;

          

           A17: ex C be thin of P st ( Union A1) = (B \/ C)

          proof

            set C = (( Union A1) \ B);

            ( Union DSeq) in Sigma by PROB_1: 17;

            then

             A18: ( union ( rng DSeq)) in Sigma by CARD_3:def 4;

            

             A19: C c= ( union ( rng CSeq))

            proof

              let x be object;

              assume

               A20: x in C;

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

              then

              consider Z be set such that

               A21: x in Z and

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

              consider n be object such that

               A23: n in NAT and

               A24: Z = (F . n) by A3, A22, FUNCT_1:def 3;

              reconsider n as Element of NAT by A23;

              

               A25: not x in ( union ( rng BSeq)) by A20, XBOOLE_0:def 5;

               not x in (BSeq . n)

              proof

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

                then

                 A26: (BSeq . n) in ( rng BSeq) by FUNCT_1:def 3;

                assume x in (BSeq . n);

                hence thesis by A25, A26, TARSKI:def 4;

              end;

              then

               A27: x in ((F . n) \ (BSeq . n)) by A21, A24, XBOOLE_0:def 5;

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

              proof

                take (CSeq . n);

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

                hence thesis by A7, A27, FUNCT_1:def 3;

              end;

              hence thesis by TARSKI:def 4;

            end;

            for A be set holds A in ( rng DSeq) implies (P . A) = 0

            proof

              let A be set;

              

               A28: ( dom DSeq) = NAT by FUNCT_2:def 1;

              assume A in ( rng DSeq);

              then ex n be object st n in NAT & A = (DSeq . n) by A28, FUNCT_1:def 3;

              hence thesis by A9;

            end;

            then

             A29: (P . ( union ( rng DSeq))) = 0 by Th8;

            ( union ( rng CSeq)) c= ( union ( rng DSeq))

            proof

              let x be object;

              assume x in ( union ( rng CSeq));

              then

              consider Z be set such that

               A30: x in Z and

               A31: Z in ( rng CSeq) by TARSKI:def 4;

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

              then

              consider n be object such that

               A32: n in NAT and

               A33: Z = (CSeq . n) by A31, FUNCT_1:def 3;

              reconsider n as Element of NAT by A32;

              n in ( dom DSeq) by A32, FUNCT_2:def 1;

              then

               A34: (DSeq . n) in ( rng DSeq) by FUNCT_1:def 3;

              (CSeq . n) c= (DSeq . n) by A9;

              hence thesis by A30, A33, A34, TARSKI:def 4;

            end;

            then C c= ( union ( rng DSeq)) by A19;

            then

             A35: C is thin of P by A29, A18, Def4;

            ( Union A1) = (C \/ (( union ( rng F)) /\ ( union ( rng BSeq)))) by A10, XBOOLE_1: 51

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

            then

            consider C be thin of P such that

             A36: ( Union A1) = (B \/ C) by A35;

            take C;

            thus thesis by A36;

          end;

          ( Union BSeq) in Sigma by PROB_1: 17;

          hence thesis by A17, CARD_3:def 4;

        end;

        hence thesis by A1;

      end;

      for A be Subset of Omega holds A in D implies (A ` ) in D

      proof

        let A be Subset of Omega;

        assume

         A37: A in D;

        ex Q be set st Q in Sigma & ex W be thin of P st (Omega \ A) = (Q \/ W)

        proof

          consider B be set such that

           A38: B in Sigma and

           A39: ex C be thin of P st A = (B \/ C) by A1, A37;

          consider C be thin of P such that

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

          reconsider B as Subset of Omega by A38;

          set H = (Omega \ B);

          consider G be set such that

           A41: G in Sigma and

           A42: C c= G and

           A43: (P . G) = 0 by Def4;

          set Q = (H \ G);

          

           A44: (Omega \ A) = (H \ C) by A40, XBOOLE_1: 41;

          

           A45: ex W be thin of P st (Omega \ A) = (Q \/ W)

          proof

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

            W c= H by XBOOLE_1: 17;

            then

            reconsider W as Subset of Omega by XBOOLE_1: 1;

            reconsider W as thin of P by A41, A43, Def4;

            take W;

            thus thesis by A42, A44, Lm1;

          end;

          take Q;

          (B ` ) in Sigma by A38, PROB_1:def 1;

          hence thesis by A41, A45, PROB_1: 6;

        end;

        hence thesis by A1;

      end;

      hence thesis by A2, Th4;

    end;

    registration

      let Omega, Sigma, P;

      cluster ( COM (Sigma,P)) -> compl-closed sigma-multiplicative;

      coherence

      proof

        for A be set holds (A in ( COM (Sigma,P)) iff ex B be set st B in Sigma & ex C be thin of P st A = (B \/ C)) by Def5;

        hence thesis by Th34;

      end;

    end

    definition

      let Omega, Sigma, P;

      :: original: thin

      redefine

      mode thin of P -> Event of ( COM (Sigma,P)) ;

      coherence by Th26;

    end

    theorem :: PROB_4:35

    

     Th35: for A be set holds (A in ( COM (Sigma,P)) iff ex A1,A2 be set st A1 in Sigma & A2 in Sigma & A1 c= A & A c= A2 & (P . (A2 \ A1)) = 0 )

    proof

      let A be set;

      thus A in ( COM (Sigma,P)) implies ex A1,A2 be set st A1 in Sigma & A2 in Sigma & A1 c= A & A c= A2 & (P . (A2 \ A1)) = 0

      proof

        assume A in ( COM (Sigma,P));

        then

        consider B be set such that

         A1: B in Sigma and

         A2: ex C be thin of P st A = (B \/ C) by Def5;

        consider C be thin of P such that

         A3: A = (B \/ C) by A2;

        reconsider B as Event of Sigma by A1;

        consider D be set such that

         A4: D in Sigma and

         A5: C c= D and

         A6: (P . D) = 0 by Def4;

        reconsider D as Event of Sigma by A4;

        reconsider E = (D \/ B) as Event of Sigma;

        

         A7: (P . (D \/ B)) <= ((P . D) + (P . B)) by PROB_1: 39;

        (P . (E \ B)) = (P . (D \ B)) by XBOOLE_1: 40

        .= ((P . (D \/ B)) - (P . B)) by Th5;

        then (P . (E \ B)) <= 0 by A6, A7, XREAL_1: 47;

        then

         A8: (P . (E \ B)) = 0 by PROB_1:def 8;

        A c= E by A3, A5, XBOOLE_1: 9;

        hence thesis by A2, A8, XBOOLE_1: 7;

      end;

      thus (ex A1,A2 be set st A1 in Sigma & A2 in Sigma & A1 c= A & A c= A2 & (P . (A2 \ A1)) = 0 ) implies A in ( COM (Sigma,P))

      proof

        given A1,A2 be set such that

         A9: A1 in Sigma and

         A10: A2 in Sigma and

         A11: A1 c= A and

         A12: A c= A2 and

         A13: (P . (A2 \ A1)) = 0 ;

        reconsider A2 as Element of Sigma by A10;

        reconsider A1 as Element of Sigma by A9;

        set C = (A \ A1);

        

         A14: C is thin of P

        proof

          reconsider D = (A2 \ A1) as Element of Sigma;

          

           A15: C c= D

          proof

            let x be object;

            assume x in C;

            then x in A & not x in A1 by XBOOLE_0:def 5;

            hence thesis by A12, XBOOLE_0:def 5;

          end;

          then C c= Omega by XBOOLE_1: 1;

          hence thesis by A13, A15, Def4;

        end;

        A = (A1 \/ C) by A11, XBOOLE_1: 45;

        hence thesis by A14, Def5;

      end;

    end;

    theorem :: PROB_4:36

    for C be non empty Subset-Family of Omega holds (for A be set holds (A in C iff ex A1,A2 be set st A1 in Sigma & A2 in Sigma & A1 c= A & A c= A2 & (P . (A2 \ A1)) = 0 )) implies C = ( COM (Sigma,P))

    proof

      let C be non empty Subset-Family of Omega;

      assume

       A1: for A be set holds (A in C iff ex A1,A2 be set st A1 in Sigma & A2 in Sigma & A1 c= A & A c= A2 & (P . (A2 \ A1)) = 0 );

      now

        let A be object;

        reconsider AA = A as set by TARSKI: 1;

        A in C iff ex A1,A2 be set st A1 in Sigma & A2 in Sigma & A1 c= AA & AA c= A2 & (P . (A2 \ A1)) = 0 by A1;

        hence A in C iff A in ( COM (Sigma,P)) by Th35;

      end;

      hence thesis by TARSKI: 2;

    end;

    definition

      let Omega, Sigma, P;

      :: PROB_4:def8

      func COM (P) -> Probability of ( COM (Sigma,P)) means

      : Def8: for B be set st B in Sigma holds for C be thin of P holds (it . (B \/ C)) = (P . B);

      existence

      proof

        reconsider C = {} as thin of P by Th24;

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

        set B = {} ;

        

         A1: {} is thin of P by Th24;

        

         A2: for x be object st x in ( COM (Sigma,P)) holds ex y be object st y in REAL & P[x, y]

        proof

          let x be object;

          assume x in ( COM (Sigma,P));

          then

          consider B be set such that

           A3: B in Sigma & ex C be thin of P st x = (B \/ C) by Def5;

          take (P . B);

          thus thesis by A3, Th25, FUNCT_2: 5;

        end;

        consider comP be Function of ( COM (Sigma,P)), REAL such that

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

        

         A5: for B be set st B in Sigma holds for C be thin of P holds (comP . (B \/ C)) = (P . B)

        proof

          let B be set;

          assume

           A6: B in Sigma;

          let C be thin of P;

          (B \/ C) in ( COM (Sigma,P)) by A6, Def5;

          hence thesis by A4, A6;

        end;

        

         A7: for BSeq be SetSequence of ( COM (Sigma,P)) st BSeq is disjoint_valued holds ( Sum (comP * BSeq)) = (comP . ( Union BSeq))

        proof

          let BSeq be SetSequence of ( COM (Sigma,P)) such that

           A8: BSeq is disjoint_valued;

          reconsider F = BSeq as sequence of ( bool Omega);

          ( rng F) c= ( COM (Sigma,P)) by RELAT_1:def 19;

          then

          reconsider F as sequence of ( COM (Sigma,P)) by FUNCT_2: 6;

          consider CSeq be SetSequence of Sigma such that

           A9: for n holds (CSeq . n) in ( ProbPart (F . n)) by Th31;

          consider B be set such that

           A10: B = ( union ( rng CSeq));

          ( Union CSeq) in Sigma by PROB_1: 17;

          then

          reconsider B as Element of Sigma by A10, CARD_3:def 4;

          consider DSeq be SetSequence of Omega such that

           A11: for n holds (DSeq . n) = ((F . n) \ (CSeq . n)) by Th32;

          

           A12: for n be Element of NAT holds (CSeq . n) in Sigma & (CSeq . n) c= (F . n) & ((F . n) \ (CSeq . n)) is thin of P

          proof

            let n be Element of NAT ;

            (CSeq . n) in ( ProbPart (F . n)) by A9;

            hence thesis by Def7;

          end;

          for n be Element of NAT holds (DSeq . n) is thin of P

          proof

            let n be Element of NAT ;

            ((F . n) \ (CSeq . n)) is thin of P by A12;

            hence thesis by A11;

          end;

          then

          consider ESeq be SetSequence of Sigma such that

           A13: for n holds (DSeq . n) c= (ESeq . n) & (P . (ESeq . n)) = 0 by Th33;

          

           A14: ( dom BSeq) = NAT by FUNCT_2:def 1;

          

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

          proof

            let x be object;

            assume x in B;

            then

            consider Z be set such that

             A16: x in Z and

             A17: Z in ( rng CSeq) by A10, TARSKI:def 4;

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

            then

            consider n be object such that

             A18: n in NAT and

             A19: Z = (CSeq . n) by A17, FUNCT_1:def 3;

            reconsider n as Element of NAT by A18;

            set P = (F . n);

            

             A20: (CSeq . n) c= P by A12;

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

            proof

              take P;

              thus thesis by A14, A16, A19, A20, FUNCT_1:def 3;

            end;

            hence thesis by TARSKI:def 4;

          end;

          

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

          proof

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

            

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

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

            reconsider C as Subset of Omega;

            

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

            proof

              let x be object;

              assume

               A24: x in C;

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

              then

              consider Z be set such that

               A25: x in Z and

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

              consider n be object such that

               A27: n in NAT and

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

              reconsider n as Element of NAT by A27;

              

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

               not x in (CSeq . n)

              proof

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

                then

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

                assume x in (CSeq . n);

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

              end;

              then

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

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

              proof

                take (DSeq . n);

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

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

              end;

              hence thesis by TARSKI:def 4;

            end;

            for A be set holds A in ( rng ESeq) implies (P . A) = 0

            proof

              let A be set;

              

               A32: ( dom ESeq) = NAT by FUNCT_2:def 1;

              assume A in ( rng ESeq);

              then ex n be object st n in NAT & A = (ESeq . n) by A32, FUNCT_1:def 3;

              hence thesis by A13;

            end;

            then

             A33: (P . ( union ( rng ESeq))) = 0 by Th8;

            ( Union ESeq) in Sigma by PROB_1: 17;

            then

             A34: ( union ( rng ESeq)) in Sigma by CARD_3:def 4;

            ( union ( rng DSeq)) c= ( union ( rng ESeq))

            proof

              let x be object;

              assume x in ( union ( rng DSeq));

              then

              consider Z be set such that

               A35: x in Z and

               A36: Z in ( rng DSeq) by TARSKI:def 4;

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

              then

              consider n be object such that

               A37: n in NAT and

               A38: Z = (DSeq . n) by A36, FUNCT_1:def 3;

              reconsider n as Element of NAT by A37;

              n in ( dom ESeq) by A37, FUNCT_2:def 1;

              then

               A39: (ESeq . n) in ( rng ESeq) by FUNCT_1:def 3;

              (DSeq . n) c= (ESeq . n) by A13;

              hence thesis by A35, A38, A39, TARSKI:def 4;

            end;

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

            then C is thin of P by A34, A33, Def4;

            then

            consider C be thin of P such that

             A40: ( union ( rng F)) = (B \/ C) by A22;

            take C;

            thus thesis by A40;

          end;

          for n,m be object st n <> m holds (CSeq . n) misses (CSeq . m)

          proof

            let n,m be object;

            

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

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

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

            proof

              let n be object;

              per cases ;

                suppose n in ( dom F);

                hence thesis by A12;

              end;

                suppose

                 A42: not n in ( dom F);

                

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

                .= (CSeq . n) by A41, A42, FUNCT_1:def 2;

                hence thesis;

              end;

            end;

            then

             A43: (CSeq . n) c= (F . n) & (CSeq . m) c= (F . m);

            assume n <> m;

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

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

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

            hence thesis;

          end;

          then

           A44: CSeq is disjoint_valued;

          ( Sum (comP * F)) = (comP . ( Union F))

          proof

            

             A45: for n holds (comP . (F . n)) = (P . (CSeq . n))

            proof

              let n;

              ((F . n) \ (CSeq . n)) is thin of P by A12;

              then

              consider C be thin of P such that

               A46: C = ((F . n) \ (CSeq . n));

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

              .= ((CSeq . n) \/ C) by A12, A46, XBOOLE_1: 28;

              hence thesis by A5;

            end;

            for x be Element of NAT holds ((comP * F) . x) = ((P * CSeq) . x)

            proof

              let x be Element of NAT ;

              ((comP * F) . x) = (comP . (F . x)) by FUNCT_2: 15

              .= (P . (CSeq . x)) by A45

              .= ((P * CSeq) . x) by FUNCT_2: 15;

              hence thesis;

            end;

            then

             A47: ( Sum (comP * F)) = ( Sum (P * CSeq)) by FUNCT_2: 63;

            (comP . ( union ( rng F))) = (P . ( union ( rng CSeq))) by A5, A10, A21;

            

            then (comP . ( Union F)) = (P . ( union ( rng CSeq))) by CARD_3:def 4

            .= (P . ( Union CSeq)) by CARD_3:def 4;

            hence thesis by A44, A47, PROB_3: 46;

          end;

          hence thesis;

        end;

        

         A48: for x be Element of ( COM (Sigma,P)) holds (comP . x) >= 0

        proof

          let x be Element of ( COM (Sigma,P));

          consider B be set such that

           A49: B in Sigma and

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

          reconsider B as Element of Sigma by A49;

          (comP . x) = (P . B) by A4, A50;

          hence thesis by PROB_1:def 8;

        end;

         {} = (B \/ C);

        

        then

         A51: (comP . {} ) = (P . {} ) by A5, PROB_1: 4

        .= 0 by VALUED_0:def 19;

        

         A52: for A,B be Event of ( COM (Sigma,P)) st A misses B holds (comP . (A \/ B)) = ((comP . A) + (comP . B))

        proof

          let A,B be Event of ( COM (Sigma,P)) such that

           A53: A misses B;

          reconsider A1 = A, B1 = B as Subset of Omega;

          reconsider BSeq = ((A1,B1) followed_by ( {} Omega)) as SetSequence of Omega;

          

           A54: (BSeq . 1) = B by FUNCT_7: 123;

          

           A55: (BSeq . 0 ) = A by FUNCT_7: 122;

          for n be Nat holds (BSeq . n) in ( COM (Sigma,P))

          proof

            let n be Nat;

            per cases ;

              suppose n = 0 ;

              hence thesis by A55;

            end;

              suppose n <> 0 ;

              then n >= 1 by NAT_1: 14;

              then

               A56: (n + 1) > 1 by NAT_1: 13;

              per cases by A56, NAT_1: 22;

                suppose n > 1;

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

                hence thesis by PROB_1: 4;

              end;

                suppose n = 1;

                hence thesis by A54;

              end;

            end;

          end;

          then ( rng BSeq) c= ( COM (Sigma,P)) by NAT_1: 52;

          then

          reconsider BSeq as SetSequence of ( COM (Sigma,P)) by RELAT_1:def 19;

          for m be Nat st 2 <= m holds (( Partial_Sums (comP * BSeq)) . m) = ((comP . A) + (comP . B))

          proof

            

             A57: (( Partial_Sums (comP * BSeq)) . 0 ) = ((comP * BSeq) . 0 ) by SERIES_1:def 1

            .= (comP . A) by A55, FUNCT_2: 15;

            ( 0 + 1) = 1;

            

            then

             A58: (( Partial_Sums (comP * BSeq)) . 1) = ((( Partial_Sums (comP * BSeq)) . 0 ) + ((comP * BSeq) . 1)) by SERIES_1:def 1

            .= ((comP . A) + (comP . B)) by A54, A57, FUNCT_2: 15;

            

             A59: for n be Nat holds (( Partial_Sums (comP * BSeq)) . (2 + n)) = ((comP . A) + (comP . B))

            proof

              defpred P[ Nat] means (( Partial_Sums (comP * BSeq)) . (2 + $1)) = ((comP . A) + (comP . B));

              

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

              proof

                let k be Nat such that

                 A61: P[k];

                

                 A62: ((2 + k) + 1) > ( 0 + 1) by XREAL_1: 8;

                

                thus (( Partial_Sums (comP * BSeq)) . (2 + (k + 1))) = ((( Partial_Sums (comP * BSeq)) . (2 + k)) + ((comP * BSeq) . ((2 + k) + 1))) by SERIES_1:def 1

                .= (((comP . A) + (comP . B)) + (comP . (BSeq . ((2 + k) + 1)))) by A61, FUNCT_2: 15

                .= (((comP . A) + (comP . B)) + (comP . {} )) by A62, FUNCT_7: 124

                .= ((comP . A) + (comP . B)) by A51;

              end;

              2 = (1 + 1);

              

              then (( Partial_Sums (comP * BSeq)) . (2 + 0 )) = ((( Partial_Sums (comP * BSeq)) . 1) + ((comP * BSeq) . 2)) by SERIES_1:def 1

              .= (((comP . A) + (comP . B)) + (comP . (BSeq . 2))) by A58, FUNCT_2: 15

              .= (((comP . A) + (comP . B)) + (comP . {} )) by FUNCT_7: 124

              .= ((comP . A) + (comP . B)) by A51;

              then

               A63: P[ 0 ];

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

            end;

            let m be Nat;

            assume 2 <= m;

            then

            consider k be Nat such that

             A64: m = (2 + k) by NAT_1: 10;

            thus thesis by A59, A64;

          end;

          then

           A65: ( Union BSeq) = (A \/ B) & ( Sum (comP * BSeq)) = ((comP . A) + (comP . B)) by DYNKIN: 3, PROB_1: 1;

          BSeq is disjoint_valued by A53, Th3;

          hence thesis by A7, A65;

        end;

        

         A66: for A,B be Event of ( COM (Sigma,P)) st A c= B holds (comP . (B \ A)) = ((comP . B) - (comP . A))

        proof

          let A,B be Event of ( COM (Sigma,P));

          assume

           A67: A c= B;

          ((comP . A) + (comP . (B \ A))) = (comP . (A \/ (B \ A))) by A52, XBOOLE_1: 79

          .= (comP . B) by A67, XBOOLE_1: 45;

          hence thesis;

        end;

        

         A68: for A,B be Event of ( COM (Sigma,P)) st A c= B holds (comP . A) <= (comP . B)

        proof

          let A,B be Event of ( COM (Sigma,P));

          assume A c= B;

          then (comP . (B \ A)) = ((comP . B) - (comP . A)) by A66;

          then 0 <= ((comP . B) - (comP . A)) by A48;

          then ( 0 + (comP . A)) <= (comP . B) by XREAL_1: 19;

          hence thesis;

        end;

        

         A69: for BSeq be SetSequence of ( COM (Sigma,P)) st BSeq is non-descending holds (comP * BSeq) is non-decreasing

        proof

          let BSeq be SetSequence of ( COM (Sigma,P)) such that

           A70: BSeq is non-descending;

          for n,m be Nat st n <= m holds ((comP * BSeq) . n) <= ((comP * BSeq) . m)

          proof

            let n,m be Nat;

            

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

            assume n <= m;

            then (BSeq . n) c= (BSeq . m) by A70, PROB_1:def 5;

            then (comP . (BSeq . n)) <= (comP . (BSeq . m)) by A68;

            then ((comP * BSeq) . n) <= (comP . (BSeq . m)) by FUNCT_2: 15, A71;

            hence thesis by FUNCT_2: 15, A71;

          end;

          hence thesis by SEQM_3: 6;

        end;

        

         A72: (comP . Omega) = (comP . (B \/ Omega))

        .= (P . Omega) by A5, A1, PROB_1: 5

        .= 1 by PROB_1:def 8;

        

         A73: for A be Event of ( COM (Sigma,P)) holds (comP . A) <= 1

        proof

          reconsider B = Omega as Event of ( COM (Sigma,P)) by PROB_1: 23;

          let A be Event of ( COM (Sigma,P));

          (comP . A) <= (comP . B) by A68;

          hence thesis by A72;

        end;

        

         A74: for BSeq be SetSequence of ( COM (Sigma,P)) holds for n holds ((comP * BSeq) . n) <= 1

        proof

          let BSeq be SetSequence of ( COM (Sigma,P));

          let n;

          ((comP * BSeq) . n) = (comP . (BSeq . n)) by FUNCT_2: 15;

          hence thesis by A73;

        end;

        

         A75: for BSeq be SetSequence of ( COM (Sigma,P)) st BSeq is non-descending holds (comP * BSeq) is bounded_above & (comP * BSeq) is convergent

        proof

          let BSeq be SetSequence of ( COM (Sigma,P));

          assume BSeq is non-descending;

          then

           A76: (comP * BSeq) is non-decreasing by A69;

          for n be Nat holds ((comP * BSeq) . n) < 2

          proof

            let n be Nat;

            n in NAT by ORDINAL1:def 12;

            then (((comP * BSeq) . n) + 0 ) < (1 + 1) by A74, XREAL_1: 8;

            hence thesis;

          end;

          hence (comP * BSeq) is bounded_above by SEQ_2:def 3;

          hence thesis by A76;

        end;

        for BSeq be SetSequence of ( COM (Sigma,P)) st BSeq is non-descending holds (comP * BSeq) is convergent & ( lim (comP * BSeq)) = (comP . ( Union BSeq))

        proof

          let BSeq be SetSequence of ( COM (Sigma,P)) such that

           A77: BSeq is non-descending;

          reconsider CSeq = ( Partial_Diff_Union BSeq) as SetSequence of ( COM (Sigma,P));

          

           A78: for n be Nat holds (( Partial_Sums (comP * CSeq)) . n) = ((comP * BSeq) . n)

          proof

            defpred P[ Nat] means (( Partial_Sums (comP * CSeq)) . $1) = ((comP * BSeq) . $1);

            

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

            proof

              let k be Nat such that

               A80: P[k];

              

               A81: (BSeq . k) c= (BSeq . (k + 1)) by A77, PROB_2: 7;

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

              

              thus (( Partial_Sums (comP * CSeq)) . (k + 1)) = (((comP * BSeq) . kk) + ((comP * CSeq) . (k + 1))) by A80, SERIES_1:def 1

              .= ((comP . (BSeq . kk)) + ((comP * CSeq) . (k + 1))) by FUNCT_2: 15

              .= ((comP . (BSeq . k)) + (comP . (CSeq . (k + 1)))) by FUNCT_2: 15

              .= (comP . ((BSeq . k) \/ (CSeq . (k + 1)))) by A52, A77, Th18

              .= (comP . ((BSeq . k) \/ ((BSeq . (k + 1)) \ (BSeq . k)))) by A77, Th16

              .= (comP . ((BSeq . k) \/ (BSeq . (k + 1)))) by XBOOLE_1: 39

              .= (comP . (BSeq . (k + 1))) by A81, XBOOLE_1: 12

              .= ((comP * BSeq) . (k + 1)) by FUNCT_2: 15;

            end;

            (( Partial_Sums (comP * CSeq)) . 0 ) = ((comP * CSeq) . 0 ) by SERIES_1:def 1

            .= (comP . (CSeq . 0 )) by FUNCT_2: 15

            .= (comP . (BSeq . 0 )) by A77, Th16

            .= ((comP * BSeq) . 0 ) by FUNCT_2: 15;

            then

             A82: P[ 0 ];

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

          end;

          

           A83: ( Partial_Sums (comP * CSeq)) = (comP * BSeq) by A78;

          (comP . ( Union BSeq)) = (comP . ( Union CSeq)) by PROB_3: 36

          .= ( Sum (comP * CSeq)) by A7

          .= ( lim ( Partial_Sums (comP * CSeq)));

          hence thesis by A75, A77, A83;

        end;

        then

        reconsider comP as Probability of ( COM (Sigma,P)) by A48, A72, A52, PROB_2: 10;

        take comP;

        thus thesis by A5;

      end;

      uniqueness

      proof

        let P1,P2 be Probability of ( COM (Sigma,P)) such that

         A84: for B be set st B in Sigma holds for C be thin of P holds (P1 . (B \/ C)) = (P . B) and

         A85: for B be set st B in Sigma holds for C be thin of P holds (P2 . (B \/ C)) = (P . B);

        for x be object holds x in ( COM (Sigma,P)) implies (P1 . x) = (P2 . x)

        proof

          let x be object;

          assume x in ( COM (Sigma,P));

          then

          consider B be set such that

           A86: B in Sigma & ex C be thin of P st x = (B \/ C) by Def5;

          (P1 . x) = (P . B) by A84, A86

          .= (P2 . x) by A85, A86;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: PROB_4:37

    ( COM P) = ( COM ( P2M P))

    proof

      set Y = ( COM P);

      ( COM (Sigma,P)) = ( COM (Sigma,( P2M P))) by Th27;

      then

      reconsider Y1 = ( P2M Y) as sigma_Measure of ( COM (Sigma,( P2M P)));

      for B be set st B in Sigma holds for C be thin of ( P2M P) holds (Y1 . (B \/ C)) = (( P2M P) . B)

      proof

        let B be set such that

         A1: B in Sigma;

        let C be thin of ( P2M P);

        reconsider C1 = C as thin of P by Th23;

        (Y . (B \/ C1)) = (P . B) by A1, Def8;

        hence thesis;

      end;

      hence thesis by MEASURE3:def 5;

    end;

    theorem :: PROB_4:38

    ( COM P) is complete

    proof

      for A be Subset of Omega holds for B be set st B in ( COM (Sigma,P)) & A c= B & (( COM P) . B) = 0 holds A in ( COM (Sigma,P))

      proof

        let A be Subset of Omega;

        let B be set;

        assume

         A1: B in ( COM (Sigma,P));

        assume that

         A2: A c= B and

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

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

        proof

          take {} ;

          consider B2 be set such that

           A4: B2 in Sigma and

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

          

           A6: (P . B2) = 0 by A3, A4, A5, Def8;

          consider C2 be thin of P such that

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

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

          consider D2 be set such that

           A8: D2 in Sigma and

           A9: C2 c= D2 and

           A10: (P . D2) = 0 by Def4;

          set O = (B2 \/ D2);

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

          then

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

          ex O be set st O in Sigma & C1 c= O & (P . O) = 0

          proof

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

            take O;

            (P . (B2 \/ D2)) <= ( 0 + 0 ) by A6, A10, PROB_1: 39;

            hence thesis by A11, PROB_1:def 8, XBOOLE_1: 13;

          end;

          then

           A12: C1 is thin of P by Def4;

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

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

          hence thesis by A12, PROB_1: 4;

        end;

        hence thesis by Def5;

      end;

      hence thesis;

    end;

    theorem :: PROB_4:39

    

     Th39: for A be Event of Sigma holds (P . A) = (( COM P) . A)

    proof

      reconsider C = {} as thin of P by Th24;

      let A be Event of Sigma;

      

      thus (P . A) = (( COM P) . (A \/ C)) by Def8

      .= (( COM P) . A);

    end;

    theorem :: PROB_4:40

    

     Th40: for C be thin of P holds (( COM P) . C) = 0

    proof

      let C be thin of P;

      consider A be set such that

       A1: A in Sigma and

       A2: C c= A and

       A3: (P . A) = 0 by Def4;

      reconsider A as Event of Sigma by A1;

      

       A4: (( COM P) . A) = 0 by A3, Th39;

      Sigma c= ( COM (Sigma,P)) by Th28;

      then

      reconsider A as Event of ( COM (Sigma,P));

      (( COM P) . C) <= (( COM P) . A) by A2, PROB_1: 34;

      hence thesis by A4, PROB_1:def 8;

    end;

    theorem :: PROB_4:41

    for A be Element of ( COM (Sigma,P)), B be set st B in ( ProbPart A) holds (P . B) = (( COM P) . A)

    proof

      let A be Element of ( COM (Sigma,P)), B be set such that

       A1: B in ( ProbPart A);

      reconsider C = (A \ B) as thin of P by A1, Def7;

      

       A2: B in Sigma by A1, Def7;

      B c= A by A1, Def7;

      then

       A3: A = (B \/ C) by XBOOLE_1: 45;

      Sigma c= ( COM (Sigma,P)) by Th28;

      then

      reconsider B as Event of ( COM (Sigma,P)) by A2;

      reconsider A as Event of ( COM (Sigma,P));

      B misses C by XBOOLE_1: 79;

      

      then

       A4: (( COM P) . A) = ((( COM P) . B) + (( COM P) . C)) by A3, PROB_1:def 8

      .= ((( COM P) . B) + 0 ) by Th40

      .= (( COM P) . B);

      reconsider B as Event of Sigma by A1, Def7;

      (( COM P) . A) = (P . B) by A4, Th39;

      hence thesis;

    end;