rpr_1.miz



    begin

    reserve E for non empty set;

    reserve a for Element of E;

    reserve A,B for Subset of E;

    reserve Y for set;

    reserve p for FinSequence;

    theorem :: RPR_1:1

    

     Th1: for e be non empty Subset of E holds e is Singleton of E iff for Y holds (Y c= e iff Y = {} or Y = e)

    proof

      let e be non empty Subset of E;

      thus e is Singleton of E implies for Y holds (Y c= e iff Y = {} or Y = e)

      proof

        assume

         A1: e is Singleton of E;

        let Y;

        ex x be object st e = {x} by A1, ZFMISC_1: 131;

        hence thesis by ZFMISC_1: 33;

      end;

      assume

       A2: for Y holds Y c= e iff Y = {} or Y = e;

      consider x be object such that

       A3: x in e by XBOOLE_0:def 1;

       {x} c= e by A3, ZFMISC_1: 31;

      hence thesis by A2;

    end;

    registration

      let E;

      cluster -> finite for Singleton of E;

      coherence ;

    end

    reserve e,e1,e2 for Singleton of E;

    theorem :: RPR_1:2

    e = (A \/ B) & A <> B implies A = {} & B = e or A = e & B = {}

    proof

      assume that

       A1: e = (A \/ B) and

       A2: A <> B;

      A c= e by A1, XBOOLE_1: 7;

      then

       A3: A = {} or A = e by Th1;

      B c= e by A1, XBOOLE_1: 7;

      hence thesis by A2, A3, Th1;

    end;

    theorem :: RPR_1:3

    e = (A \/ B) implies A = e & B = e or A = e & B = {} or A = {} & B = e

    proof

      assume

       A1: e = (A \/ B);

      then A c= e & B c= e by XBOOLE_1: 7;

      then A = {} & B = e or A = e & B = {} or A = e & B = e or A = {} & B = {} by Th1;

      hence thesis by A1;

    end;

    theorem :: RPR_1:4

     {a} is Singleton of E;

    theorem :: RPR_1:5

    e1 c= e2 implies e1 = e2 by Th1;

    theorem :: RPR_1:6

    

     Th6: ex a st a in E & e = {a}

    proof

      set x = the Element of e;

       {x} = e by Th1;

      hence thesis;

    end;

    theorem :: RPR_1:7

    ex e st e is Singleton of E

    proof

      take { the Element of E};

      thus thesis;

    end;

    theorem :: RPR_1:8

    ex p st p is FinSequence of E & ( rng p) = e & ( len p) = 1

    proof

      consider a such that a in E and

       A1: e = {a} by Th6;

      ( rng <*a*>) = {a} & ( len <*a*>) = 1 by FINSEQ_1: 39;

      hence thesis by A1;

    end;

    definition

      let E be set;

      mode Event of E is Subset of E;

    end

    theorem :: RPR_1:9

    for E be non empty set, e be Singleton of E, A be Event of E holds e misses A or (e /\ A) = e

    proof

      let E be non empty set, e be Singleton of E, A be Event of E;

      (e /\ E) = e & (A \/ (A ` )) = ( [#] E) by SUBSET_1: 10, XBOOLE_1: 28;

      then e = ((e /\ A) \/ (e /\ (A ` ))) by XBOOLE_1: 23;

      then (e /\ A) c= e by XBOOLE_1: 7;

      then (e /\ A) = {} or (e /\ A) = e by Th1;

      hence thesis;

    end;

    theorem :: RPR_1:10

    for E be non empty set, A be Event of E st A <> {} holds ex e be Singleton of E st e c= A

    proof

      let E be non empty set, A be Event of E;

      set x = the Element of A;

      assume

       A1: A <> {} ;

      then

      reconsider x as Element of E by TARSKI:def 3;

       {x} c= A by A1, ZFMISC_1: 31;

      hence thesis;

    end;

    theorem :: RPR_1:11

    for E be non empty set, e be Singleton of E, A be Event of E st e c= (A \/ (A ` )) holds e c= A or e c= (A ` )

    proof

      let E be non empty set, e be Singleton of E, A be Event of E;

      ex a be Element of E st a in E & e = {a} by Th6;

      then

      consider a be Element of E such that

       A1: e = {a};

      assume e c= (A \/ (A ` ));

      then a in (A \/ (A ` )) by A1, ZFMISC_1: 31;

      then a in A or a in (A ` ) by XBOOLE_0:def 3;

      hence thesis by A1, ZFMISC_1: 31;

    end;

    theorem :: RPR_1:12

    e1 = e2 or e1 misses e2

    proof

      (e1 /\ e2) c= e1 by XBOOLE_1: 17;

      then (e1 /\ e2) = {} or (e1 /\ e2) = e1 by Th1;

      then e1 c= e2 or (e1 /\ e2) = {} by XBOOLE_1: 17;

      hence thesis by Th1;

    end;

    theorem :: RPR_1:13

    

     Th13: (A /\ B) misses (A /\ (B ` ))

    proof

      (A /\ B) misses (A \ B) by XBOOLE_1: 89;

      hence thesis by SUBSET_1: 13;

    end;

    

     Lm1: for E be finite non empty set holds 0 < ( card E)

    proof

      let E be finite non empty set;

      ( card { the Element of E}) <= ( card E) by NAT_1: 43;

      hence thesis by CARD_1: 30;

    end;

    definition

      let E be finite set;

      let A be Event of E;

      :: RPR_1:def1

      func prob (A) -> Real equals (( card A) / ( card E));

      coherence ;

    end

    theorem :: RPR_1:14

    for E be finite non empty set, e be Singleton of E holds ( prob e) = (1 / ( card E)) by CARD_1:def 7;

    theorem :: RPR_1:15

    for E be finite non empty set holds ( prob ( [#] E)) = 1 by XCMPLX_1: 60;

    theorem :: RPR_1:16

    

     Th16: for E be finite non empty set, A,B be Event of E st A misses B holds ( prob (A /\ B)) = 0 by CARD_1: 27;

    theorem :: RPR_1:17

    for E be finite non empty set, A be Event of E holds ( prob A) <= 1

    proof

      let E be finite non empty set, A be Event of E;

       0 < ( card E) by Lm1;

      then (( card A) * (( card E) " )) <= (( card E) * (( card E) " )) by NAT_1: 43, XREAL_1: 64;

      then (( card A) / ( card E)) <= (( card E) * (( card E) " )) by XCMPLX_0:def 9;

      then ( prob ( [#] E)) = (( card E) / ( card E)) & ( prob A) <= (( card E) / ( card E)) by XCMPLX_0:def 9;

      hence thesis by XCMPLX_1: 60;

    end;

    theorem :: RPR_1:18

    

     Th18: for E be finite non empty set, A be Event of E holds 0 <= ( prob A)

    proof

      let E be finite non empty set, A be Event of E;

       0 < ( card E) & 0 <= ( card A) by Lm1, CARD_1: 27;

      hence thesis;

    end;

    theorem :: RPR_1:19

    

     Th19: for E be finite non empty set, A,B be Event of E st A c= B holds ( prob A) <= ( prob B)

    proof

      let E be finite non empty set, A,B be Event of E;

      assume

       A1: A c= B;

       0 < ( card E) by Lm1;

      then (( card A) * (( card E) " )) <= (( card B) * (( card E) " )) by A1, NAT_1: 43, XREAL_1: 64;

      then (( card A) / ( card E)) <= (( card B) * (( card E) " )) by XCMPLX_0:def 9;

      hence thesis by XCMPLX_0:def 9;

    end;

    theorem :: RPR_1:20

    

     Th20: for E be finite non empty set, A,B be Event of E holds ( prob (A \/ B)) = ((( prob A) + ( prob B)) - ( prob (A /\ B)))

    proof

      let E be finite non empty set, A,B be Event of E;

      set q = (( card E) " );

      set p = ( card E);

      ( card (A \/ B) qua Event of E) = ((( card A) + ( card B)) - ( card (A /\ B))) by CARD_2: 45;

      then (( card (A \/ B)) * q) = ((( card A) * q) + ((( card B) * q) - (( card (A /\ B)) * q)));

      then (( card (A \/ B)) / p) = (((( card A) * q) + (( card B) * q)) - (( card (A /\ B)) * q)) by XCMPLX_0:def 9;

      then (( card (A \/ B)) / p) = (((( card A) / p) + (( card B) * q)) - (( card (A /\ B)) * q)) by XCMPLX_0:def 9;

      then (( card (A \/ B)) / p) = (((( card A) / p) + (( card B) / p)) - (( card (A /\ B)) * q)) by XCMPLX_0:def 9;

      hence thesis by XCMPLX_0:def 9;

    end;

    theorem :: RPR_1:21

    

     Th21: for E be finite non empty set, A,B be Event of E st A misses B holds ( prob (A \/ B)) = (( prob A) + ( prob B))

    proof

      let E be finite non empty set, A,B be Event of E;

      assume A misses B;

      then ( prob (A /\ B)) = 0 by Th16;

      then ( prob (A \/ B)) = ((( prob A) + ( prob B)) - 0 ) by Th20;

      hence thesis;

    end;

    theorem :: RPR_1:22

    

     Th22: for E be finite non empty set, A be Event of E holds ( prob A) = (1 - ( prob (A ` ))) & ( prob (A ` )) = (1 - ( prob A))

    proof

      let E be finite non empty set, A be Event of E;

      A misses (A ` ) by SUBSET_1: 24;

      then ( prob (A \/ (A ` ))) = (( prob A) + ( prob (A ` ))) by Th21;

      then ( prob ( [#] E)) = (( prob A) + ( prob (A ` ))) by SUBSET_1: 10;

      then 1 = (( prob A) + ( prob (A ` ))) by XCMPLX_1: 60;

      hence thesis;

    end;

    theorem :: RPR_1:23

    

     Th23: for E be finite non empty set, A,B be Event of E holds ( prob (A \ B)) = (( prob A) - ( prob (A /\ B)))

    proof

      let E be finite non empty set, A,B be Event of E;

      ( prob A) = ( prob ((A \ B) \/ (A /\ B))) by XBOOLE_1: 51;

      then ( prob A) = (( prob (A \ B)) + ( prob (A /\ B))) by Th21, XBOOLE_1: 89;

      hence thesis;

    end;

    theorem :: RPR_1:24

    

     Th24: for E be finite non empty set, A,B be Event of E st B c= A holds ( prob (A \ B)) = (( prob A) - ( prob B))

    proof

      let E be finite non empty set, A,B be Event of E;

      assume B c= A;

      then ( prob (A /\ B)) = ( prob B) by XBOOLE_1: 28;

      hence thesis by Th23;

    end;

    theorem :: RPR_1:25

    for E be finite non empty set, A,B be Event of E holds ( prob (A \/ B)) <= (( prob A) + ( prob B))

    proof

      let E be finite non empty set, A,B be Event of E;

      ( prob (A \/ B)) = ((( prob A) + ( prob B)) - ( prob (A /\ B))) by Th20;

      hence thesis by Th18, XREAL_1: 43;

    end;

    theorem :: RPR_1:26

    

     Th26: for E be finite non empty set, A,B be Event of E holds ( prob A) = (( prob (A /\ B)) + ( prob (A /\ (B ` ))))

    proof

      let E be finite non empty set, A,B be Event of E;

      A = (A /\ (A \/ ( [#] E))) by XBOOLE_1: 21;

      then A = (A /\ ( [#] E)) by SUBSET_1: 11;

      then

       A1: A = (A /\ (B \/ (B ` ))) by SUBSET_1: 10;

      ( prob ((A /\ B) \/ (A /\ (B ` )))) = (( prob (A /\ B)) + ( prob (A /\ (B ` )))) by Th13, Th21;

      hence thesis by A1, XBOOLE_1: 23;

    end;

    theorem :: RPR_1:27

    for E be finite non empty set, A,B be Event of E holds ( prob A) = (( prob (A \/ B)) - ( prob (B \ A)))

    proof

      let E be finite non empty set, A,B be Event of E;

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

      then ( prob (A \/ B)) = (( prob A) + ( prob (B \ A))) by Th21, XBOOLE_1: 79;

      hence thesis;

    end;

    theorem :: RPR_1:28

    for E be finite non empty set, A,B be Event of E holds (( prob A) + ( prob ((A ` ) /\ B))) = (( prob B) + ( prob ((B ` ) /\ A)))

    proof

      let E be finite non empty set, A,B be Event of E;

      ( prob A) = (( prob (A /\ B)) + ( prob (A /\ (B ` )))) & ( prob B) = (( prob (A /\ B)) + ( prob (B /\ (A ` )))) by Th26;

      hence thesis;

    end;

    theorem :: RPR_1:29

    

     Th29: for E be finite non empty set, A,B,C be Event of E holds ( prob ((A \/ B) \/ C)) = ((((( prob A) + ( prob B)) + ( prob C)) - ((( prob (A /\ B)) + ( prob (A /\ C))) + ( prob (B /\ C)))) + ( prob ((A /\ B) /\ C)))

    proof

      let E be finite non empty set, A,B,C be Event of E;

      ( prob ((A \/ B) \/ C)) = ((( prob (A \/ B)) + ( prob C)) - ( prob ((A \/ B) /\ C))) by Th20

      .= ((((( prob A) + ( prob B)) - ( prob (A /\ B))) + ( prob C)) - ( prob ((A \/ B) /\ C))) by Th20

      .= ((((( prob A) + ( prob B)) + ( prob C)) + ( - ( prob (A /\ B)))) - ( prob ((A /\ C) \/ (B /\ C)))) by XBOOLE_1: 23

      .= ((((( prob A) + ( prob B)) + ( prob C)) + ( - ( prob (A /\ B)))) - ((( prob (A /\ C)) + ( prob (B /\ C))) - ( prob ((A /\ C) /\ (B /\ C))))) by Th20

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

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

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

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

      hence thesis;

    end;

    theorem :: RPR_1:30

    for E be finite non empty set, A,B,C be Event of E st A misses B & A misses C & B misses C holds ( prob ((A \/ B) \/ C)) = ((( prob A) + ( prob B)) + ( prob C))

    proof

      let E be finite non empty set, A,B,C be Event of E;

      assume that

       A1: A misses B and

       A2: A misses C and

       A3: B misses C;

      

       A4: ( prob (A /\ (B /\ C))) = 0 by A1, Th16, XBOOLE_1: 74;

      ( prob ((A \/ B) \/ C)) = ((((( prob A) + ( prob B)) + ( prob C)) - ((( prob (A /\ B)) + ( prob (A /\ C))) + ( prob (B /\ C)))) + ( prob ((A /\ B) /\ C))) by Th29

      .= ((((( prob A) + ( prob B)) + ( prob C)) - ((( prob (A /\ B)) + ( prob (A /\ C))) + ( prob (B /\ C)))) + 0 ) by A4, XBOOLE_1: 16

      .= (((( prob A) + ( prob B)) + ( prob C)) - ((( prob (A /\ B)) + ( prob (A /\ C))) + 0 )) by A3, Th16

      .= (((( prob A) + ( prob B)) + ( prob C)) - (( prob (A /\ B)) + 0 )) by A2, Th16

      .= (((( prob A) + ( prob B)) + ( prob C)) - 0 ) by A1, Th16;

      hence thesis;

    end;

    theorem :: RPR_1:31

    for E be finite non empty set, A,B be Event of E holds (( prob A) - ( prob B)) <= ( prob (A \ B))

    proof

      let E be finite non empty set, A,B be Event of E;

      ( prob (A /\ B)) <= ( prob B) by Th19, XBOOLE_1: 17;

      then (( prob A) - ( prob B)) <= (( prob A) - ( prob (A /\ B))) by XREAL_1: 13;

      hence thesis by Th23;

    end;

    definition

      let E be finite set;

      let B,A be Event of E;

      :: RPR_1:def2

      func prob (A,B) -> Real equals (( prob (A /\ B)) / ( prob B));

      coherence ;

    end

    theorem :: RPR_1:32

    for E be finite non empty set, A be Event of E holds ( prob (A,( [#] E))) = ( prob A)

    proof

      let E be finite non empty set, A be Event of E;

      ( prob ( [#] E)) = 1 by XCMPLX_1: 60;

      hence thesis by XBOOLE_1: 28;

    end;

    theorem :: RPR_1:33

    for E be finite non empty set holds ( prob (( [#] E),( [#] E))) = 1

    proof

      let E be finite non empty set;

      ( prob ( [#] E)) = 1 by XCMPLX_1: 60;

      hence thesis;

    end;

    theorem :: RPR_1:34

    for E be finite non empty set, A,B be Event of E st 0 < ( prob B) holds ( prob (A,B)) <= 1

    proof

      let E be finite non empty set, A,B be Event of E;

      assume

       A1: 0 < ( prob B);

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

      then (( prob (A /\ B)) * (( prob B) " )) <= (( prob B) * (( prob B) " )) by A1, Th19, XREAL_1: 64;

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

      hence thesis by XCMPLX_0:def 9;

    end;

    theorem :: RPR_1:35

    for E be finite non empty set, A,B be Event of E st 0 < ( prob B) holds 0 <= ( prob (A,B))

    proof

      let E be finite non empty set, A,B be Event of E;

      assume

       A1: 0 < ( prob B);

       0 <= ( prob (A /\ B)) by Th18;

      hence thesis by A1;

    end;

    theorem :: RPR_1:36

    

     Th36: for E be finite non empty set, A,B be Event of E st 0 < ( prob B) holds ( prob (A,B)) = (1 - (( prob (B \ A)) / ( prob B)))

    proof

      let E be finite non empty set, A,B be Event of E;

      (( prob (B \ A)) + ( prob (A /\ B))) = ((( prob B) - ( prob (A /\ B))) + ( prob (A /\ B))) by Th23;

      then ( prob (A,B)) = ((( prob B) - ( prob (B \ A))) / ( prob B));

      then

       A1: ( prob (A,B)) = ((( prob B) / ( prob B)) - (( prob (B \ A)) / ( prob B))) by XCMPLX_1: 120;

      assume 0 < ( prob B);

      hence thesis by A1, XCMPLX_1: 60;

    end;

    theorem :: RPR_1:37

    for E be finite non empty set, A,B be Event of E st 0 < ( prob B) & A c= B holds ( prob (A,B)) = (( prob A) / ( prob B))

    proof

      let E be finite non empty set, A,B be Event of E;

      assume that

       A1: 0 < ( prob B) and

       A2: A c= B;

      ( prob (A,B)) = (1 - (( prob (B \ A)) / ( prob B))) by A1, Th36;

      then ( prob (A,B)) = (1 - ((( prob B) - ( prob A)) / ( prob B))) by A2, Th24;

      then ( prob (A,B)) = (1 - ((( prob B) / ( prob B)) - (( prob A) / ( prob B)))) by XCMPLX_1: 120;

      then ( prob (A,B)) = (1 - (1 - (( prob A) / ( prob B)))) by A1, XCMPLX_1: 60;

      hence thesis;

    end;

    theorem :: RPR_1:38

    

     Th38: for E be finite non empty set, A,B be Event of E st A misses B holds ( prob (A,B)) = 0

    proof

      let E be finite non empty set, A,B be Event of E;

      assume A misses B;

      

      then ( prob (A,B)) = ( 0 / ( prob B)) by Th16

      .= ( 0 * (( prob B) " ));

      hence thesis;

    end;

    theorem :: RPR_1:39

    

     Th39: for E be finite non empty set, A,B be Event of E st 0 < ( prob A) & 0 < ( prob B) holds (( prob A) * ( prob (B,A))) = (( prob B) * ( prob (A,B)))

    proof

      let E be finite non empty set, A,B be Event of E;

      assume that

       A1: 0 < ( prob A) and

       A2: 0 < ( prob B);

      (( prob A) * ( prob (B,A))) = ( prob (A /\ B)) by A1, XCMPLX_1: 87;

      hence thesis by A2, XCMPLX_1: 87;

    end;

    theorem :: RPR_1:40

    

     Th40: for E be finite non empty set, A,B be Event of E st 0 < ( prob B) holds ( prob (A,B)) = (1 - ( prob ((A ` ),B))) & ( prob ((A ` ),B)) = (1 - ( prob (A,B)))

    proof

      let E be finite non empty set, A,B be Event of E;

      assume

       A1: 0 < ( prob B);

      ((A \/ (A ` )) /\ B) = (( [#] E) /\ B) & (( [#] E) /\ B) = B by SUBSET_1: 10, XBOOLE_1: 28;

      then ((A /\ B) \/ ((A ` ) /\ B)) = B by XBOOLE_1: 23;

      then (( prob (A /\ B)) + ( prob ((A ` ) /\ B))) = ( prob B) by Th13, Th21;

      then ((( prob (A,B)) * ( prob B)) + ( prob ((A ` ) /\ B))) = ( prob B) by A1, XCMPLX_1: 87;

      then ((( prob (A,B)) * ( prob B)) + (( prob ((A ` ),B)) * ( prob B))) = ( prob B) by A1, XCMPLX_1: 87;

      then (((( prob (A,B)) + ( prob ((A ` ),B))) * ( prob B)) * (( prob B) " )) = 1 by A1, XCMPLX_0:def 7;

      then ((( prob (A,B)) + ( prob ((A ` ),B))) * (( prob B) * (( prob B) " ))) = 1;

      then ((( prob (A,B)) + ( prob ((A ` ),B))) * 1) = 1 by A1, XCMPLX_0:def 7;

      hence thesis;

    end;

    theorem :: RPR_1:41

    

     Th41: for E be finite non empty set, A,B be Event of E st 0 < ( prob B) & B c= A holds ( prob (A,B)) = 1

    proof

      let E be finite non empty set, A,B be Event of E;

      assume that

       A1: 0 < ( prob B) and

       A2: B c= A;

      ( prob (A /\ B)) = ( prob B) by A2, XBOOLE_1: 28;

      hence thesis by A1, XCMPLX_1: 60;

    end;

    theorem :: RPR_1:42

    for E be finite non empty set, B be Event of E st 0 < ( prob B) holds ( prob (( [#] E),B)) = 1 by Th41;

    theorem :: RPR_1:43

    for E be finite non empty set, A be Event of E holds ( prob ((A ` ),A)) = 0

    proof

      let E be finite non empty set, A be Event of E;

      (A ` ) misses A by SUBSET_1: 24;

      then ( prob ((A ` ) /\ A)) = 0 by Th16;

      hence thesis;

    end;

    theorem :: RPR_1:44

    for E be finite non empty set, A be Event of E holds ( prob (A,(A ` ))) = 0

    proof

      let E be finite non empty set, A be Event of E;

      A misses (A ` ) by SUBSET_1: 24;

      then ( prob (A /\ (A ` ))) = 0 by Th16;

      hence thesis;

    end;

    theorem :: RPR_1:45

    

     Th45: for E be finite non empty set, A,B be Event of E st 0 < ( prob B) & A misses B holds ( prob ((A ` ),B)) = 1

    proof

      let E be finite non empty set, A,B be Event of E;

      assume that

       A1: 0 < ( prob B) and

       A2: A misses B;

      ( prob (A,B)) = 0 by A2, Th38;

      then (1 - ( prob ((A ` ),B))) = 0 by A1, Th40;

      hence thesis;

    end;

    theorem :: RPR_1:46

    

     Th46: for E be finite non empty set, A,B be Event of E st 0 < ( prob A) & ( prob B) < 1 & A misses B holds ( prob (A,(B ` ))) = (( prob A) / (1 - ( prob B)))

    proof

      let E be finite non empty set, A,B be Event of E;

      assume that

       A1: 0 < ( prob A) and

       A2: ( prob B) < 1 and

       A3: A misses B;

      (( prob B) - 1) < (1 - 1) by A2, XREAL_1: 9;

      then 0 < ( - ( - (1 - ( prob B))));

      then

       A4: 0 < ( prob (B ` )) by Th22;

      then (( prob A) * ( prob ((B ` ),A))) = (( prob (B ` )) * ( prob (A,(B ` )))) by A1, Th39;

      then (( prob A) * 1) = (( prob (B ` )) * ( prob (A,(B ` )))) by A1, A3, Th45;

      then (( prob A) * (( prob (B ` )) " )) = (( prob (A,(B ` ))) * (( prob (B ` )) * (( prob (B ` )) " )));

      then

       A5: (( prob A) * (( prob (B ` )) " )) = (( prob (A,(B ` ))) * 1) by A4, XCMPLX_0:def 7;

      ( prob (B ` )) = (1 - ( prob B)) by Th22;

      hence thesis by A5, XCMPLX_0:def 9;

    end;

    theorem :: RPR_1:47

    for E be finite non empty set, A,B be Event of E st 0 < ( prob A) & ( prob B) < 1 & A misses B holds ( prob ((A ` ),(B ` ))) = (1 - (( prob A) / (1 - ( prob B))))

    proof

      let E be finite non empty set, A,B be Event of E;

      assume that

       A1: 0 < ( prob A) and

       A2: ( prob B) < 1 and

       A3: A misses B;

      

       A4: ( prob (B ` )) = (1 - ( prob B)) by Th22;

      (( prob B) - 1) < (1 - 1) by A2, XREAL_1: 9;

      then 0 < ( - ( - (1 - ( prob B))));

      then ( prob ((A ` ),(B ` ))) = (1 - ( prob (A,(B ` )))) by A4, Th40;

      hence thesis by A1, A2, A3, Th46;

    end;

    theorem :: RPR_1:48

    for E be finite non empty set, A,B,C be Event of E st 0 < ( prob (B /\ C)) & 0 < ( prob C) holds ( prob ((A /\ B) /\ C)) = ((( prob (A,(B /\ C))) * ( prob (B,C))) * ( prob C))

    proof

      let E be finite non empty set, A,B,C be Event of E;

      assume that

       A1: 0 < ( prob (B /\ C)) and

       A2: 0 < ( prob C);

      

       A3: ( prob (B /\ C)) = (( prob (B,C)) * ( prob C)) by A2, XCMPLX_1: 87;

      ( prob ((A /\ B) /\ C)) = ( prob (A /\ (B /\ C))) by XBOOLE_1: 16;

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

      hence thesis by A3;

    end;

    theorem :: RPR_1:49

    

     Th49: for E be finite non empty set, A,B be Event of E st 0 < ( prob B) & ( prob B) < 1 holds ( prob A) = ((( prob (A,B)) * ( prob B)) + (( prob (A,(B ` ))) * ( prob (B ` ))))

    proof

      let E be finite non empty set, A,B be Event of E;

      assume that

       A1: 0 < ( prob B) and

       A2: ( prob B) < 1;

      (( prob B) - 1) < (1 - 1) by A2, XREAL_1: 9;

      then 0 < ( - ( - (1 - ( prob B))));

      then

       A3: 0 < ( prob (B ` )) by Th22;

      ( prob A) = (( prob (A /\ B)) + ( prob (A /\ (B ` )))) by Th26;

      then ( prob A) = ((( prob (A,B)) * ( prob B)) + ( prob (A /\ (B ` )))) by A1, XCMPLX_1: 87;

      hence thesis by A3, XCMPLX_1: 87;

    end;

    theorem :: RPR_1:50

    

     Th50: for E be finite non empty set, A,B1,B2 be Event of E st 0 < ( prob B1) & 0 < ( prob B2) & (B1 \/ B2) = E & B1 misses B2 holds ( prob A) = ((( prob (A,B1)) * ( prob B1)) + (( prob (A,B2)) * ( prob B2)))

    proof

      let E be finite non empty set, A,B1,B2 be Event of E;

      assume that

       A1: 0 < ( prob B1) and

       A2: 0 < ( prob B2) and

       A3: (B1 \/ B2) = E and

       A4: B1 misses B2;

      

       A5: (B2 \ B1) = (E \ B1) by A3, XBOOLE_1: 40;

      then 0 < ( prob (B1 ` )) by A2, A4, XBOOLE_1: 83;

      then 0 < (1 - ( prob B1)) by Th22;

      then

       A6: (1 - (1 - ( prob B1))) < 1 by XREAL_1: 44;

      B2 = (B1 ` ) by A4, A5, XBOOLE_1: 83;

      hence thesis by A1, A6, Th49;

    end;

    theorem :: RPR_1:51

    

     Th51: for E be finite non empty set, A,B1,B2,B3 be Event of E st 0 < ( prob B1) & 0 < ( prob B2) & 0 < ( prob B3) & ((B1 \/ B2) \/ B3) = E & B1 misses B2 & B1 misses B3 & B2 misses B3 holds ( prob A) = (((( prob (A,B1)) * ( prob B1)) + (( prob (A,B2)) * ( prob B2))) + (( prob (A,B3)) * ( prob B3)))

    proof

      let E be finite non empty set, A,B1,B2,B3 be Event of E;

      assume that

       A1: 0 < ( prob B1) and

       A2: 0 < ( prob B2) and

       A3: 0 < ( prob B3) and

       A4: ((B1 \/ B2) \/ B3) = E and

       A5: (B1 /\ B2) = {} and

       A6: (B1 /\ B3) = {} and

       A7: (B2 /\ B3) = {} ;

      ((B1 /\ B3) \/ (B2 /\ B3)) = (B2 /\ B3) by A6;

      then ((B1 \/ B2) /\ B3) = {} by A7, XBOOLE_1: 23;

      then

       A8: (B1 \/ B2) misses B3;

      (((B1 \/ B2) \/ B3) /\ A) = A by A4, XBOOLE_1: 28;

      then (((B1 \/ B2) /\ A) \/ (B3 /\ A)) = A by XBOOLE_1: 23;

      then ( prob A) = (( prob ((B1 \/ B2) /\ A)) + ( prob (B3 /\ A))) by A8, Th21, XBOOLE_1: 76;

      then

       A9: ( prob A) = (( prob ((B1 /\ A) \/ (B2 /\ A))) + ( prob (B3 /\ A))) by XBOOLE_1: 23;

      B1 misses B2 by A5;

      then ( prob A) = ((( prob (A /\ B1)) + ( prob (A /\ B2))) + ( prob (A /\ B3))) by A9, Th21, XBOOLE_1: 76;

      then ( prob A) = (((( prob (A,B1)) * ( prob B1)) + ( prob (A /\ B2))) + ( prob (A /\ B3))) by A1, XCMPLX_1: 87;

      then ( prob A) = (((( prob (A,B1)) * ( prob B1)) + (( prob (A,B2)) * ( prob B2))) + ( prob (A /\ B3))) by A2, XCMPLX_1: 87;

      hence thesis by A3, XCMPLX_1: 87;

    end;

    theorem :: RPR_1:52

    for E be finite non empty set, A,B1,B2 be Event of E st 0 < ( prob B1) & 0 < ( prob B2) & (B1 \/ B2) = E & B1 misses B2 holds ( prob (B1,A)) = ((( prob (A,B1)) * ( prob B1)) / ((( prob (A,B1)) * ( prob B1)) + (( prob (A,B2)) * ( prob B2))))

    proof

      let E be finite non empty set, A,B1,B2 be Event of E;

      assume that

       A1: 0 < ( prob B1) and

       A2: 0 < ( prob B2) & (B1 \/ B2) = E & B1 misses B2;

      ( prob A) = ((( prob (A,B1)) * ( prob B1)) + (( prob (A,B2)) * ( prob B2))) by A1, A2, Th50;

      hence thesis by A1, XCMPLX_1: 87;

    end;

    theorem :: RPR_1:53

    for E be finite non empty set, A,B1,B2,B3 be Event of E st 0 < ( prob B1) & 0 < ( prob B2) & 0 < ( prob B3) & ((B1 \/ B2) \/ B3) = E & B1 misses B2 & B1 misses B3 & B2 misses B3 holds ( prob (B1,A)) = ((( prob (A,B1)) * ( prob B1)) / (((( prob (A,B1)) * ( prob B1)) + (( prob (A,B2)) * ( prob B2))) + (( prob (A,B3)) * ( prob B3))))

    proof

      let E be finite non empty set, A,B1,B2,B3 be Event of E;

      assume that

       A1: 0 < ( prob B1) and

       A2: 0 < ( prob B2) & 0 < ( prob B3) & ((B1 \/ B2) \/ B3) = E & B1 misses B2 & B1 misses B3 & B2 misses B3;

      ( prob A) = (((( prob (A,B1)) * ( prob B1)) + (( prob (A,B2)) * ( prob B2))) + (( prob (A,B3)) * ( prob B3))) by A1, A2, Th51;

      hence thesis by A1, XCMPLX_1: 87;

    end;

    definition

      let E be finite set;

      let A,B be Event of E;

      :: RPR_1:def3

      pred A,B are_independent means ( prob (A /\ B)) = (( prob A) * ( prob B));

      symmetry ;

    end

    theorem :: RPR_1:54

    for E be finite non empty set, A,B be Event of E st 0 < ( prob B) & (A,B) are_independent holds ( prob (A,B)) = ( prob A)

    proof

      let E be finite non empty set, A,B be Event of E;

      assume that

       A1: 0 < ( prob B) and

       A2: (A,B) are_independent ;

      ( prob (A /\ B)) = (( prob A) * ( prob B)) by A2;

      then ( prob (A,B)) = (( prob A) * (( prob B) / ( prob B))) by XCMPLX_1: 74;

      then ( prob (A,B)) = (( prob A) * 1) by A1, XCMPLX_1: 60;

      hence thesis;

    end;

    theorem :: RPR_1:55

    for E be finite non empty set, A,B be Event of E st ( prob B) = 0 holds (A,B) are_independent

    proof

      let E be finite non empty set, A,B be Event of E;

      assume

       A1: ( prob B) = 0 ;

      then ( prob (A /\ B)) <= 0 by Th19, XBOOLE_1: 17;

      then ( prob (A /\ B)) = 0 by Th18;

      hence thesis by A1;

    end;

    theorem :: RPR_1:56

    for E be finite non empty set, A,B be Event of E st (A,B) are_independent holds ((A ` ),B) are_independent

    proof

      let E be finite non empty set, A,B be Event of E;

      ( prob ((A ` ) /\ B)) = ( prob (B \ A)) by SUBSET_1: 13;

      then

       A1: ( prob ((A ` ) /\ B)) = (( prob B) - ( prob (A /\ B))) by Th23;

      assume (A,B) are_independent ;

      then ( prob ((A ` ) /\ B)) = ((1 * ( prob B)) - (( prob A) * ( prob B))) by A1;

      then ( prob ((A ` ) /\ B)) = ((1 - ( prob A)) * ( prob B));

      then ( prob ((A ` ) /\ B)) = (( prob (A ` )) * ( prob B)) by Th22;

      hence thesis;

    end;

    theorem :: RPR_1:57

    for E be finite non empty set, A,B be Event of E st A misses B & (A,B) are_independent holds ( prob A) = 0 or ( prob B) = 0 by Th16, XCMPLX_1: 6;