prob_2.miz



    begin

    reserve Omega for set;

    reserve m,n,k for Nat;

    reserve x,y for object;

    reserve r,r1,r2,r3 for Real;

    reserve seq,seq1 for Real_Sequence;

    reserve Sigma for SigmaField of Omega;

    reserve ASeq,BSeq for SetSequence of Sigma;

    reserve A,B,C,A1,A2,A3 for Event of Sigma;

    theorem :: PROB_2:1

    

     Th1: for r, r1, r2, r3 st r <> 0 & r1 <> 0 holds ((r3 / r1) = (r2 / r) iff (r3 * r) = (r2 * r1))

    proof

      let r, r1, r2, r3;

      assume that

       A1: r <> 0 and

       A2: r1 <> 0 ;

      thus (r3 / r1) = (r2 / r) implies (r3 * r) = (r2 * r1)

      proof

        assume

         A3: (r3 / r1) = (r2 / r);

        (r3 * r) = (((r3 / r1) * r1) * r) by A2, XCMPLX_1: 87

        .= (((r2 / r) * r) * r1) by A3

        .= (r2 * r1) by A1, XCMPLX_1: 87;

        hence thesis;

      end;

      assume

       A4: (r3 * r) = (r2 * r1);

      (r3 / r1) = ((r3 * 1) / r1)

      .= ((r3 * (r * (r " ))) / r1) by A1, XCMPLX_0:def 7

      .= (((r2 * r1) * (r " )) / r1) by A4, XCMPLX_1: 4

      .= (((r2 * (r " )) * r1) / r1)

      .= (((r2 / r) * r1) / r1) by XCMPLX_0:def 9

      .= (((r2 / r) * r1) * (r1 " )) by XCMPLX_0:def 9

      .= ((r2 / r) * (r1 * (r1 " )))

      .= ((r2 / r) * 1) by A2, XCMPLX_0:def 7

      .= (r2 / r);

      hence thesis;

    end;

    theorem :: PROB_2:2

    

     Th2: (seq is convergent & for n holds (seq1 . n) = (r - (seq . n))) implies seq1 is convergent & ( lim seq1) = (r - ( lim seq))

    proof

      assume that

       A1: seq is convergent and

       A2: for n holds (seq1 . n) = (r - (seq . n));

      consider r1 be Real such that

       A3: for r2 be Real st 0 < r2 holds ex n st for m st n <= m holds |.((seq . m) - r1).| < r2 by A1, SEQ_2:def 6;

       A4:

      now

        let r2 be Real;

        assume 0 < r2;

        then

        consider n such that

         A5: for m st n <= m holds |.((seq . m) - r1).| < r2 by A3;

        take n;

        now

          let m such that

           A6: n <= m;

           |.((seq . m) - r1).| = |.( - ((seq . m) - r1)).| by COMPLEX1: 52

          .= |.((r1 - r) + (r - (seq . m))).|

          .= |.((seq1 . m) + ( - ( - (r1 - r)))).| by A2

          .= |.((seq1 . m) - (r - r1)).|;

          hence |.((seq1 . m) - (r - r1)).| < r2 by A5, A6;

        end;

        hence for m st n <= m holds |.((seq1 . m) - (r - r1)).| < r2;

      end;

      hence

       A7: seq1 is convergent by SEQ_2:def 6;

      ( lim seq) = r1 by A1, A3, SEQ_2:def 7;

      hence thesis by A4, A7, SEQ_2:def 7;

    end;

    definition

      let Omega, Sigma, ASeq, n;

      :: original: .

      redefine

      func ASeq . n -> Event of Sigma ;

      coherence by PROB_1: 25;

    end

    definition

      let Omega, Sigma, ASeq;

      :: PROB_2:def1

      func @Intersection ASeq -> Event of Sigma equals ( Intersection ASeq);

      coherence

      proof

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

        hence thesis by PROB_1:def 6;

      end;

    end

    theorem :: PROB_2:3

    

     Th3: ex BSeq st for n holds (BSeq . n) = ((ASeq . n) /\ B)

    proof

      deffunc F( Element of NAT ) = ((ASeq . $1) /\ B);

      consider f be Function such that

       A1: ( dom f) = NAT & for n be Element of NAT holds (f . n) = F(n) from FUNCT_1:sch 4;

      now

        let m;

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

        ((ASeq . m) /\ B) in ( bool Omega);

        then (f . mm) in ( bool Omega) by A1;

        hence (f . m) in ( bool Omega);

      end;

      then for x be object st x in NAT holds (f . x) in ( bool Omega);

      then

      reconsider f as SetSequence of Omega by A1, FUNCT_2: 3;

      now

        let m be Nat;

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

        ((ASeq . m1) /\ B) in Sigma;

        hence (f . m) in Sigma by A1;

      end;

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

      then

      reconsider f as SetSequence of Sigma by RELAT_1:def 19;

      take f;

      let n;

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

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

      hence thesis;

    end;

    theorem :: PROB_2:4

    

     Th4: (ASeq is non-ascending & for n holds (BSeq . n) = ((ASeq . n) /\ B)) implies BSeq is non-ascending

    proof

      assume that

       A1: ASeq is non-ascending and

       A2: for n holds (BSeq . n) = ((ASeq . n) /\ B);

      thus BSeq qua Function is non-ascending

      proof

        let m, n;

        assume m <= n;

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

        then ((ASeq . n) /\ B) c= ((ASeq . m) /\ B) by XBOOLE_1: 26;

        then (BSeq . n) c= ((ASeq . m) /\ B) by A2;

        hence (BSeq . n) c= (BSeq . m) by A2;

      end;

    end;

    theorem :: PROB_2:5

    

     Th5: (for n holds (BSeq . n) = ((ASeq . n) /\ B)) implies (( Intersection ASeq) /\ B) = ( Intersection BSeq)

    proof

      assume

       A1: for n holds (BSeq . n) = ((ASeq . n) /\ B);

       A2:

      now

        let x be object;

        assume

         A3: x in ( Intersection BSeq);

        

         A4: for n holds x in ((ASeq . n) /\ B)

        proof

          let n;

          x in (BSeq . n) by A3, PROB_1: 13;

          hence thesis by A1;

        end;

        

         A5: for n holds x in (ASeq . n) & x in B

        proof

          let n;

          x in ((ASeq . n) /\ B) by A4;

          hence thesis by XBOOLE_0:def 4;

        end;

        then x in ( Intersection ASeq) by PROB_1: 13;

        hence x in (( Intersection ASeq) /\ B) by A5, XBOOLE_0:def 4;

      end;

      now

        let x be object;

        assume

         A6: x in (( Intersection ASeq) /\ B);

        then

         A7: x in ( Intersection ASeq) by XBOOLE_0:def 4;

        

         A8: for n holds x in ((ASeq . n) /\ B)

        proof

          let n;

          x in (ASeq . n) & x in B by A6, A7, PROB_1: 13, XBOOLE_0:def 4;

          hence thesis by XBOOLE_0:def 4;

        end;

        for n holds x in (BSeq . n)

        proof

          let n;

          x in ((ASeq . n) /\ B) by A8;

          hence thesis by A1;

        end;

        hence x in ( Intersection BSeq) by PROB_1: 13;

      end;

      hence thesis by A2, TARSKI: 2;

    end;

    registration

      let Omega, Sigma, ASeq;

      cluster ( Complement ASeq) -> Sigma -valued;

      coherence

      proof

        now

          let n be Nat;

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

          (( Complement ASeq) . n1) = ((ASeq . n1) ` ) by PROB_1:def 2;

          then (( Complement ASeq) . n1) is Event of Sigma by PROB_1: 20;

          hence (( Complement ASeq) . n) in Sigma;

        end;

        then ( rng ( Complement ASeq)) c= Sigma by NAT_1: 52;

        hence thesis by RELAT_1:def 19;

      end;

    end

    theorem :: PROB_2:6

    for X be set, S be SetSequence of X holds S is non-ascending iff for n holds (S . (n + 1)) c= (S . n)

    proof

      let X be set, S be SetSequence of X;

      thus S is non-ascending implies for n holds (S . (n + 1)) c= (S . n) by NAT_1: 11;

      assume

       A1: for n holds (S . (n + 1)) c= (S . n);

      now

        let n, m such that

         A2: n <= m;

         A3:

        now

          defpred P[ Nat] means (S . (n + $1)) c= (S . n);

          

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

          proof

            let k such that

             A5: (S . (n + k)) c= (S . n);

            (S . ((n + k) + 1)) c= (S . (n + k)) by A1;

            hence thesis by A5, XBOOLE_1: 1;

          end;

          

           A6: P[ 0 ];

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

        end;

        consider k be Nat such that

         A7: m = (n + k) by A2, NAT_1: 10;

        thus (S . m) c= (S . n) by A3, A7;

      end;

      hence thesis;

    end;

    theorem :: PROB_2:7

    for X be set, S be SetSequence of X holds S is non-descending iff for n holds (S . n) c= (S . (n + 1))

    proof

      let X be set, S be SetSequence of X;

      thus S is non-descending implies for n holds (S . n) c= (S . (n + 1)) by NAT_1: 11;

      assume

       A1: for n holds (S . n) c= (S . (n + 1));

      now

        let n, m such that

         A2: n <= m;

         A3:

        now

          defpred P[ Nat] means (S . n) c= (S . (n + $1));

          

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

          proof

            let k such that

             A5: (S . n) c= (S . (n + k));

            (S . (n + k)) c= (S . ((n + k) + 1)) by A1;

            hence thesis by A5, XBOOLE_1: 1;

          end;

          

           A6: P[ 0 ];

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

        end;

        consider k be Nat such that

         A7: m = (n + k) by A2, NAT_1: 10;

        thus (S . n) c= (S . m) by A3, A7;

      end;

      hence thesis;

    end;

    theorem :: PROB_2:8

    

     Th8: for ASeq be SetSequence of Omega holds (ASeq is non-ascending iff ( Complement ASeq) is non-descending)

    proof

      let ASeq be SetSequence of Omega;

      thus ASeq is non-ascending implies ( Complement ASeq) is non-descending

      proof

        assume

         A1: ASeq is non-ascending;

        now

          let n, m;

          assume n <= m;

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

          then ((ASeq . n) ` ) c= ((ASeq . m) ` ) by SUBSET_1: 12;

          then (( Complement ASeq) . n) c= ((ASeq . m) ` ) by PROB_1:def 2;

          hence (( Complement ASeq) . n) c= (( Complement ASeq) . m) by PROB_1:def 2;

        end;

        hence thesis;

      end;

      assume

       A2: ( Complement ASeq) is non-descending;

      now

        let n, m;

        assume n <= m;

        then (( Complement ASeq) . n) c= (( Complement ASeq) . m) by A2;

        then ((ASeq . n) ` ) c= (( Complement ASeq) . m) by PROB_1:def 2;

        then ((ASeq . n) ` ) c= ((ASeq . m) ` ) by PROB_1:def 2;

        hence (ASeq . m) c= (ASeq . n) by SUBSET_1: 12;

      end;

      hence thesis;

    end;

    

     Lm1: for ASeq be SetSequence of Omega holds (ASeq is non-descending iff ( Complement ASeq) is non-ascending)

    proof

      let ASeq be SetSequence of Omega;

      thus ASeq is non-descending implies ( Complement ASeq) is non-ascending

      proof

        assume

         A1: ASeq is non-descending;

        now

          let n, m;

          assume n <= m;

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

          then ((ASeq . m) ` ) c= ((ASeq . n) ` ) by SUBSET_1: 12;

          then (( Complement ASeq) . m) c= ((ASeq . n) ` ) by PROB_1:def 2;

          hence (( Complement ASeq) . m) c= (( Complement ASeq) . n) by PROB_1:def 2;

        end;

        hence thesis;

      end;

      assume

       A2: ( Complement ASeq) is non-ascending;

      now

        let n, m;

        assume n <= m;

        then (( Complement ASeq) . m) c= (( Complement ASeq) . n) by A2;

        then ((ASeq . m) ` ) c= (( Complement ASeq) . n) by PROB_1:def 2;

        then ((ASeq . m) ` ) c= ((ASeq . n) ` ) by PROB_1:def 2;

        hence (ASeq . n) c= (ASeq . m) by SUBSET_1: 12;

      end;

      hence thesis;

    end;

    definition

      let F be Function;

      :: PROB_2:def2

      attr F is disjoint_valued means x <> y implies (F . x) misses (F . y);

    end

    definition

      let Omega, Sigma, ASeq;

      :: original: disjoint_valued

      redefine

      :: PROB_2:def3

      attr ASeq is disjoint_valued means for m, n st m <> n holds (ASeq . m) misses (ASeq . n);

      compatibility

      proof

        thus ASeq is disjoint_valued implies for m, n st m <> n holds (ASeq . m) misses (ASeq . n);

        

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

        assume

         A2: for m, n st m <> n holds (ASeq . m) misses (ASeq . n);

        let x, y;

        assume

         A3: x <> y;

        per cases ;

          suppose x in ( dom ASeq) & y in ( dom ASeq);

          hence thesis by A1, A2, A3;

        end;

          suppose not (x in ( dom ASeq) & y in ( dom ASeq));

          then (ASeq . x) = {} or (ASeq . y) = {} by FUNCT_1:def 2;

          hence thesis by XBOOLE_1: 65;

        end;

      end;

    end

    reserve Omega for non empty set;

    reserve Sigma for SigmaField of Omega;

    reserve A,B,C,A1,A2,A3 for Event of Sigma;

    reserve ASeq,BSeq for SetSequence of Sigma;

    reserve P,P1,P2 for Probability of Sigma;

    

     Lm2: for P, ASeq st ASeq is non-descending holds (P * ASeq) is convergent & ( lim (P * ASeq)) = (P . ( Union ASeq))

    proof

      let P, ASeq such that

       A1: ASeq is non-descending;

      set BSeq = ( Complement ASeq);

      

       A2: BSeq is non-ascending by A1, Lm1;

      then

       A3: (P * BSeq) is convergent by PROB_1:def 8;

       A4:

      now

        let n;

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

        ((P * BSeq) . n) = (P . (BSeq . nn)) by FUNCT_2: 15

        .= (P . ((ASeq . n) ` )) by PROB_1:def 2

        .= (P . (( [#] Sigma) \ (ASeq . n)))

        .= (1 - (P . (ASeq . n))) by PROB_1: 32

        .= (1 - ((P * ASeq) . nn)) by FUNCT_2: 15

        .= (1 + ( - ((P * ASeq) . n)));

        hence ((P * ASeq) . n) = (1 - ((P * BSeq) . n));

      end;

      hence (P * ASeq) is convergent by A3, Th2;

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

      ( Intersection BSeq) = (( [#] Sigma) \ ( Union ASeq));

      then

       A5: (P . ( Intersection BSeq)) = (1 - (P . V)) by PROB_1: 32;

      

      thus ( lim (P * ASeq)) = (1 - ( lim (P * BSeq))) by A3, A4, Th2

      .= (1 - (1 - (P . V))) by A2, A5, PROB_1:def 8

      .= (P . ( Union ASeq));

    end;

    theorem :: PROB_2:9

    

     Th9: (for A holds (P . A) = (P1 . A)) implies P = P1

    proof

      assume for A holds (P . A) = (P1 . A);

      then for x be object st x in Sigma holds (P . x) = (P1 . x);

      hence thesis by FUNCT_2: 12;

    end;

    theorem :: PROB_2:10

    for P be Function of Sigma, REAL holds P is Probability of Sigma iff (for A holds 0 <= (P . A)) & (P . Omega) = 1 & (for A, B st A misses B holds (P . (A \/ B)) = ((P . A) + (P . B))) & for ASeq st ASeq is non-descending holds (P * ASeq) is convergent & ( lim (P * ASeq)) = (P . ( Union ASeq))

    proof

      let P be Function of Sigma, REAL ;

      thus P is Probability of Sigma implies (for A holds 0 <= (P . A)) & (P . Omega) = 1 & (for A, B st A misses B holds (P . (A \/ B)) = ((P . A) + (P . B))) & for ASeq st ASeq is non-descending holds (P * ASeq) is convergent & ( lim (P * ASeq)) = (P . ( Union ASeq)) by Lm2, PROB_1:def 8;

      assume that

       A1: for A holds 0 <= (P . A) and

       A2: (P . Omega) = 1 and

       A3: for A, B st A misses B holds (P . (A \/ B)) = ((P . A) + (P . B)) and

       A4: for ASeq st ASeq is non-descending holds (P * ASeq) is convergent & ( lim (P * ASeq)) = (P . ( Union ASeq));

      for ASeq st ASeq is non-ascending holds (P * ASeq) is convergent & ( lim (P * ASeq)) = (P . ( Intersection ASeq))

      proof

        let ASeq such that

         A5: ASeq is non-ascending;

        ( Intersection ASeq) = ( @Intersection ASeq);

        then

        reconsider V = ( Intersection ASeq) as Event of Sigma;

        set BSeq = ( Complement ASeq);

        

         A6: for A holds (P . (A ` )) = (1 - (P . A))

        proof

          let A;

          reconsider B = (A ` ) as Event of Sigma by PROB_1: 20;

          

           A7: A misses B by SUBSET_1: 24;

          1 = (P . ( [#] Omega)) by A2

          .= (P . (A \/ B)) by SUBSET_1: 10

          .= ((P . A) + (P . B)) by A3, A7;

          hence thesis;

        end;

         A8:

        now

          let n;

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

          ((P * BSeq) . n) = (P . (BSeq . nn)) by FUNCT_2: 15

          .= (P . ((ASeq . n) ` )) by PROB_1:def 2

          .= (1 - (P . (ASeq . n))) by A6

          .= (1 - ((P * ASeq) . nn)) by FUNCT_2: 15

          .= (1 + ( - ((P * ASeq) . n)));

          hence ((P * ASeq) . n) = (1 - ((P * BSeq) . n));

        end;

        ( Union BSeq) = (( Intersection ASeq) ` );

        then

         A9: (P . ( Union BSeq)) = (1 - (P . V)) by A6;

        

         A10: BSeq is non-descending by A5, Th8;

        then

         A11: (P * BSeq) is convergent by A4;

        hence (P * ASeq) is convergent by A8, Th2;

        

        thus ( lim (P * ASeq)) = (1 - ( lim (P * BSeq))) by A11, A8, Th2

        .= (1 - (1 - (P . V))) by A4, A10, A9

        .= (P . ( Intersection ASeq));

      end;

      hence thesis by A1, A2, A3, PROB_1:def 8;

    end;

    theorem :: PROB_2:11

    (P . ((A \/ B) \/ C)) = (((((P . A) + (P . B)) + (P . C)) - (((P . (A /\ B)) + (P . (B /\ C))) + (P . (A /\ C)))) + (P . ((A /\ B) /\ C)))

    proof

      

       A1: (P . ((A \/ B) /\ C)) = (P . ((A /\ C) \/ (B /\ C))) by XBOOLE_1: 23

      .= (((P . (A /\ C)) + (P . (B /\ C))) - (P . ((A /\ C) /\ (B /\ C)))) by PROB_1: 38

      .= (((P . (A /\ C)) + (P . (B /\ C))) - (P . (A /\ ((B /\ C) /\ C)))) by XBOOLE_1: 16

      .= (((P . (A /\ C)) + (P . (B /\ C))) - (P . (A /\ (B /\ (C /\ C))))) by XBOOLE_1: 16

      .= (((P . (B /\ C)) + (P . (A /\ C))) - (P . ((A /\ B) /\ C))) by XBOOLE_1: 16;

      (P . ((A \/ B) \/ C)) = (((P . (A \/ B)) + (P . C)) - (P . ((A \/ B) /\ C))) by PROB_1: 38

      .= (((((P . A) + (P . B)) - (P . (A /\ B))) + (P . C)) - (P . ((A \/ B) /\ C))) by PROB_1: 38

      .= ((((P . A) + (P . B)) + (P . C)) - ((P . (A /\ B)) + (P . ((A \/ B) /\ C))));

      hence thesis by A1;

    end;

    theorem :: PROB_2:12

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

    theorem :: PROB_2:13

    (P . (A /\ B)) <= (P . B) & (P . (A /\ B)) <= (P . A) by PROB_1: 34, XBOOLE_1: 17;

    theorem :: PROB_2:14

    

     Th14: C = (B ` ) implies (P . A) = ((P . (A /\ B)) + (P . (A /\ C)))

    proof

      assume

       A1: C = (B ` );

      then B misses C by SUBSET_1: 24;

      then (A /\ C) misses B by XBOOLE_1: 74;

      then

       A2: (A /\ B) misses (A /\ C) by XBOOLE_1: 74;

      (P . A) = (P . (A /\ ( [#] Omega))) by XBOOLE_1: 28

      .= (P . (A /\ (B \/ C))) by A1, SUBSET_1: 10

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

      .= ((P . (A /\ B)) + (P . (A /\ C))) by A2, PROB_1:def 8;

      hence thesis;

    end;

    theorem :: PROB_2:15

    

     Th15: (((P . A) + (P . B)) - 1) <= (P . (A /\ B))

    proof

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

      then (((P . A) + (P . B)) - (P . (A /\ B))) <= 1 by PROB_1: 35;

      then ((P . A) + (P . B)) <= ((P . (A /\ B)) + 1) by XREAL_1: 20;

      hence thesis by XREAL_1: 20;

    end;

    theorem :: PROB_2:16

    

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

    proof

      ((P . (( [#] Sigma) \ A)) + (P . A)) = 1 by PROB_1: 31;

      hence thesis;

    end;

    theorem :: PROB_2:17

    

     Th17: (P . A) < 1 iff 0 < (P . (( [#] Sigma) \ A))

    proof

      thus (P . A) < 1 implies 0 < (P . (( [#] Sigma) \ A))

      proof

        assume (P . A) < 1;

        then (1 - (P . (( [#] Sigma) \ A))) < 1 by Th16;

        then (1 + ( - (P . (( [#] Sigma) \ A)))) < 1;

        then ( - (P . (( [#] Sigma) \ A))) < (1 - 1) by XREAL_1: 20;

        hence thesis;

      end;

      assume 0 < (P . (( [#] Sigma) \ A));

      then 0 < (1 - (P . A)) by PROB_1: 32;

      then ((P . A) + 0 ) < 1 by XREAL_1: 20;

      hence thesis;

    end;

    theorem :: PROB_2:18

    (P . (( [#] Sigma) \ A)) < 1 iff 0 < (P . A)

    proof

      thus (P . (( [#] Sigma) \ A)) < 1 implies 0 < (P . A)

      proof

        assume (P . (( [#] Sigma) \ A)) < 1;

        then (1 - (P . A)) < 1 by PROB_1: 32;

        then (1 + ( - (P . A))) < 1;

        then ( - (P . A)) < (1 - 1) by XREAL_1: 20;

        hence thesis;

      end;

      assume 0 < (P . A);

      then 0 < (1 - (P . (( [#] Sigma) \ A))) by Th16;

      then ((P . (( [#] Sigma) \ A)) + 0 ) < 1 by XREAL_1: 20;

      hence thesis;

    end;

    definition

      let Omega, Sigma, P, A, B;

      :: PROB_2:def4

      pred A,B are_independent_respect_to P means (P . (A /\ B)) = ((P . A) * (P . B));

      let C;

      :: PROB_2:def5

      pred A,B,C are_independent_respect_to P means (P . ((A /\ B) /\ C)) = (((P . A) * (P . B)) * (P . C)) & (P . (A /\ B)) = ((P . A) * (P . B)) & (P . (A /\ C)) = ((P . A) * (P . C)) & (P . (B /\ C)) = ((P . B) * (P . C));

    end

    theorem :: PROB_2:19

    (A,B) are_independent_respect_to P implies (B,A) are_independent_respect_to P;

    theorem :: PROB_2:20

    (A,B,C) are_independent_respect_to P iff (P . ((A /\ B) /\ C)) = (((P . A) * (P . B)) * (P . C)) & (A,B) are_independent_respect_to P & (B,C) are_independent_respect_to P & (A,C) are_independent_respect_to P;

    theorem :: PROB_2:21

    (A,B,C) are_independent_respect_to P implies (B,A,C) are_independent_respect_to P;

    theorem :: PROB_2:22

    (A,B,C) are_independent_respect_to P implies (A,C,B) are_independent_respect_to P by XBOOLE_1: 16;

    theorem :: PROB_2:23

    for E be Event of Sigma st E = {} holds (A,E) are_independent_respect_to P

    proof

      let E be Event of Sigma;

      

       A1: (P . (A /\ ( {} Sigma))) = ((P . A) * 0 ) by VALUED_0:def 19

      .= ((P . A) * (P . ( {} Sigma))) by VALUED_0:def 19;

      assume E = {} ;

      hence thesis by A1;

    end;

    theorem :: PROB_2:24

    (A,( [#] Sigma)) are_independent_respect_to P

    proof

      (P . (A /\ ( [#] Sigma))) = ((P . A) * 1) by XBOOLE_1: 28

      .= ((P . A) * (P . ( [#] Sigma))) by PROB_1: 30;

      hence thesis;

    end;

    theorem :: PROB_2:25

    

     Th25: for A, B, P st (A,B) are_independent_respect_to P holds (A,(( [#] Sigma) \ B)) are_independent_respect_to P

    proof

      let A, B, P;

      assume (A,B) are_independent_respect_to P;

      then

       A1: (P . (A /\ B)) = ((P . A) * (P . B));

      (P . (A /\ (( [#] Sigma) \ B))) = (P . (A /\ (B ` )))

      .= (P . (A \ B)) by SUBSET_1: 13

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

      .= (((P . A) * 1) - ((P . A) * (P . B))) by A1, PROB_1: 33, XBOOLE_1: 17

      .= ((P . A) * (1 - (P . B)))

      .= ((P . A) * (P . (( [#] Sigma) \ B))) by PROB_1: 32;

      hence thesis;

    end;

    theorem :: PROB_2:26

    

     Th26: (A,B) are_independent_respect_to P implies ((( [#] Sigma) \ A),(( [#] Sigma) \ B)) are_independent_respect_to P

    proof

      assume (A,B) are_independent_respect_to P;

      then (A,(( [#] Sigma) \ B)) are_independent_respect_to P by Th25;

      then ((( [#] Sigma) \ B),A) are_independent_respect_to P;

      then ((( [#] Sigma) \ B),(( [#] Sigma) \ A)) are_independent_respect_to P by Th25;

      hence thesis;

    end;

    theorem :: PROB_2:27

    for A, B, C, P st (A,B) are_independent_respect_to P & (A,C) are_independent_respect_to P & B misses C holds (A,(B \/ C)) are_independent_respect_to P

    proof

      let A, B, C, P;

      assume that

       A1: (A,B) are_independent_respect_to P and

       A2: (A,C) are_independent_respect_to P and

       A3: B misses C;

      

       A4: (A /\ B) misses (A /\ C) by A3, XBOOLE_1: 76;

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

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

      .= (((P . A) * (P . B)) + (P . (A /\ C))) by A1

      .= (((P . A) * (P . B)) + ((P . A) * (P . C))) by A2

      .= ((P . A) * ((P . B) + (P . C)))

      .= ((P . A) * (P . (B \/ C))) by A3, PROB_1:def 8;

      hence thesis;

    end;

    theorem :: PROB_2:28

    for P, A, B st (A,B) are_independent_respect_to P & (P . A) < 1 & (P . B) < 1 holds (P . (A \/ B)) < 1

    proof

       A1:

      now

        let r, r1;

        assume 0 < r1;

        then ( - r1) < ( - 0 ) by XREAL_1: 24;

        then (r + ( - r1)) < (r + 0 ) by XREAL_1: 6;

        hence (r - r1) < r;

      end;

      let P, A, B;

      assume that

       A2: (A,B) are_independent_respect_to P and

       A3: (P . A) < 1 & (P . B) < 1;

      

       A4: ((( [#] Sigma) \ A),(( [#] Sigma) \ B)) are_independent_respect_to P by A2, Th26;

      

       A5: 0 < (P . (( [#] Sigma) \ A)) & 0 < (P . (( [#] Sigma) \ B)) by A3, Th17;

      (P . (A \/ B)) = (1 - (P . (( [#] Sigma) \ (A \/ B)))) by Th16

      .= (1 - (P . ((( [#] Sigma) \ A) /\ (( [#] Sigma) \ B)))) by XBOOLE_1: 53

      .= (1 - ((P . (( [#] Sigma) \ A)) * (P . (( [#] Sigma) \ B)))) by A4;

      hence thesis by A5, A1, XREAL_1: 129;

    end;

    definition

      let Omega, Sigma, P, B;

      assume

       A1: 0 < (P . B);

      :: PROB_2:def6

      func P .|. B -> Probability of Sigma means

      : Def6: for A holds (it . A) = ((P . (A /\ B)) / (P . B));

      existence

      proof

        defpred P[ object, object] means ex A, r st (A = $1 & r = $2) & r = ((P . (A /\ B)) / (P . B));

        

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

        proof

          let x be object;

          assume x in Sigma;

          then

          reconsider x as Event of Sigma;

          consider y such that

           A3: y = ((P . (x /\ B)) / (P . B));

          take y;

          thus thesis by A3;

        end;

        consider f be Function of Sigma, REAL such that

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

        

         A5: for A holds (f . A) = ((P . (A /\ B)) / (P . B))

        proof

          let A;

          ex C, r1 st C = A & r1 = (f . A) & r1 = ((P . (C /\ B)) / (P . B)) by A4;

          hence thesis;

        end;

        

        then

         A6: (f . Omega) = ((P . (( [#] Sigma) /\ B)) / (P . B))

        .= ((P . B) / (P . B)) by XBOOLE_1: 28

        .= 1 by A1, XCMPLX_1: 60;

        

         A7: for A, C st A misses C holds (f . (A \/ C)) = ((f . A) + (f . C))

        proof

          let A, C;

          assume A misses C;

          then

           A8: (A /\ B) misses (C /\ B) by XBOOLE_1: 76;

          

          thus (f . (A \/ C)) = ((P . ((A \/ C) /\ B)) / (P . B)) by A5

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

          .= (((P . (A /\ B)) + (P . (C /\ B))) / (P . B)) by A8, PROB_1:def 8

          .= (((P . (A /\ B)) / (P . B)) + ((P . (C /\ B)) / (P . B))) by XCMPLX_1: 62

          .= (((P . (A /\ B)) / (P . B)) + (f . C)) by A5

          .= ((f . A) + (f . C)) by A5;

        end;

        

         A9: for A holds 0 <= (f . A)

        proof

          let A;

           0 <= (P . (A /\ B)) by PROB_1:def 8;

          then 0 <= ((P . (A /\ B)) / (P . B)) by A1;

          hence thesis by A5;

        end;

        for ASeq st ASeq is non-ascending holds (f * ASeq) is convergent & ( lim (f * ASeq)) = (f . ( Intersection ASeq))

        proof

          let ASeq such that

           A10: ASeq is non-ascending;

          consider BSeq such that

           A11: for n holds (BSeq . n) = ((ASeq . n) /\ B) by Th3;

          

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

           A13:

          now

            let n be object;

            assume

             A14: n in ( dom (f * ASeq));

            then

            reconsider n1 = n as Element of NAT by FUNCT_2:def 1;

            

            thus ((f * ASeq) . n) = (f . (ASeq . n)) by A12, A14, FUNCT_2: 15

            .= ((P . ((ASeq . n1) /\ B)) / (P . B)) by A5

            .= ((P . (BSeq . n)) / (P . B)) by A11

            .= (((P * BSeq) . n) / (P . B)) by A12, A14, FUNCT_2: 15

            .= (((P . B) " ) * ((P * BSeq) . n)) by XCMPLX_0:def 9;

          end;

          

           A15: BSeq is non-ascending by A10, A11, Th4;

          then

           A16: (P * BSeq) is convergent by PROB_1:def 8;

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

          then

           A17: (f * ASeq) = (((P . B) " ) (#) (P * BSeq)) by A12, A13, VALUED_1:def 5;

          hence (f * ASeq) is convergent by A16, SEQ_2: 7;

          ( lim (P * BSeq)) = (P . ( Intersection BSeq)) by A15, PROB_1:def 8;

          

          hence ( lim (f * ASeq)) = (((P . B) " ) * (P . ( @Intersection BSeq))) by A17, A16, SEQ_2: 8

          .= ((P . ( @Intersection BSeq)) / (P . B)) by XCMPLX_0:def 9

          .= ((P . (( @Intersection ASeq) /\ B)) / (P . B)) by A11, Th5

          .= (f . ( Intersection ASeq)) by A5;

        end;

        then

        reconsider f as Probability of Sigma by A9, A6, A7, PROB_1:def 8;

        take f;

        thus thesis by A5;

      end;

      uniqueness

      proof

        let P1, P2;

        assume that

         A18: for A holds (P1 . A) = ((P . (A /\ B)) / (P . B)) and

         A19: for A holds (P2 . A) = ((P . (A /\ B)) / (P . B));

        now

          let A;

          

          thus (P1 . A) = ((P . (A /\ B)) / (P . B)) by A18

          .= (P2 . A) by A19;

        end;

        hence thesis by Th9;

      end;

    end

    theorem :: PROB_2:29

    

     Th29: for P, B, A st 0 < (P . B) holds (P . (A /\ B)) = (((P .|. B) . A) * (P . B))

    proof

      let P, B, A;

      assume

       A1: 0 < (P . B);

      

      then (((P .|. B) . A) * (P . B)) = (((P . (A /\ B)) / (P . B)) * (P . B)) by Def6

      .= (((P . (A /\ B)) * ((P . B) " )) * (P . B)) by XCMPLX_0:def 9

      .= ((P . (A /\ B)) * (((P . B) " ) * (P . B)))

      .= ((P . (A /\ B)) * 1) by A1, XCMPLX_0:def 7

      .= (P . (A /\ B));

      hence thesis;

    end;

    theorem :: PROB_2:30

    for P, A, B, C st 0 < (P . (A /\ B)) holds (P . ((A /\ B) /\ C)) = (((P . A) * ((P .|. A) . B)) * ((P .|. (A /\ B)) . C))

    proof

      let P, A, B, C;

      assume

       A1: 0 < (P . (A /\ B));

      then

       A2: 0 < (P . A) by PROB_1: 34, XBOOLE_1: 17;

      (P . ((A /\ B) /\ C)) = ((P . (B /\ A)) * ((P .|. (A /\ B)) . C)) by A1, Th29

      .= (((P . A) * ((P .|. A) . B)) * ((P .|. (A /\ B)) . C)) by A2, Th29;

      hence thesis;

    end;

    theorem :: PROB_2:31

    

     Th31: for P, A, B, C st C = (B ` ) & 0 < (P . B) & 0 < (P . C) holds (P . A) = ((((P .|. B) . A) * (P . B)) + (((P .|. C) . A) * (P . C)))

    proof

      let P, A, B, C;

      assume that

       A1: C = (B ` ) and

       A2: 0 < (P . B) and

       A3: 0 < (P . C);

      (P . A) = ((P . (A /\ B)) + (P . (A /\ C))) by A1, Th14

      .= ((((P .|. B) . A) * (P . B)) + (P . (A /\ C))) by A2, Th29

      .= ((((P .|. B) . A) * (P . B)) + (((P .|. C) . A) * (P . C))) by A3, Th29;

      hence thesis;

    end;

    theorem :: PROB_2:32

    

     Th32: for P, A, A1, A2, A3 st A1 misses A2 & A3 = ((A1 \/ A2) ` ) & 0 < (P . A1) & 0 < (P . A2) & 0 < (P . A3) holds (P . A) = (((((P .|. A1) . A) * (P . A1)) + (((P .|. A2) . A) * (P . A2))) + (((P .|. A3) . A) * (P . A3)))

    proof

      let P, A, A1, A2, A3;

      assume that

       A1: A1 misses A2 and

       A2: A3 = ((A1 \/ A2) ` ) and

       A3: 0 < (P . A1) and

       A4: 0 < (P . A2) and

       A5: 0 < (P . A3);

      

       A6: (A /\ A1) misses (A /\ A2) by A1, XBOOLE_1: 76;

      (A1 \/ A2) misses A3 by A2, SUBSET_1: 24;

      then

       A7: (A /\ (A1 \/ A2)) misses (A /\ A3) by XBOOLE_1: 76;

      

       A8: ((A1 \/ A2) \/ A3) = ( [#] Omega) by A2, SUBSET_1: 10

      .= Omega;

      (((((P .|. A1) . A) * (P . A1)) + (((P .|. A2) . A) * (P . A2))) + (((P .|. A3) . A) * (P . A3))) = (((P . (A /\ A1)) + (((P .|. A2) . A) * (P . A2))) + (((P .|. A3) . A) * (P . A3))) by A3, Th29

      .= (((P . (A /\ A1)) + (P . (A /\ A2))) + (((P .|. A3) . A) * (P . A3))) by A4, Th29

      .= (((P . (A /\ A1)) + (P . (A /\ A2))) + (P . (A /\ A3))) by A5, Th29

      .= ((P . ((A /\ A1) \/ (A /\ A2))) + (P . (A /\ A3))) by A6, PROB_1:def 8

      .= ((P . (A /\ (A1 \/ A2))) + (P . (A /\ A3))) by XBOOLE_1: 23

      .= (P . ((A /\ (A1 \/ A2)) \/ (A /\ A3))) by A7, PROB_1:def 8

      .= (P . (A /\ Omega)) by A8, XBOOLE_1: 23

      .= (P . A) by XBOOLE_1: 28;

      hence thesis;

    end;

    theorem :: PROB_2:33

    for P, A, B st 0 < (P . B) holds (((P .|. B) . A) = (P . A) iff (A,B) are_independent_respect_to P)

    proof

      let P, A, B;

      assume

       A1: 0 < (P . B);

      thus ((P .|. B) . A) = (P . A) implies (A,B) are_independent_respect_to P

      proof

        assume ((P .|. B) . A) = (P . A);

        then (((P . (A /\ B)) / (P . B)) * (P . B)) = ((P . A) * (P . B)) by A1, Def6;

        then (P . (A /\ B)) = ((P . A) * (P . B)) by A1, XCMPLX_1: 87;

        hence thesis;

      end;

      assume (A,B) are_independent_respect_to P;

      then ((P . (A /\ B)) * ((P . B) " )) = (((P . A) * (P . B)) * ((P . B) " ));

      then ((P . (A /\ B)) * ((P . B) " )) = ((P . A) * ((P . B) * ((P . B) " )));

      then ((P . (A /\ B)) * ((P . B) " )) = ((P . A) * 1) by A1, XCMPLX_0:def 7;

      then ((P . (A /\ B)) / (P . B)) = (P . A) by XCMPLX_0:def 9;

      hence thesis by A1, Def6;

    end;

    theorem :: PROB_2:34

    for P, A, B st 0 < (P . B) & (P . B) < 1 & ((P .|. B) . A) = ((P .|. (( [#] Sigma) \ B)) . A) holds (A,B) are_independent_respect_to P

    proof

      let P, A, B;

      assume that

       A1: 0 < (P . B) and

       A2: (P . B) < 1 and

       A3: ((P .|. B) . A) = ((P .|. (( [#] Sigma) \ B)) . A);

       0 < (P . (( [#] Sigma) \ B)) & ((P . (A /\ B)) / (P . B)) = ((P .|. (( [#] Sigma) \ B)) . A) by A1, A2, A3, Def6, Th17;

      then

       A4: ((P . (A /\ B)) / (P . B)) = ((P . (A /\ (( [#] Sigma) \ B))) / (P . (( [#] Sigma) \ B))) by Def6;

      

       A5: (B ` ) = (( [#] Sigma) \ B);

      (P . (( [#] Sigma) \ B)) <> 0 by A2, Th17;

      then ((P . (A /\ B)) * (P . (( [#] Sigma) \ B))) = ((P . (A /\ (( [#] Sigma) \ B))) * (P . B)) by A1, A4, Th1;

      then ((P . (A /\ B)) * (1 - (P . B))) = ((P . (A /\ (( [#] Sigma) \ B))) * (P . B)) by PROB_1: 32;

      

      then (P . (A /\ B)) = (((P . (A /\ (( [#] Sigma) \ B))) + (P . (A /\ B))) * (P . B))

      .= ((P . A) * (P . B)) by A5, Th14;

      hence thesis;

    end;

    theorem :: PROB_2:35

    for P, A, B st 0 < (P . B) holds ((((P . A) + (P . B)) - 1) / (P . B)) <= ((P .|. B) . A)

    proof

      let P, A, B such that

       A1: 0 < (P . B);

      ((((P . A) + (P . B)) - 1) / (P . B)) <= ((P . (A /\ B)) / (P . B)) by A1, Th15, XREAL_1: 72;

      hence thesis by A1, Def6;

    end;

    theorem :: PROB_2:36

    

     Th36: for A, B, P st 0 < (P . A) & 0 < (P . B) holds ((P .|. B) . A) = ((((P .|. A) . B) * (P . A)) / (P . B))

    proof

      let A, B, P;

      assume that

       A1: 0 < (P . A) and

       A2: 0 < (P . B);

      

      thus ((((P .|. A) . B) * (P . A)) / (P . B)) = ((P . (A /\ B)) / (P . B)) by A1, Th29

      .= ((P .|. B) . A) by A2, Def6;

    end;

    ::$Notion-Name

    theorem :: PROB_2:37

    for B, A1, A2, P st 0 < (P . B) & A2 = (A1 ` ) & 0 < (P . A1) & 0 < (P . A2) holds ((P .|. B) . A1) = ((((P .|. A1) . B) * (P . A1)) / ((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2)))) & ((P .|. B) . A2) = ((((P .|. A2) . B) * (P . A2)) / ((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))))

    proof

      let B, A1, A2, P;

      assume that

       A1: 0 < (P . B) and

       A2: A2 = (A1 ` ) and

       A3: 0 < (P . A1) and

       A4: 0 < (P . A2);

      

      thus ((((P .|. A1) . B) * (P . A1)) / ((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2)))) = ((((P .|. A1) . B) * (P . A1)) / (P . B)) by A2, A3, A4, Th31

      .= ((P .|. B) . A1) by A1, A3, Th36;

      

      thus ((((P .|. A2) . B) * (P . A2)) / ((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2)))) = ((((P .|. A2) . B) * (P . A2)) / (P . B)) by A2, A3, A4, Th31

      .= ((P .|. B) . A2) by A1, A4, Th36;

    end;

    theorem :: PROB_2:38

    for B, A1, A2, A3, P st 0 < (P . B) & 0 < (P . A1) & 0 < (P . A2) & 0 < (P . A3) & A1 misses A2 & A3 = ((A1 \/ A2) ` ) holds ((P .|. B) . A1) = ((((P .|. A1) . B) * (P . A1)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3)))) & ((P .|. B) . A2) = ((((P .|. A2) . B) * (P . A2)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3)))) & ((P .|. B) . A3) = ((((P .|. A3) . B) * (P . A3)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))))

    proof

      let B, A1, A2, A3, P;

      assume that

       A1: 0 < (P . B) and

       A2: 0 < (P . A1) and

       A3: 0 < (P . A2) and

       A4: 0 < (P . A3) and

       A5: A1 misses A2 & A3 = ((A1 \/ A2) ` );

      

      thus ((((P .|. A1) . B) * (P . A1)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3)))) = ((((P .|. A1) . B) * (P . A1)) / (P . B)) by A2, A3, A4, A5, Th32

      .= ((P .|. B) . A1) by A1, A2, Th36;

      

      thus ((((P .|. A2) . B) * (P . A2)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3)))) = ((((P .|. A2) . B) * (P . A2)) / (P . B)) by A2, A3, A4, A5, Th32

      .= ((P .|. B) . A2) by A1, A3, Th36;

      

      thus ((((P .|. A3) . B) * (P . A3)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3)))) = ((((P .|. A3) . B) * (P . A3)) / (P . B)) by A2, A3, A4, A5, Th32

      .= ((P .|. B) . A3) by A1, A4, Th36;

    end;

    theorem :: PROB_2:39

    for A, B, P st 0 < (P . B) holds (1 - ((P . (( [#] Sigma) \ A)) / (P . B))) <= ((P .|. B) . A)

    proof

      let A, B, P;

      assume

       A1: 0 < (P . B);

      (((P . B) + (P . A)) - 1) <= (P . (A /\ B)) by Th15;

      then ((P . B) + ( - (1 - (P . A)))) <= (P . (A /\ B));

      then ((P . B) + ( - (P . (( [#] Sigma) \ A)))) <= (P . (A /\ B)) by PROB_1: 32;

      then (((P . B) + ( - (P . (( [#] Sigma) \ A)))) / (P . B)) <= ((P . (A /\ B)) / (P . B)) by A1, XREAL_1: 72;

      then (((P . B) - (P . (( [#] Sigma) \ A))) / (P . B)) <= ((P .|. B) . A) by A1, Def6;

      then (((P . B) / (P . B)) - ((P . (( [#] Sigma) \ A)) / (P . B))) <= ((P .|. B) . A) by XCMPLX_1: 120;

      hence thesis by A1, XCMPLX_1: 60;

    end;