prob_1.miz



    begin

    reserve Omega for set;

    reserve X,Y,Z,p,x,y,z for set;

    reserve D,E for Subset of Omega;

    reserve f for Function;

    reserve m,n for Nat;

    reserve r,r1 for Real;

    reserve seq for Real_Sequence;

    theorem :: PROB_1:1

    

     Th1: for r, seq st (ex n st for m st n <= m holds (seq . m) = r) holds seq is convergent & ( lim seq) = r

    proof

      let r, seq such that

       A1: ex n st for m st n <= m holds (seq . m) = r;

      

       A2: for r1 st 0 < r1 holds ex n st for m st n <= m holds |.((seq . m) - r).| < r1

      proof

        consider n such that

         A3: for m st n <= m holds (seq . m) = r by A1;

        let r1 such that

         A4: 0 < r1;

        take n;

        let m;

        assume n <= m;

        then (seq . m) = r by A3;

        hence thesis by A4, ABSVALUE: 2;

      end;

      then seq is convergent by SEQ_2:def 6;

      hence thesis by A2, SEQ_2:def 7;

    end;

    definition

      let X be set;

      let IT be Subset-Family of X;

      :: PROB_1:def1

      attr IT is compl-closed means

      : Def1: for A be Subset of X st A in IT holds (A ` ) in IT;

    end

    registration

      let X be set;

      cluster ( bool X) -> cap-closed;

      coherence

      proof

        let A,B be set;

        assume that

         A1: A in ( bool X) and B in ( bool X);

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

        hence thesis;

      end;

    end

    registration

      let X be set;

      cluster ( bool X) -> compl-closed;

      coherence ;

    end

    registration

      let X be set;

      cluster non empty compl-closed cap-closed for Subset-Family of X;

      existence

      proof

        take ( bool X);

        thus thesis;

      end;

    end

    definition

      let X be set;

      mode Field_Subset of X is non empty compl-closed cap-closed Subset-Family of X;

    end

    reserve F for Field_Subset of X;

    theorem :: PROB_1:2

    

     Th2: for A,B be Subset of X holds {A, B} is Subset-Family of X

    proof

      let A,B be Subset of X;

      set C = {A, B};

      C c= ( bool X)

      proof

        let x be object;

        assume x in C;

        then x = A or x = B by TARSKI:def 2;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: PROB_1:3

    

     Th3: for A,B be set st A in F & B in F holds (A \/ B) in F

    proof

      let A,B be set;

      assume

       A1: A in F & B in F;

      then

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

      (A1 ` ) in F & (B1 ` ) in F by A1, Def1;

      then ((A1 ` ) /\ (B1 ` )) in F by FINSUB_1:def 2;

      then ((A1 \/ B1) ` ) in F by XBOOLE_1: 53;

      then (((A1 \/ B1) ` ) ` ) in F by Def1;

      hence thesis;

    end;

    theorem :: PROB_1:4

    

     Th4: {} in F

    proof

      consider A be Subset of X such that

       A1: A in F by SUBSET_1: 4;

      A misses (A ` ) by XBOOLE_1: 79;

      then

       A2: (A /\ (A ` )) = {} by XBOOLE_0:def 7;

      (A ` ) in F by A1, Def1;

      hence thesis by A1, A2, FINSUB_1:def 2;

    end;

    theorem :: PROB_1:5

    

     Th5: X in F

    proof

      consider A be Subset of X such that

       A1: A in F by SUBSET_1: 4;

      

       A2: (A \/ (A ` )) = ( [#] X) by SUBSET_1: 10

      .= X;

      (A ` ) in F by A1, Def1;

      hence thesis by A1, A2, Th3;

    end;

    theorem :: PROB_1:6

    

     Th6: for A,B be Subset of X holds A in F & B in F implies (A \ B) in F

    proof

      let A,B be Subset of X;

      assume

       A1: A in F;

      assume B in F;

      then (B ` ) in F by Def1;

      then (A /\ (B ` )) in F by A1, FINSUB_1:def 2;

      hence thesis by SUBSET_1: 13;

    end;

    theorem :: PROB_1:7

    for A,B be set holds (A in F & B in F implies ((A \ B) \/ B) in F)

    proof

      let A,B be set;

      (A \/ B) = ((A \ B) \/ B) by XBOOLE_1: 39;

      hence thesis by Th3;

    end;

    registration

      let X be set;

      cluster { {} , X} -> cap-closed;

      coherence

      proof

        let A,B be set;

        

         A1: (A = {} or B = {} ) implies (A /\ B) = {} ;

        A = X & B = X implies (A /\ B) = X;

        hence thesis by A1, TARSKI:def 2;

      end;

    end

    theorem :: PROB_1:8

     { {} , X} is Field_Subset of X

    proof

       {} c= X & X in ( bool X) by ZFMISC_1:def 1;

      then

      reconsider EX = { {} , X} as Subset-Family of X by Th2;

      now

        let A be Subset of X;

        

         A1: A = {} implies (A ` ) = X;

        A = X implies (A ` ) = ( {} X) by XBOOLE_1: 37;

        hence A in EX implies (A ` ) in EX by A1, TARSKI:def 2;

      end;

      hence thesis by Def1;

    end;

    theorem :: PROB_1:9

    ( bool X) is Field_Subset of X;

    theorem :: PROB_1:10

     { {} , X} c= F & F c= ( bool X)

    proof

       {} in F & X in F by Th4, Th5;

      then for x be object holds x in { {} , X} implies x in F by TARSKI:def 2;

      hence thesis;

    end;

    definition

      let X be set;

      mode SetSequence of X is sequence of ( bool X);

    end

    reserve ASeq,BSeq for SetSequence of Omega;

    reserve A1 for SetSequence of X;

    theorem :: PROB_1:11

    

     Th11: ( union ( rng A1)) is Subset of X

    proof

      for Y st Y in ( rng A1) holds Y c= X

      proof

        let Y;

        assume Y in ( rng A1);

        then

        consider y be object such that

         A1: y in ( dom A1) and

         A2: Y = (A1 . y) by FUNCT_1:def 3;

        reconsider y as Element of NAT by A1, FUNCT_2:def 1;

        Y = (A1 . y) by A2;

        hence thesis;

      end;

      hence thesis by ZFMISC_1: 76;

    end;

    definition

      let X be set, A1 be SetSequence of X;

      :: original: Union

      redefine

      func Union A1 -> Subset of X ;

      coherence by Th11;

    end

    theorem :: PROB_1:12

    

     Th12: x in ( Union A1) iff ex n st x in (A1 . n)

    proof

      set DX = ( union ( rng A1));

      for x holds x in DX iff ex n st x in (A1 . n)

      proof

        let x;

        thus x in DX implies ex n st x in (A1 . n)

        proof

          assume x in DX;

          then

          consider Y such that

           A1: x in Y and

           A2: Y in ( rng A1) by TARSKI:def 4;

          consider p be object such that

           A3: p in ( dom A1) and

           A4: Y = (A1 . p) by A2, FUNCT_1:def 3;

          p in NAT by A3, FUNCT_2:def 1;

          hence thesis by A1, A4;

        end;

        thus (ex n st x in (A1 . n)) implies x in DX

        proof

          given n such that

           A5: x in (A1 . n);

          n in NAT by ORDINAL1:def 12;

          then n in ( dom A1) by FUNCT_2:def 1;

          then (A1 . n) in ( rng A1) by FUNCT_1:def 3;

          hence thesis by A5, TARSKI:def 4;

        end;

      end;

      hence thesis;

    end;

    definition

      let X be set, A1 be SetSequence of X;

      :: PROB_1:def2

      func Complement A1 -> SetSequence of X means

      : Def2: for n holds (it . n) = ((A1 . n) ` );

      existence

      proof

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

        consider f be sequence of ( bool X) such that

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

        

         A2: for x be Nat holds (f . x) = ((A1 . x) ` )

        proof

          let x be Nat;

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

          (f . x) = F(x) by A1;

          hence thesis;

        end;

        take f;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let BSeq,CSeq be SetSequence of X such that

         A3: for n holds (BSeq . n) = ((A1 . n) ` ) and

         A4: for m holds (CSeq . m) = ((A1 . m) ` );

        

         A5: for x be object st x in NAT holds (BSeq . x) = (CSeq . x)

        proof

          let x be object;

          assume x in NAT ;

          then

          reconsider x as Element of NAT ;

          (BSeq . x) = ((A1 . x) ` ) by A3

          .= (CSeq . x) by A4;

          hence thesis;

        end;

        thus thesis by A5;

      end;

      involutiveness

      proof

        let IT,A1 be SetSequence of X;

        assume

         A6: for n holds (IT . n) = ((A1 . n) ` );

        let n;

        

        thus (A1 . n) = (((A1 . n) ` ) ` )

        .= ((IT . n) ` ) by A6;

      end;

    end

    definition

      let X be set, A1 be SetSequence of X;

      :: PROB_1:def3

      func Intersection A1 -> Subset of X equals (( Union ( Complement A1)) ` );

      correctness ;

    end

    theorem :: PROB_1:13

    

     Th13: for x be object holds x in ( Intersection A1) iff for n holds x in (A1 . n)

    proof

      let x be object;

      

       A1: for n holds (X \ (( Complement A1) . n)) = (A1 . n)

      proof

        let n;

        (X \ (( Complement A1) . n)) = (((A1 . n) ` ) ` ) by Def2

        .= (A1 . n);

        hence thesis;

      end;

      

       A2: (for n holds (x in X & not x in (( Complement A1) . n))) iff for n holds x in (A1 . n)

      proof

        thus (for n holds (x in X & not x in (( Complement A1) . n))) implies for n holds x in (A1 . n)

        proof

          assume

           A3: for n holds x in X & not x in (( Complement A1) . n);

          let n;

           not x in (( Complement A1) . n) by A3;

          then x in (X \ (( Complement A1) . n)) by A3, XBOOLE_0:def 5;

          hence thesis by A1;

        end;

        assume

         A4: for n holds x in (A1 . n);

        let n;

        x in (A1 . n) by A4;

        then x in (X \ (( Complement A1) . n)) by A1;

        hence thesis by XBOOLE_0:def 5;

      end;

      x in X & not x in ( Union ( Complement A1)) iff x in X & for n holds not x in (( Complement A1) . n) by Th12;

      hence thesis by A2, XBOOLE_0:def 5;

    end;

    

     Lm1: for A,B be Subset of X holds ( Complement (A followed_by B)) = ((A ` ) followed_by (B ` ))

    proof

      let A,B be Subset of X;

      let n be Element of NAT ;

      per cases by NAT_1: 3;

        suppose

         A1: n = 0 ;

        

        thus (( Complement (A followed_by B)) . n) = (((A followed_by B) . n) ` ) by Def2

        .= (A ` ) by A1, FUNCT_7: 119

        .= (((A ` ) followed_by (B ` )) . n) by A1, FUNCT_7: 119;

      end;

        suppose

         A2: n > 0 ;

        

        thus (( Complement (A followed_by B)) . n) = (((A followed_by B) . n) ` ) by Def2

        .= (B ` ) by A2, FUNCT_7: 120

        .= (((A ` ) followed_by (B ` )) . n) by A2, FUNCT_7: 120;

      end;

    end;

    theorem :: PROB_1:14

    

     Th14: for A,B be Subset of X holds ( Intersection (A followed_by B)) = (A /\ B)

    proof

      let A,B be Subset of X;

      set A1 = (A followed_by B);

      ( Complement A1) = ((A ` ) followed_by (B ` )) by Lm1;

      then ( rng ( Complement A1)) = {(A ` ), (B ` )} by FUNCT_7: 126;

      then ( Union ( Complement A1)) = ((A ` ) \/ (B ` )) by ZFMISC_1: 75;

      then (( Union ( Complement A1)) ` ) = (((A ` ) ` ) /\ ((B ` ) ` )) by XBOOLE_1: 53;

      hence thesis;

    end;

    definition

      let f be Function;

      :: PROB_1:def4

      attr f is non-ascending means for n, m st n <= m holds (f . m) c= (f . n);

      :: PROB_1:def5

      attr f is non-descending means for n, m st n <= m holds (f . n) c= (f . m);

    end

    definition

      let X be set, F be Subset-Family of X;

      :: PROB_1:def6

      attr F is sigma-multiplicative means

      : Def6: for A1 be SetSequence of X st ( rng A1) c= F holds ( Intersection A1) in F;

    end

    registration

      let X be set;

      cluster ( bool X) -> sigma-multiplicative;

      coherence ;

    end

    registration

      let X be set;

      cluster compl-closed sigma-multiplicative non empty for Subset-Family of X;

      existence

      proof

        take ( bool X);

        thus thesis;

      end;

    end

    definition

      let X be set;

      mode SigmaField of X is compl-closed sigma-multiplicative non empty Subset-Family of X;

    end

    theorem :: PROB_1:15

    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 ( Intersection A1) in S) & for A be Subset of X st A in S holds (A ` ) in S by Def1, Def6;

    theorem :: PROB_1:16

    

     Th16: Y is SigmaField of X implies Y is Field_Subset of X

    proof

      assume

       A1: Y is SigmaField of X;

      Y is cap-closed

      proof

        let A,B be set;

        assume

         A2: A in Y & B in Y;

        then

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

        set A1 = (A9 followed_by B9);

        ( rng A1) = {A9, B9} by FUNCT_7: 126;

        then

         A3: ( rng A1) c= Y by A2, ZFMISC_1: 32;

        ( Intersection A1) = (A /\ B) by Th14;

        hence thesis by A1, A3, Def6;

      end;

      hence thesis by A1;

    end;

    registration

      let X be set;

      cluster -> cap-closed compl-closed for SigmaField of X;

      coherence by Th16;

    end

    reserve Sigma for SigmaField of Omega;

    reserve Si for SigmaField of X;

    registration

      let X be set, F be non empty Subset-Family of X;

      cluster F -valued for SetSequence of X;

      existence

      proof

        set A1 = ( NAT --> the Element of F);

        reconsider A1 as SetSequence of X by FUNCOP_1: 45;

        take A1;

        thus thesis;

      end;

    end

    definition

      let X be set, F be non empty Subset-Family of X;

      mode SetSequence of F is F -valued SetSequence of X;

    end

    theorem :: PROB_1:17

    

     Th17: for ASeq be SetSequence of Si holds ( Union ASeq) in Si

    proof

      let ASeq be SetSequence of Si;

      

       A1: ( rng A1) c= Si implies for n be Nat holds (( Complement A1) . n) in Si

      proof

        assume

         A2: ( rng A1) c= Si;

        let n be Nat;

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

        then n in NAT & ((A1 . n) ` ) in Si by A2, Def1, ORDINAL1:def 12;

        hence thesis by Def2;

      end;

      

       A3: ( rng A1) c= Si implies ( Union ( Complement ( Complement A1))) in Si

      proof

        assume ( rng A1) c= Si;

        then for n be Nat holds (( Complement A1) . n) in Si by A1;

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

        then ( Intersection ( Complement A1)) in Si by Def6;

        then ((( Union ( Complement ( Complement A1))) ` ) ` ) in Si by Def1;

        hence thesis;

      end;

      

       A4: for A1 st ( rng A1) c= Si holds ( Union A1) in Si

      proof

        let A1;

        assume ( rng A1) c= Si;

        then ( Union ( Complement ( Complement A1))) in Si by A3;

        hence thesis;

      end;

      ( rng ASeq) c= Si by RELAT_1:def 19;

      hence thesis by A4;

    end;

    notation

      let X be set;

      let F be SigmaField of X;

      synonym Event of F for Element of F;

    end

    definition

      let X be set, F be SigmaField of X;

      :: original: Event

      redefine

      mode Event of F -> Subset of X ;

      coherence

      proof

        let E be Event of F;

        E in F;

        hence thesis;

      end;

    end

    theorem :: PROB_1:18

    x in Si implies x is Event of Si;

    theorem :: PROB_1:19

    for A,B be Event of Si holds (A /\ B) is Event of Si by FINSUB_1:def 2;

    theorem :: PROB_1:20

    for A be Event of Si holds (A ` ) is Event of Si by Def1;

    theorem :: PROB_1:21

    for A,B be Event of Si holds (A \/ B) is Event of Si by Th3;

    theorem :: PROB_1:22

     {} is Event of Si by Th4;

    theorem :: PROB_1:23

    X is Event of Si by Th5;

    theorem :: PROB_1:24

    for A,B be Event of Si holds (A \ B) is Event of Si by Th6;

    registration

      let X, Si;

      cluster empty for Event of Si;

      existence

      proof

         {} is Event of Si by Th4;

        hence thesis;

      end;

    end

    definition

      let X, Si;

      :: PROB_1:def7

      func [#] Si -> Event of Si equals X;

      coherence by Th5;

    end

    definition

      let X, Si;

      let A,B be Event of Si;

      :: original: /\

      redefine

      func A /\ B -> Event of Si ;

      coherence by FINSUB_1:def 2;

      :: original: \/

      redefine

      func A \/ B -> Event of Si ;

      coherence by Th3;

      :: original: \

      redefine

      func A \ B -> Event of Si ;

      coherence by Th6;

    end

    theorem :: PROB_1:25

    A1 is SetSequence of Si iff for n holds (A1 . n) is Event of Si

    proof

      thus A1 is SetSequence of Si implies for n holds (A1 . n) is Event of Si

      proof

        assume A1 is SetSequence of Si;

        then

         A1: ( rng A1) c= Si by RELAT_1:def 19;

        for n holds (A1 . n) is Event of Si by NAT_1: 51, A1;

        hence thesis;

      end;

      assume

       A2: for n holds (A1 . n) is Event of Si;

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

      proof

        let n be Nat;

        (A1 . n) is Event of Si by A2;

        hence thesis;

      end;

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

      hence thesis by RELAT_1:def 19;

    end;

    theorem :: PROB_1:26

    ASeq is SetSequence of Sigma implies ( Union ASeq) is Event of Sigma by Th17;

    reserve A,B for Event of Sigma,

ASeq for SetSequence of Sigma;

    theorem :: PROB_1:27

    

     Th27: ex f st (( dom f) = Sigma & for D st D in Sigma holds (p in D implies (f . D) = 1) & ( not p in D implies (f . D) = 0 ))

    proof

      deffunc G( set) = 0 ;

      deffunc F( set) = 1;

      defpred C[ set] means p in $1;

      ex f be Function st ( dom f) = Sigma & for x be set st x in Sigma holds ( C[x] implies (f . x) = F(x)) & ( not C[x] implies (f . x) = G(x)) from PARTFUN1:sch 5;

      then

      consider f be Function such that

       A1: ( dom f) = Sigma and

       A2: for x be set st x in Sigma holds ( C[x] implies (f . x) = 1) & ( not C[x] implies (f . x) = 0 );

      take f;

      thus ( dom f) = Sigma by A1;

      let D;

      assume

       A3: D in Sigma;

      hence p in D implies (f . D) = 1 by A2;

      assume not p in D;

      hence thesis by A2, A3;

    end;

    reserve P for Function of Sigma, REAL ;

    theorem :: PROB_1:28

    

     Th28: ex P st for D st D in Sigma holds (p in D implies (P . D) = 1) & ( not p in D implies (P . D) = 0 )

    proof

      consider f such that

       A1: ( dom f) = Sigma and

       A2: for D st D in Sigma holds (p in D implies (f . D) = 1) & ( not p in D implies (f . D) = 0 ) by Th27;

      

       A3: 0 in REAL by XREAL_0:def 1;

      ( rng f) c= REAL

      proof

        let y be object;

        assume y in ( rng f);

        then

        consider x be object such that

         A4: x in ( dom f) and

         A5: y = (f . x) by FUNCT_1:def 3;

        reconsider x as Subset of Omega by A1, A4;

        reconsider j = 1 as Real;

        

         A6: 1 in REAL by XREAL_0:def 1;

        

         A7: not p in x implies y = 0 by A1, A2, A4, A5;

        p in x implies y = j by A1, A2, A4, A5;

        hence thesis by A7, A3, A6;

      end;

      then

      reconsider f as Function of Sigma, REAL by A1, FUNCT_2:def 1, RELSET_1: 4;

      take f;

      thus thesis by A2;

    end;

    theorem :: PROB_1:29

    

     Th29: (P * ASeq) is Real_Sequence

    proof

      ( rng ASeq) c= Sigma by RELAT_1:def 19;

      then ( rng ASeq) c= ( dom P) by FUNCT_2:def 1;

      

      then

       A1: ( dom (P * ASeq)) = ( dom ASeq) by RELAT_1: 27

      .= NAT by FUNCT_2:def 1;

      ( rng (P * ASeq)) c= REAL by RELAT_1:def 19;

      hence thesis by A1, FUNCT_2:def 1, RELSET_1: 4;

    end;

    definition

      let Omega, Sigma, ASeq, P;

      :: original: *

      redefine

      func P * ASeq -> Real_Sequence ;

      coherence by Th29;

    end

    reserve Omega for non empty set;

    reserve Sigma for SigmaField of Omega;

    reserve A,B for Event of Sigma,

ASeq for SetSequence of Sigma;

    reserve P for Function of Sigma, REAL ;

    reserve D,E for Subset of Omega;

    reserve BSeq for SetSequence of Omega;

    definition

      let Omega, Sigma;

      :: PROB_1:def8

      mode Probability of Sigma -> Function of Sigma, REAL means

      : Def8: (for A holds 0 <= (it . A)) & (it . Omega) = 1 & (for A, B st A misses B holds (it . (A \/ B)) = ((it . A) + (it . B))) & for ASeq st ASeq is non-ascending holds (it * ASeq) is convergent & ( lim (it * ASeq)) = (it . ( Intersection ASeq));

      existence

      proof

        set p = the Element of Omega;

        consider P such that

         A1: for D st D in Sigma holds (p in D implies (P . D) = 1) & ( not p in D implies (P . D) = 0 ) by Th28;

        take P;

        thus for A holds 0 <= (P . A) by A1;

        ( [#] Sigma) in Sigma;

        hence (P . Omega) = 1 by A1;

        thus for A, B st A misses B holds (P . (A \/ B)) = ((P . A) + (P . B))

        proof

          let A, B such that

           A2: A misses B;

          

           A3: p in A & not p in B implies p in (A \/ B) by XBOOLE_0:def 3;

          

           A4: not p in A & p in B implies (P . A) = 0 & (P . B) = 1 by A1;

          

           A5: not p in A & p in B implies p in (A \/ B) by XBOOLE_0:def 3;

          

           A6: not p in A & not p in B implies (P . A) = 0 & (P . B) = 0 by A1;

          

           A7: not p in A & not p in B implies not p in (A \/ B) by XBOOLE_0:def 3;

          p in A & not p in B implies (P . A) = 1 & (P . B) = 0 by A1;

          hence thesis by A1, A2, A3, A4, A5, A6, A7, XBOOLE_0: 3;

        end;

        let ASeq;

        

         A8: for n holds ((P * ASeq) . n) = (P . (ASeq . n))

        proof

          let n;

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

          ( dom (P * ASeq)) = NAT by FUNCT_2:def 1;

          then ((P * ASeq) . n) = (P . (ASeq . n)) by FUNCT_1: 12;

          hence thesis;

        end;

        

         A9: (for n holds p in (ASeq . n)) implies for n holds ((P * ASeq) . n) = 1

        proof

          assume

           A10: for n holds p in (ASeq . n);

          for n holds ((P * ASeq) . n) = 1

          proof

            let n;

            

             A11: ( rng ASeq) c= Sigma & (ASeq . n) in ( rng ASeq) by NAT_1: 51, RELAT_1:def 19;

            p in (ASeq . n) by A10;

            then (P . (ASeq . n)) = 1 by A1, A11;

            hence thesis by A8;

          end;

          hence thesis;

        end;

        assume

         A12: ASeq is non-ascending;

        

         A13: not (for n holds p in (ASeq . n)) implies ex m st for n st m <= n holds ((P * ASeq) . n) = 0

        proof

          assume not (for n holds p in (ASeq . n));

          then

          consider m such that

           A14: not p in (ASeq . m);

          take m;

          for n st m <= n holds ((P * ASeq) . n) = 0

          proof

            let n;

            assume m <= n;

            then (ASeq . n) c= (ASeq . m) by A12;

            then

             A15: not p in (ASeq . n) by A14;

            ( rng ASeq) c= Sigma & (ASeq . n) in ( rng ASeq) by NAT_1: 51, RELAT_1:def 19;

            then (P . (ASeq . n)) = 0 by A1, A15;

            hence thesis by A8;

          end;

          hence thesis;

        end;

        

         A16: (ex m st (for n st m <= n holds ((P * ASeq) . n) = 0 )) implies (P * ASeq) is convergent & ( lim (P * ASeq)) = 0 by Th1;

        ( rng ASeq) c= Sigma by RELAT_1:def 19;

        then

         A17: ( Intersection ASeq) in Sigma by Def6;

        reconsider r = 1 as Real;

        

         A18: (for n holds ((P * ASeq) . n) = 1) implies (P * ASeq) is convergent & ( lim (P * ASeq)) = 1

        proof

          assume

           A19: for n holds ((P * ASeq) . n) = 1;

          ex m st for n st m <= n holds ((P * ASeq) . n) = r

          proof

            take 0 ;

            thus thesis by A19;

          end;

          hence thesis by Th1;

        end;

        per cases ;

          suppose

           A20: not (for n holds p in (ASeq . n));

          then not p in ( Intersection ASeq) by Th13;

          hence thesis by A1, A13, A16, A20, A17;

        end;

          suppose

           A21: for n holds p in (ASeq . n);

          then p in ( Intersection ASeq) by Th13;

          hence thesis by A1, A9, A18, A21, A17;

        end;

      end;

    end

    reserve P for Probability of Sigma;

    registration

      let Omega, Sigma;

      cluster -> zeroed for Probability of Sigma;

      coherence

      proof

        reconsider E = {} as Event of Sigma by Th4;

        let P be Probability of Sigma;

        

         A1: {} misses ( [#] Sigma) & ( {} \/ ( [#] Sigma)) = ( [#] Sigma) by XBOOLE_1: 65;

        1 = (P . ( [#] Sigma)) by Def8;

        then 1 = ((P . E) + 1) by A1, Def8;

        hence (P . {} ) = 0 ;

      end;

    end

    theorem :: PROB_1:30

    (P . ( [#] Sigma)) = 1 by Def8;

    theorem :: PROB_1:31

    

     Th31: ((P . (( [#] Sigma) \ A)) + (P . A)) = 1

    proof

      

       A1: ((( [#] Sigma) \ A) \/ A) = ((A ` ) \/ A)

      .= ( [#] Omega) by SUBSET_1: 10

      .= Omega;

      (( [#] Sigma) \ A) misses A by XBOOLE_1: 79;

      

      then ((P . (( [#] Sigma) \ A)) + (P . A)) = (P . Omega) by A1, Def8

      .= 1 by Def8;

      hence thesis;

    end;

    theorem :: PROB_1:32

    (P . (( [#] Sigma) \ A)) = (1 - (P . A))

    proof

      ((P . (( [#] Sigma) \ A)) + (P . A)) = 1 by Th31;

      hence thesis;

    end;

    theorem :: PROB_1:33

    

     Th33: A c= B implies (P . (B \ A)) = ((P . B) - (P . A))

    proof

      assume

       A1: A c= B;

      A misses (B \ A) by XBOOLE_1: 79;

      

      then ((P . A) + (P . (B \ A))) = (P . (A \/ (B \ A))) by Def8

      .= (P . B) by A1, XBOOLE_1: 45;

      hence thesis;

    end;

    theorem :: PROB_1:34

    

     Th34: A c= B implies (P . A) <= (P . B)

    proof

      assume A c= B;

      then (P . (B \ A)) = ((P . B) - (P . A)) by Th33;

      then 0 <= ((P . B) - (P . A)) by Def8;

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

      hence thesis;

    end;

    theorem :: PROB_1:35

    (P . A) <= 1

    proof

      (P . ( [#] Sigma)) = 1 by Def8;

      hence thesis by Th34;

    end;

    theorem :: PROB_1:36

    

     Th36: (P . (A \/ B)) = ((P . A) + (P . (B \ A)))

    proof

      

       A1: A misses (B \ A) by XBOOLE_1: 79;

      (P . (A \/ B)) = (P . (A \/ (B \ A))) by XBOOLE_1: 39

      .= ((P . A) + (P . (B \ A))) by A1, Def8;

      hence thesis;

    end;

    theorem :: PROB_1:37

    

     Th37: (P . (A \/ B)) = ((P . A) + (P . (B \ (A /\ B))))

    proof

      

      thus (P . (A \/ B)) = ((P . A) + (P . (B \ A))) by Th36

      .= ((P . A) + (P . (B \ (A /\ B)))) by XBOOLE_1: 47;

    end;

    theorem :: PROB_1:38

    

     Th38: (P . (A \/ B)) = (((P . A) + (P . B)) - (P . (A /\ B)))

    proof

      (P . (A \/ B)) = ((P . A) + (P . (B \ (A /\ B)))) by Th37

      .= ((P . A) + ((P . B) - (P . (A /\ B)))) by Th33, XBOOLE_1: 17;

      hence thesis;

    end;

    theorem :: PROB_1:39

    (P . (A \/ B)) <= ((P . A) + (P . B))

    proof

       0 <= (P . (A /\ B)) & (P . (A \/ B)) = (((P . A) + (P . B)) - (P . (A /\ B))) by Def8, Th38;

      hence thesis by XREAL_1: 43;

    end;

    reserve D for Subset of REAL ;

    reserve S for Subset-Family of Omega;

    theorem :: PROB_1:40

    ( bool X) is SigmaField of X;

    definition

      let Omega;

      let X be Subset-Family of Omega;

      :: PROB_1:def9

      func sigma (X) -> SigmaField of Omega means X c= it & for Z st X c= Z & Z is SigmaField of Omega holds it c= Z;

      existence

      proof

        set V = { S : X c= S & S is SigmaField of Omega };

        set Y = ( meet V);

         A1:

        now

          let Z;

          assume Z in V;

          then ex S st Z = S & X c= S & S is SigmaField of Omega;

          hence X c= Z;

        end;

        

         A2: ( bool Omega) in V;

        

         A3: for E st E in Y holds (E ` ) in Y

        proof

          let E such that

           A4: E in Y;

          now

            let Z;

            assume Z in V;

            then E in Z & ex S st Z = S & X c= S & S is SigmaField of Omega by A4, SETFAM_1:def 1;

            hence (E ` ) in Z by Def1;

          end;

          hence thesis by A2, SETFAM_1:def 1;

        end;

        

         A5: for BSeq st ( rng BSeq) c= Y holds ( Intersection BSeq) in Y

        proof

          let BSeq such that

           A6: ( rng BSeq) c= Y;

          now

            let Z;

            assume

             A7: Z in V;

            now

              let n be Nat;

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

              hence (BSeq . n) in Z by A6, A7, SETFAM_1:def 1;

            end;

            then

             A8: ( rng BSeq) c= Z by NAT_1: 52;

            ex S st Z = S & X c= S & S is SigmaField of Omega by A7;

            hence ( Intersection BSeq) in Z by A8, Def6;

          end;

          hence thesis by A2, SETFAM_1:def 1;

        end;

        now

          let Z;

          assume Z in V;

          then ex S st Z = S & X c= S & S is SigmaField of Omega;

          hence {} in Z by Th4;

        end;

        then

        reconsider Y as SigmaField of Omega by A2, A5, A3, Def1, Def6, SETFAM_1: 3, SETFAM_1:def 1;

        take Y;

        for Z st X c= Z & Z is SigmaField of Omega holds Y c= Z

        proof

          let Z;

          assume that

           A9: X c= Z and

           A10: Z is SigmaField of Omega;

          reconsider Z as Subset-Family of Omega by A10;

          Z in V by A9, A10;

          hence thesis by SETFAM_1: 3;

        end;

        hence thesis by A2, A1, SETFAM_1: 5;

      end;

      uniqueness

      proof

        let R1,R2 be SigmaField of Omega;

        assume X c= R1 & (for Z st X c= Z & Z is SigmaField of Omega holds R1 c= Z) & X c= R2 & for Z st X c= Z & Z is SigmaField of Omega holds R2 c= Z;

        then R1 c= R2 & R2 c= R1;

        hence thesis by XBOOLE_0:def 10;

      end;

    end

    definition

      let r be ExtReal;

      :: PROB_1:def10

      func halfline r -> Subset of REAL equals ]. -infty , r.[;

      coherence

      proof

         ]. -infty , r.[ c= REAL

        proof

          let x be Real;

          assume x in ]. -infty , r.[;

          then -infty < x & x < r by XXREAL_1: 4;

          hence thesis by XXREAL_0: 48;

        end;

        hence thesis;

      end;

    end

    definition

      :: PROB_1:def11

      func Family_of_halflines -> Subset-Family of REAL equals the set of all ( halfline r) where r be Element of REAL ;

      coherence

      proof

         the set of all ( halfline r) where r be Element of REAL c= ( bool REAL )

        proof

          let p be object;

          assume p in the set of all ( halfline r) where r be Element of REAL ;

          then ex r be Element of REAL st p = ( halfline r);

          hence p in ( bool REAL );

        end;

        hence thesis;

      end;

    end

    definition

      :: PROB_1:def12

      func Borel_Sets -> SigmaField of REAL equals ( sigma Family_of_halflines );

      correctness ;

    end

    theorem :: PROB_1:41

    for A,B be Subset of X holds ( Complement (A followed_by B)) = ((A ` ) followed_by (B ` )) by Lm1;

    definition

      let X,Y be set;

      let A be Subset-Family of X;

      let F be Function of Y, ( bool A);

      let x be set;

      :: original: .

      redefine

      func F . x -> Subset-Family of X ;

      coherence

      proof

        per cases ;

          suppose

           A1: x in ( dom F);

          

           A2: ( rng F) c= ( bool A) by RELAT_1:def 19;

          

           A3: ( bool A) c= ( bool ( bool X)) by ZFMISC_1: 67;

          (F . x) in ( rng F) by A1, FUNCT_1:def 3;

          then (F . x) in ( bool A) by A2;

          hence thesis by A3;

        end;

          suppose not x in ( dom F);

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

          hence thesis by XBOOLE_1: 2;

        end;

      end;

    end