:: RPR_1 semantic presentation

begin


theorem Th1: :: RPR_1:1
for E being non empty set
for e being non empty Subset of E holds
( e is Singleton of E iff for Y being set holds
( Y c= e iff ( Y = {} or Y = e ) ) )
proof
let E be non empty set ; ::_thesis: for e being non empty Subset of E holds
( e is Singleton of E iff for Y being set holds
( Y c= e iff ( Y = {} or Y = e ) ) )
let e be non empty Subset of E; ::_thesis: ( e is Singleton of E iff for Y being set holds
( Y c= e iff ( Y = {} or Y = e ) ) )
thus  ( e is Singleton of E implies for Y being set holds
( Y c= e iff ( Y = {} or Y = e ) ) ) ::_thesis: ( ( for Y being set holds
( Y c= e iff ( Y = {} or Y = e ) ) ) implies e is Singleton of E )
proof
assume A1: e is Singleton of E ; ::_thesis: for Y being set holds
( Y c= e iff ( Y = {} or Y = e ) )
let Y be set ; ::_thesis: ( Y c= e iff ( Y = {} or Y = e ) )
 ex x being set st e = {x} by A1, ZFMISC_1:131;
hence  ( Y c= e iff ( Y = {} or Y = e ) ) by ZFMISC_1:33; ::_thesis: verum
end;
assume A2: for Y being set holds
( Y c= e iff ( Y = {} or Y = e ) ) ; ::_thesis: e is Singleton of E
consider x being set  such that
A3: x in e by XBOOLE_0:def_1;
 {x} c= e by A3, ZFMISC_1:31;
hence  e is Singleton of E by A2; ::_thesis: verum
end;

registration
let E be non empty set ;
cluster1 -element  ->  finite for Element of K11(E);
coherence
 for b1 being Singleton of E holds b1 is finite ;
end;


theorem :: RPR_1:2
for E being non empty set
for A, B being Subset of E
for e being Singleton of E st e = A \/ B & A <> B & not ( A = {} & B = e ) holds
( A = e & B = {} )
proof
let E be non empty set ; ::_thesis: for A, B being Subset of E
for e being Singleton of E st e = A \/ B & A <> B & not ( A = {} & B = e ) holds
( A = e & B = {} )
let A, B be Subset of E; ::_thesis: for e being Singleton of E st e = A \/ B & A <> B & not ( A = {} & B = e ) holds
( A = e & B = {} )
let e be Singleton of E; ::_thesis: ( e = A \/ B & A <> B & not ( A = {} & B = e ) implies ( A = e & B = {} ) )
assume that
A1: e = A \/ B and
A2: A <> B ; ::_thesis: ( ( A = {} & B = e ) or ( A = e & 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  ( ( A = {} & B = e ) or ( A = e & B = {} ) ) by A2, A3, Th1; ::_thesis: verum
end;

theorem :: RPR_1:3
for E being non empty set
for A, B being Subset of E
for e being Singleton of E holds
( not e = A \/ B or ( A = e & B = e ) or ( A = e & B = {} ) or ( A = {} & B = e ) )
proof
let E be non empty set ; ::_thesis: for A, B being Subset of E
for e being Singleton of E holds
( not e = A \/ B or ( A = e & B = e ) or ( A = e & B = {} ) or ( A = {} & B = e ) )
let A, B be Subset of E; ::_thesis: for e being Singleton of E holds
( not e = A \/ B or ( A = e & B = e ) or ( A = e & B = {} ) or ( A = {} & B = e ) )
let e be Singleton of E; ::_thesis: ( not e = A \/ B or ( A = e & B = e ) or ( A = e & B = {} ) or ( A = {} & B = e ) )
assume A1: e = A \/ B ; ::_thesis: ( ( A = e & B = e ) or ( A = e & B = {} ) or ( A = {} & B = e ) )
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  ( ( A = e & B = e ) or ( A = e & B = {} ) or ( A = {} & B = e ) ) by A1; ::_thesis: verum
end;

theorem :: RPR_1:4
for E being non empty set
for a being Element of E holds {a} is Singleton of E ;

theorem :: RPR_1:5
for E being non empty set
for e1, e2 being Singleton of E st e1 c= e2 holds
e1 = e2 by Th1;

theorem Th6: :: RPR_1:6
for E being non empty set
for e being Singleton of E ex a being Element of E st
( a in E & e = {a} )
proof
let E be non empty set ; ::_thesis: for e being Singleton of E ex a being Element of E st
( a in E & e = {a} )
let e be Singleton of E; ::_thesis: ex a being Element of E st
( a in E & e = {a} )
set x = the Element of e;
 { the Element of e} = e by Th1;
hence  ex a being Element of E st
( a in E & e = {a} ) ; ::_thesis: verum
end;

theorem :: RPR_1:7
for E being non empty set ex e being Singleton of E st e is Singleton of E
proof
let E be non empty set ; ::_thesis: ex e being Singleton of E st e is Singleton of E
take  { the Element of E} ; ::_thesis: { the Element of E} is Singleton of E
thus  { the Element of E} is Singleton of E ; ::_thesis: verum
end;

theorem :: RPR_1:8
for E being non empty set
for e being Singleton of E ex p being FinSequence st
( p is FinSequence of E & rng p = e & len p = 1 )
proof
let E be non empty set ; ::_thesis: for e being Singleton of E ex p being FinSequence st
( p is FinSequence of E & rng p = e & len p = 1 )
let e be Singleton of E; ::_thesis: ex p being FinSequence st
( p is FinSequence of E & rng p = e & len p = 1 )
consider a being Element of E such that
 a in E and
A1: e = {a} by Th6;
 ( rng <*a*> = {a} & len <*a*> = 1 ) by FINSEQ_1:39;
hence  ex p being FinSequence st
( p is FinSequence of E & rng p = e & len p = 1 ) by A1; ::_thesis: verum
end;

definition
let E be set ;
mode Event of E is Subset of E;
end;

theorem :: RPR_1:9
for E being non empty set
for e being Singleton of E
for A being Event of E holds
( e misses A or e /\ A = e )
proof
let E be non empty set ; ::_thesis: for e being Singleton of E
for A being Event of E holds
( e misses A or e /\ A = e )
let e be Singleton of E; ::_thesis: for A being Event of E holds
( e misses A or e /\ A = e )
let A be Event of E; ::_thesis: ( e misses A or e /\ A = 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  ( e misses A or e /\ A = e ) by XBOOLE_0:def_7; ::_thesis: verum
end;

theorem :: RPR_1:10
for E being non empty set
for A being Event of E st A <> {} holds
ex e being Singleton of E st e c= A
proof
let E be non empty set ; ::_thesis: for A being Event of E st A <> {} holds
ex e being Singleton of E st e c= A
let A be Event of E; ::_thesis: ( A <> {} implies ex e being Singleton of E st e c= A )
set x = the Element of A;
assume A1: A <> {} ; ::_thesis: ex e being Singleton of E st e c= A
then reconsider x = the Element of A as Element of E by TARSKI:def_3;
 {x} c= A by A1, ZFMISC_1:31;
hence  ex e being Singleton of E st e c= A ; ::_thesis: verum
end;

theorem :: RPR_1:11
for E being non empty set
for e being Singleton of E
for A being Event of E holds
( not e c= A \/ (A `) or e c= A or e c= A ` )
proof
let E be non empty set ; ::_thesis: for e being Singleton of E
for A being Event of E holds
( not e c= A \/ (A `) or e c= A or e c= A ` )
let e be Singleton of E; ::_thesis: for A being Event of E holds
( not e c= A \/ (A `) or e c= A or e c= A ` )
let A be Event of E; ::_thesis: ( not e c= A \/ (A `) or e c= A or e c= A ` )
 ex a being Element of E st
( a in E & e = {a} ) by Th6;
then consider a being Element of E such that
A1: e = {a} ;
assume  e c= A \/ (A `) ; ::_thesis: ( e c= A or e c= 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  ( e c= A or e c= A ` ) by A1, ZFMISC_1:31; ::_thesis: verum
end;

theorem :: RPR_1:12
for E being non empty set
for e1, e2 being Singleton of E holds
( e1 = e2 or e1 misses e2 )
proof
let E be non empty set ; ::_thesis: for e1, e2 being Singleton of E holds
( e1 = e2 or e1 misses e2 )
let e1, e2 be Singleton of E; ::_thesis: ( e1 = e2 or e1 misses e2 )
 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  ( e1 = e2 or e1 misses e2 ) by Th1, XBOOLE_0:def_7; ::_thesis: verum
end;

theorem Th13: :: RPR_1:13
for E being non empty set
for A, B being Subset of E holds A /\ B misses A /\ (B `)
proof
let E be non empty set ; ::_thesis: for A, B being Subset of E holds A /\ B misses A /\ (B `)
let A, B be Subset of E; ::_thesis: A /\ B misses A /\ (B `)
 A /\ B misses A \ B by XBOOLE_1:89;
hence  A /\ B misses A /\ (B `) by SUBSET_1:13; ::_thesis: verum
end;

Lm1:  for E being non empty finite set holds 0 < card E
proof
let E be non empty finite set ; ::_thesis: 0 < card E
 card { the Element of E} <= card E by NAT_1:43;
hence  0 < card E by CARD_1:30; ::_thesis: verum
end;

definition
let E be finite set ;
let A be Event of E;
func prob A ->  Real equals :: RPR_1:def 1
(card A) / (card E);
coherence
 (card A) / (card E) is Real by XREAL_0:def_1;
end;

:: deftheorem  defines prob RPR_1:def_1_:_
 for E being finite set
for A being Event of E holds prob A = (card A) / (card E);

theorem :: RPR_1:14
for E being non empty finite set
for e being Singleton of E holds prob e = 1 / (card E) by CARD_1:def_7;

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

theorem Th16: :: RPR_1:16
for E being non empty finite set
for A, B being Event of E st A misses B holds
prob (A /\ B) = 0
proof
let E be non empty finite set ; ::_thesis: for A, B being Event of E st A misses B holds
prob (A /\ B) = 0
let A, B be Event of E; ::_thesis: ( A misses B implies prob (A /\ B) = 0 )
assume  A misses B ; ::_thesis: prob (A /\ B) = 0
then  A /\ B = {} E by XBOOLE_0:def_7;
hence  prob (A /\ B) = 0 by CARD_1:27; ::_thesis: verum
end;

theorem :: RPR_1:17
for E being non empty finite set
for A being Event of E holds prob A <= 1
proof
let E be non empty finite set ; ::_thesis: for A being Event of E holds prob A <= 1
let A be Event of E; ::_thesis: prob A <= 1
 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  prob A <= 1 by XCMPLX_1:60; ::_thesis: verum
end;

theorem Th18: :: RPR_1:18
for E being non empty finite set
for A being Event of E holds 0 <= prob A
proof
let E be non empty finite set ; ::_thesis: for A being Event of E holds 0 <= prob A
let A be Event of E; ::_thesis: 0 <= prob A
 ( 0 < card E & 0 <= card A ) by Lm1, CARD_1:27;
hence  0 <= prob A ; ::_thesis: verum
end;

theorem Th19: :: RPR_1:19
for E being non empty finite set
for A, B being Event of E st A c= B holds
prob A <= prob B
proof
let E be non empty finite set ; ::_thesis: for A, B being Event of E st A c= B holds
prob A <= prob B
let A, B be Event of E; ::_thesis: ( A c= B implies prob A <= prob B )
assume A1: A c= B ; ::_thesis: prob A <= prob 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  prob A <= prob B by XCMPLX_0:def_9; ::_thesis: verum
end;

theorem Th20: :: RPR_1:20
for E being non empty finite set
for A, B being Event of E holds prob (A \/ B) = ((prob A) + (prob B)) - (prob (A /\ B))
proof
let E be non empty finite set ; ::_thesis: for A, B being Event of E holds prob (A \/ B) = ((prob A) + (prob B)) - (prob (A /\ B))
let A, B be Event of E; ::_thesis: prob (A \/ B) = ((prob A) + (prob B)) - (prob (A /\ B))
set q = (card E) " ;
set p = card E;
 card (A \/ B) = ((card A) + (card B)) - (card (A /\ B)) by CARD_2:45;
then  (card (A \/ B)) * ((card E) ") = ((card A) * ((card E) ")) + (((card B) * ((card E) ")) - ((card (A /\ B)) * ((card E) "))) ;
then  (card (A \/ B)) / (card E) = (((card A) * ((card E) ")) + ((card B) * ((card E) "))) - ((card (A /\ B)) * ((card E) ")) by XCMPLX_0:def_9;
then  (card (A \/ B)) / (card E) = (((card A) / (card E)) + ((card B) * ((card E) "))) - ((card (A /\ B)) * ((card E) ")) by XCMPLX_0:def_9;
then  (card (A \/ B)) / (card E) = (((card A) / (card E)) + ((card B) / (card E))) - ((card (A /\ B)) * ((card E) ")) by XCMPLX_0:def_9;
hence  prob (A \/ B) = ((prob A) + (prob B)) - (prob (A /\ B)) by XCMPLX_0:def_9; ::_thesis: verum
end;

theorem Th21: :: RPR_1:21
for E being non empty finite set
for A, B being Event of E st A misses B holds
prob (A \/ B) = (prob A) + (prob B)
proof
let E be non empty finite set ; ::_thesis: for A, B being Event of E st A misses B holds
prob (A \/ B) = (prob A) + (prob B)
let A, B be Event of E; ::_thesis: ( A misses B implies prob (A \/ B) = (prob A) + (prob B) )
assume  A misses B ; ::_thesis: prob (A \/ B) = (prob A) + (prob B)
then  prob (A /\ B) = 0 by Th16;
then  prob (A \/ B) = ((prob A) + (prob B)) - 0 by Th20;
hence  prob (A \/ B) = (prob A) + (prob B) ; ::_thesis: verum
end;

theorem Th22: :: RPR_1:22
for E being non empty finite set
for A being Event of E holds
( prob A = 1 - (prob (A `)) & prob (A `) = 1 - (prob A) )
proof
let E be non empty finite set ; ::_thesis: for A being Event of E holds
( prob A = 1 - (prob (A `)) & prob (A `) = 1 - (prob A) )
let A be Event of E; ::_thesis: ( prob A = 1 - (prob (A `)) & prob (A `) = 1 - (prob A) )
 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  ( prob A = 1 - (prob (A `)) & prob (A `) = 1 - (prob A) ) ; ::_thesis: verum
end;

theorem Th23: :: RPR_1:23
for E being non empty finite set
for A, B being Event of E holds prob (A \ B) = (prob A) - (prob (A /\ B))
proof
let E be non empty finite set ; ::_thesis: for A, B being Event of E holds prob (A \ B) = (prob A) - (prob (A /\ B))
let A, B be Event of E; ::_thesis: prob (A \ B) = (prob A) - (prob (A /\ B))
 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  prob (A \ B) = (prob A) - (prob (A /\ B)) ; ::_thesis: verum
end;

theorem Th24: :: RPR_1:24
for E being non empty finite set
for A, B being Event of E st B c= A holds
prob (A \ B) = (prob A) - (prob B)
proof
let E be non empty finite set ; ::_thesis: for A, B being Event of E st B c= A holds
prob (A \ B) = (prob A) - (prob B)
let A, B be Event of E; ::_thesis: ( B c= A implies prob (A \ B) = (prob A) - (prob B) )
assume  B c= A ; ::_thesis: prob (A \ B) = (prob A) - (prob B)
then  prob (A /\ B) = prob B by XBOOLE_1:28;
hence  prob (A \ B) = (prob A) - (prob B) by Th23; ::_thesis: verum
end;

theorem :: RPR_1:25
for E being non empty finite set
for A, B being Event of E holds prob (A \/ B) <= (prob A) + (prob B)
proof
let E be non empty finite set ; ::_thesis: for A, B being Event of E holds prob (A \/ B) <= (prob A) + (prob B)
let A, B be Event of E; ::_thesis: prob (A \/ B) <= (prob A) + (prob B)
 prob (A \/ B) = ((prob A) + (prob B)) - (prob (A /\ B)) by Th20;
hence  prob (A \/ B) <= (prob A) + (prob B) by Th18, XREAL_1:43; ::_thesis: verum
end;

theorem Th26: :: RPR_1:26
for E being non empty finite set
for A, B being Event of E holds prob A = (prob (A /\ B)) + (prob (A /\ (B `)))
proof
let E be non empty finite set ; ::_thesis: for A, B being Event of E holds prob A = (prob (A /\ B)) + (prob (A /\ (B `)))
let A, B be Event of E; ::_thesis: prob A = (prob (A /\ B)) + (prob (A /\ (B `)))
 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  prob A = (prob (A /\ B)) + (prob (A /\ (B `))) by A1, XBOOLE_1:23; ::_thesis: verum
end;

theorem :: RPR_1:27
for E being non empty finite set
for A, B being Event of E holds prob A = (prob (A \/ B)) - (prob (B \ A))
proof
let E be non empty finite set ; ::_thesis: for A, B being Event of E holds prob A = (prob (A \/ B)) - (prob (B \ A))
let A, B be Event of E; ::_thesis: prob A = (prob (A \/ B)) - (prob (B \ A))
 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  prob A = (prob (A \/ B)) - (prob (B \ A)) ; ::_thesis: verum
end;

theorem :: RPR_1:28
for E being non empty finite set
for A, B being Event of E holds (prob A) + (prob ((A `) /\ B)) = (prob B) + (prob ((B `) /\ A))
proof
let E be non empty finite set ; ::_thesis: for A, B being Event of E holds (prob A) + (prob ((A `) /\ B)) = (prob B) + (prob ((B `) /\ A))
let A, B be Event of E; ::_thesis: (prob A) + (prob ((A `) /\ B)) = (prob B) + (prob ((B `) /\ A))
 ( prob A = (prob (A /\ B)) + (prob (A /\ (B `))) & prob B = (prob (A /\ B)) + (prob (B /\ (A `))) ) by Th26;
hence  (prob A) + (prob ((A `) /\ B)) = (prob B) + (prob ((B `) /\ A)) ; ::_thesis: verum
end;

theorem Th29: :: RPR_1:29
for E being non empty finite set
for A, B, C being 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 non empty finite set ; ::_thesis: for A, B, C being 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))
let A, B, C be Event of E; ::_thesis: prob ((A \/ B) \/ C) = ((((prob A) + (prob B)) + (prob C)) - (((prob (A /\ B)) + (prob (A /\ C))) + (prob (B /\ C)))) + (prob ((A /\ B) /\ C))
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  prob ((A \/ B) \/ C) = ((((prob A) + (prob B)) + (prob C)) - (((prob (A /\ B)) + (prob (A /\ C))) + (prob (B /\ C)))) + (prob ((A /\ B) /\ C)) ; ::_thesis: verum
end;

theorem :: RPR_1:30
for E being non empty finite set
for A, B, C being 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 non empty finite set ; ::_thesis: for A, B, C being Event of E st A misses B & A misses C & B misses C holds
prob ((A \/ B) \/ C) = ((prob A) + (prob B)) + (prob C)
let A, B, C be Event of E; ::_thesis: ( A misses B & A misses C & B misses C implies prob ((A \/ B) \/ C) = ((prob A) + (prob B)) + (prob C) )
assume that
A1: A misses B and
A2: A misses C and
A3: B misses C ; ::_thesis: prob ((A \/ B) \/ C) = ((prob A) + (prob B)) + (prob 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  prob ((A \/ B) \/ C) = ((prob A) + (prob B)) + (prob C) ; ::_thesis: verum
end;

theorem :: RPR_1:31
for E being non empty finite set
for A, B being Event of E holds (prob A) - (prob B) <= prob (A \ B)
proof
let E be non empty finite set ; ::_thesis: for A, B being Event of E holds (prob A) - (prob B) <= prob (A \ B)
let A, B be Event of E; ::_thesis: (prob A) - (prob B) <= prob (A \ B)
 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  (prob A) - (prob B) <= prob (A \ B) by Th23; ::_thesis: verum
end;

definition
let E be finite set ;
let B, A be Event of E;
func prob (A,B) ->  Real equals :: RPR_1:def 2
(prob (A /\ B)) / (prob B);
coherence
 (prob (A /\ B)) / (prob B) is Real ;
end;

:: deftheorem  defines prob RPR_1:def_2_:_
 for E being finite set
for B, A being Event of E holds prob (A,B) = (prob (A /\ B)) / (prob B);

theorem :: RPR_1:32
for E being non empty finite set
for A being Event of E holds prob (A,([#] E)) = prob A
proof
let E be non empty finite set ; ::_thesis: for A being Event of E holds prob (A,([#] E)) = prob A
let A be Event of E; ::_thesis: prob (A,([#] E)) = prob A
 prob ([#] E) = 1 by XCMPLX_1:60;
hence  prob (A,([#] E)) = prob A by XBOOLE_1:28; ::_thesis: verum
end;

theorem :: RPR_1:33
for E being non empty finite set holds prob (([#] E),([#] E)) = 1
proof
let E be non empty finite set ; ::_thesis: prob (([#] E),([#] E)) = 1
 prob ([#] E) = 1 by XCMPLX_1:60;
hence  prob (([#] E),([#] E)) = 1 ; ::_thesis: verum
end;

theorem :: RPR_1:34
for E being non empty finite set
for A, B being Event of E st 0 < prob B holds
prob (A,B) <= 1
proof
let E be non empty finite set ; ::_thesis: for A, B being Event of E st 0 < prob B holds
prob (A,B) <= 1
let A, B be Event of E; ::_thesis: ( 0 < prob B implies prob (A,B) <= 1 )
assume A1: 0 < prob B ; ::_thesis: prob (A,B) <= 1
 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  prob (A,B) <= 1 by XCMPLX_0:def_9; ::_thesis: verum
end;

theorem :: RPR_1:35
for E being non empty finite set
for A, B being Event of E st 0 < prob B holds
0 <= prob (A,B)
proof
let E be non empty finite set ; ::_thesis: for A, B being Event of E st 0 < prob B holds
0 <= prob (A,B)
let A, B be Event of E; ::_thesis: ( 0 < prob B implies 0 <= prob (A,B) )
assume A1: 0 < prob B ; ::_thesis: 0 <= prob (A,B)
 0 <= prob (A /\ B) by Th18;
hence  0 <= prob (A,B) by A1; ::_thesis: verum
end;

theorem Th36: :: RPR_1:36
for E being non empty finite set
for A, B being Event of E st 0 < prob B holds
prob (A,B) = 1 - ((prob (B \ A)) / (prob B))
proof
let E be non empty finite set ; ::_thesis: for A, B being Event of E st 0 < prob B holds
prob (A,B) = 1 - ((prob (B \ A)) / (prob B))
let A, B be Event of E; ::_thesis: ( 0 < prob B implies prob (A,B) = 1 - ((prob (B \ A)) / (prob B)) )
 (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 ; ::_thesis: prob (A,B) = 1 - ((prob (B \ A)) / (prob B))
hence  prob (A,B) = 1 - ((prob (B \ A)) / (prob B)) by A1, XCMPLX_1:60; ::_thesis: verum
end;

theorem :: RPR_1:37
for E being non empty finite set
for A, B being Event of E st 0 < prob B & A c= B holds
prob (A,B) = (prob A) / (prob B)
proof
let E be non empty finite set ; ::_thesis: for A, B being Event of E st 0 < prob B & A c= B holds
prob (A,B) = (prob A) / (prob B)
let A, B be Event of E; ::_thesis: ( 0 < prob B & A c= B implies prob (A,B) = (prob A) / (prob B) )
assume that
A1: 0 < prob B and
A2: A c= B ; ::_thesis: prob (A,B) = (prob A) / (prob 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  prob (A,B) = (prob A) / (prob B) ; ::_thesis: verum
end;

theorem Th38: :: RPR_1:38
for E being non empty finite set
for A, B being Event of E st A misses B holds
prob (A,B) = 0
proof
let E be non empty finite set ; ::_thesis: for A, B being Event of E st A misses B holds
prob (A,B) = 0
let A, B be Event of E; ::_thesis: ( A misses B implies prob (A,B) = 0 )
assume  A misses B ; ::_thesis: prob (A,B) = 0
then  prob (A,B) = 0 / (prob B) by Th16
.= 0 * ((prob B) ") ;
hence  prob (A,B) = 0 ; ::_thesis: verum
end;

theorem Th39: :: RPR_1:39
for E being non empty finite set
for A, B being 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 non empty finite set ; ::_thesis: for A, B being Event of E st 0 < prob A & 0 < prob B holds
(prob A) * (prob (B,A)) = (prob B) * (prob (A,B))
let A, B be Event of E; ::_thesis: ( 0 < prob A & 0 < prob B implies (prob A) * (prob (B,A)) = (prob B) * (prob (A,B)) )
assume that
A1: 0 < prob A and
A2: 0 < prob B ; ::_thesis: (prob A) * (prob (B,A)) = (prob B) * (prob (A,B))
 (prob A) * (prob (B,A)) = prob (A /\ B) by A1, XCMPLX_1:87;
hence  (prob A) * (prob (B,A)) = (prob B) * (prob (A,B)) by A2, XCMPLX_1:87; ::_thesis: verum
end;

theorem Th40: :: RPR_1:40
for E being non empty finite set
for A, B being 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 non empty finite set ; ::_thesis: for A, B being Event of E st 0 < prob B holds
( prob (A,B) = 1 - (prob ((A `),B)) & prob ((A `),B) = 1 - (prob (A,B)) )
let A, B be Event of E; ::_thesis: ( 0 < prob B implies ( prob (A,B) = 1 - (prob ((A `),B)) & prob ((A `),B) = 1 - (prob (A,B)) ) )
assume A1: 0 < prob B ; ::_thesis: ( prob (A,B) = 1 - (prob ((A `),B)) & prob ((A `),B) = 1 - (prob (A,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  ( prob (A,B) = 1 - (prob ((A `),B)) & prob ((A `),B) = 1 - (prob (A,B)) ) ; ::_thesis: verum
end;

theorem Th41: :: RPR_1:41
for E being non empty finite set
for A, B being Event of E st 0 < prob B & B c= A holds
prob (A,B) = 1
proof
let E be non empty finite set ; ::_thesis: for A, B being Event of E st 0 < prob B & B c= A holds
prob (A,B) = 1
let A, B be Event of E; ::_thesis: ( 0 < prob B & B c= A implies prob (A,B) = 1 )
assume that
A1: 0 < prob B and
A2: B c= A ; ::_thesis: prob (A,B) = 1
 prob (A /\ B) = prob B by A2, XBOOLE_1:28;
hence  prob (A,B) = 1 by A1, XCMPLX_1:60; ::_thesis: verum
end;

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

theorem :: RPR_1:43
for E being non empty finite set
for A being Event of E holds prob ((A `),A) = 0
proof
let E be non empty finite set ; ::_thesis: for A being Event of E holds prob ((A `),A) = 0
let A be Event of E; ::_thesis: prob ((A `),A) = 0
 A ` misses A by SUBSET_1:24;
then  prob ((A `) /\ A) = 0 by Th16;
hence  prob ((A `),A) = 0 ; ::_thesis: verum
end;

theorem :: RPR_1:44
for E being non empty finite set
for A being Event of E holds prob (A,(A `)) = 0
proof
let E be non empty finite set ; ::_thesis: for A being Event of E holds prob (A,(A `)) = 0
let A be Event of E; ::_thesis: prob (A,(A `)) = 0
 A misses A ` by SUBSET_1:24;
then  prob (A /\ (A `)) = 0 by Th16;
hence  prob (A,(A `)) = 0 ; ::_thesis: verum
end;

theorem Th45: :: RPR_1:45
for E being non empty finite set
for A, B being Event of E st 0 < prob B & A misses B holds
prob ((A `),B) = 1
proof
let E be non empty finite set ; ::_thesis: for A, B being Event of E st 0 < prob B & A misses B holds
prob ((A `),B) = 1
let A, B be Event of E; ::_thesis: ( 0 < prob B & A misses B implies prob ((A `),B) = 1 )
assume that
A1: 0 < prob B and
A2: A misses B ; ::_thesis: prob ((A `),B) = 1
 prob (A,B) = 0 by A2, Th38;
then  1 - (prob ((A `),B)) = 0 by A1, Th40;
hence  prob ((A `),B) = 1 ; ::_thesis: verum
end;

theorem Th46: :: RPR_1:46
for E being non empty finite set
for A, B being 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 non empty finite set ; ::_thesis: for A, B being Event of E st 0 < prob A & prob B < 1 & A misses B holds
prob (A,(B `)) = (prob A) / (1 - (prob B))
let A, B be Event of E; ::_thesis: ( 0 < prob A & prob B < 1 & A misses B implies prob (A,(B `)) = (prob A) / (1 - (prob B)) )
assume that
A1: 0 < prob A and
A2: prob B < 1 and
A3: A misses B ; ::_thesis: prob (A,(B `)) = (prob A) / (1 - (prob 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  prob (A,(B `)) = (prob A) / (1 - (prob B)) by A5, XCMPLX_0:def_9; ::_thesis: verum
end;

theorem :: RPR_1:47
for E being non empty finite set
for A, B being 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 non empty finite set ; ::_thesis: for A, B being Event of E st 0 < prob A & prob B < 1 & A misses B holds
prob ((A `),(B `)) = 1 - ((prob A) / (1 - (prob B)))
let A, B be Event of E; ::_thesis: ( 0 < prob A & prob B < 1 & A misses B implies prob ((A `),(B `)) = 1 - ((prob A) / (1 - (prob B))) )
assume that
A1: 0 < prob A and
A2: prob B < 1 and
A3: A misses B ; ::_thesis: prob ((A `),(B `)) = 1 - ((prob A) / (1 - (prob 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  prob ((A `),(B `)) = 1 - ((prob A) / (1 - (prob B))) by A1, A2, A3, Th46; ::_thesis: verum
end;

theorem :: RPR_1:48
for E being non empty finite set
for A, B, C being 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 non empty finite set ; ::_thesis: for A, B, C being 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)
let A, B, C be Event of E; ::_thesis: ( 0 < prob (B /\ C) & 0 < prob C implies prob ((A /\ B) /\ C) = ((prob (A,(B /\ C))) * (prob (B,C))) * (prob C) )
assume that
A1: 0 < prob (B /\ C) and
A2: 0 < prob C ; ::_thesis: prob ((A /\ B) /\ C) = ((prob (A,(B /\ C))) * (prob (B,C))) * (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  prob ((A /\ B) /\ C) = ((prob (A,(B /\ C))) * (prob (B,C))) * (prob C) by A3; ::_thesis: verum
end;

theorem Th49: :: RPR_1:49
for E being non empty finite set
for A, B being 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 non empty finite set ; ::_thesis: for A, B being Event of E st 0 < prob B & prob B < 1 holds
prob A = ((prob (A,B)) * (prob B)) + ((prob (A,(B `))) * (prob (B `)))
let A, B be Event of E; ::_thesis: ( 0 < prob B & prob B < 1 implies prob A = ((prob (A,B)) * (prob B)) + ((prob (A,(B `))) * (prob (B `))) )
assume that
A1: 0 < prob B and
A2: prob B < 1 ; ::_thesis: prob A = ((prob (A,B)) * (prob B)) + ((prob (A,(B `))) * (prob (B `)))
 (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  prob A = ((prob (A,B)) * (prob B)) + ((prob (A,(B `))) * (prob (B `))) by A3, XCMPLX_1:87; ::_thesis: verum
end;

theorem Th50: :: RPR_1:50
for E being non empty finite set
for A, B1, B2 being 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 non empty finite set ; ::_thesis: for A, B1, B2 being 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))
let A, B1, B2 be Event of E; ::_thesis: ( 0 < prob B1 & 0 < prob B2 & B1 \/ B2 = E & B1 misses B2 implies prob A = ((prob (A,B1)) * (prob B1)) + ((prob (A,B2)) * (prob B2)) )
assume that
A1: 0 < prob B1 and
A2: 0 < prob B2 and
A3: B1 \/ B2 = E and
A4: B1 misses B2 ; ::_thesis: prob A = ((prob (A,B1)) * (prob B1)) + ((prob (A,B2)) * (prob 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  prob A = ((prob (A,B1)) * (prob B1)) + ((prob (A,B2)) * (prob B2)) by A1, A6, Th49; ::_thesis: verum
end;

theorem Th51: :: RPR_1:51
for E being non empty finite set
for A, B1, B2, B3 being 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 non empty finite set ; ::_thesis: for A, B1, B2, B3 being 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))
let A, B1, B2, B3 be Event of E; ::_thesis: ( 0 < prob B1 & 0 < prob B2 & 0 < prob B3 & (B1 \/ B2) \/ B3 = E & B1 misses B2 & B1 misses B3 & B2 misses B3 implies prob A = (((prob (A,B1)) * (prob B1)) + ((prob (A,B2)) * (prob B2))) + ((prob (A,B3)) * (prob B3)) )
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 = {} ; :: according to XBOOLE_0:def_7 ::_thesis: prob A = (((prob (A,B1)) * (prob B1)) + ((prob (A,B2)) * (prob B2))) + ((prob (A,B3)) * (prob B3))
 (B1 /\ B3) \/ (B2 /\ B3) = B2 /\ B3 by A6;
then  (B1 \/ B2) /\ B3 = {} by A7, XBOOLE_1:23;
then A8: B1 \/ B2 misses B3 by XBOOLE_0:def_7;
 ((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, XBOOLE_0:def_7;
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  prob A = (((prob (A,B1)) * (prob B1)) + ((prob (A,B2)) * (prob B2))) + ((prob (A,B3)) * (prob B3)) by A3, XCMPLX_1:87; ::_thesis: verum
end;

theorem :: RPR_1:52
for E being non empty finite set
for A, B1, B2 being 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 non empty finite set ; ::_thesis: for A, B1, B2 being 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)))
let A, B1, B2 be Event of E; ::_thesis: ( 0 < prob B1 & 0 < prob B2 & B1 \/ B2 = E & B1 misses B2 implies prob (B1,A) = ((prob (A,B1)) * (prob B1)) / (((prob (A,B1)) * (prob B1)) + ((prob (A,B2)) * (prob B2))) )
assume that
A1: 0 < prob B1 and
A2: ( 0 < prob B2 & B1 \/ B2 = E & B1 misses B2 ) ; ::_thesis: prob (B1,A) = ((prob (A,B1)) * (prob B1)) / (((prob (A,B1)) * (prob B1)) + ((prob (A,B2)) * (prob B2)))
 prob A = ((prob (A,B1)) * (prob B1)) + ((prob (A,B2)) * (prob B2)) by A1, A2, Th50;
hence  prob (B1,A) = ((prob (A,B1)) * (prob B1)) / (((prob (A,B1)) * (prob B1)) + ((prob (A,B2)) * (prob B2))) by A1, XCMPLX_1:87; ::_thesis: verum
end;

theorem :: RPR_1:53
for E being non empty finite set
for A, B1, B2, B3 being 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 non empty finite set ; ::_thesis: for A, B1, B2, B3 being 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)))
let A, B1, B2, B3 be Event of E; ::_thesis: ( 0 < prob B1 & 0 < prob B2 & 0 < prob B3 & (B1 \/ B2) \/ B3 = E & B1 misses B2 & B1 misses B3 & B2 misses B3 implies prob (B1,A) = ((prob (A,B1)) * (prob B1)) / ((((prob (A,B1)) * (prob B1)) + ((prob (A,B2)) * (prob B2))) + ((prob (A,B3)) * (prob B3))) )
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 ) ; ::_thesis: prob (B1,A) = ((prob (A,B1)) * (prob B1)) / ((((prob (A,B1)) * (prob B1)) + ((prob (A,B2)) * (prob B2))) + ((prob (A,B3)) * (prob B3)))
 prob A = (((prob (A,B1)) * (prob B1)) + ((prob (A,B2)) * (prob B2))) + ((prob (A,B3)) * (prob B3)) by A1, A2, Th51;
hence  prob (B1,A) = ((prob (A,B1)) * (prob B1)) / ((((prob (A,B1)) * (prob B1)) + ((prob (A,B2)) * (prob B2))) + ((prob (A,B3)) * (prob B3))) by A1, XCMPLX_1:87; ::_thesis: verum
end;

definition
let E be finite set ;
let A, B be Event of E;
predA,B are_independent  means :Def3: :: RPR_1:def 3
 prob (A /\ B) = (prob A) * (prob B);
symmetry
 for A, B being Event of E st prob (A /\ B) = (prob A) * (prob B) holds
prob (B /\ A) = (prob B) * (prob A) ;
end;

:: deftheorem Def3 defines are_independent RPR_1:def_3_:_
 for E being finite set
for A, B being Event of E holds
( A,B are_independent iff prob (A /\ B) = (prob A) * (prob B) );

theorem :: RPR_1:54
for E being non empty finite set
for A, B being Event of E st 0 < prob B & A,B are_independent holds
prob (A,B) = prob A
proof
let E be non empty finite set ; ::_thesis: for A, B being Event of E st 0 < prob B & A,B are_independent holds
prob (A,B) = prob A
let A, B be Event of E; ::_thesis: ( 0 < prob B & A,B are_independent implies prob (A,B) = prob A )
assume that
A1: 0 < prob B and
A2: A,B are_independent ; ::_thesis: prob (A,B) = prob A
 prob (A /\ B) = (prob A) * (prob B) by A2, Def3;
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  prob (A,B) = prob A ; ::_thesis: verum
end;

theorem :: RPR_1:55
for E being non empty finite set
for A, B being Event of E st prob B = 0 holds
A,B are_independent
proof
let E be non empty finite set ; ::_thesis: for A, B being Event of E st prob B = 0 holds
A,B are_independent
let A, B be Event of E; ::_thesis: ( prob B = 0 implies A,B are_independent )
A1: 0 = (prob A) * 0 ;
assume A2: prob B = 0 ; ::_thesis: A,B are_independent
then  prob (A /\ B) <= 0 by Th19, XBOOLE_1:17;
then  prob (A /\ B) = 0 by Th18;
hence  A,B are_independent by A2, A1, Def3; ::_thesis: verum
end;

theorem :: RPR_1:56
for E being non empty finite set
for A, B being Event of E st A,B are_independent holds
A ` ,B are_independent
proof
let E be non empty finite set ; ::_thesis: for A, B being Event of E st A,B are_independent holds
A ` ,B are_independent
let A, B be Event of E; ::_thesis: ( A,B are_independent implies A ` ,B are_independent )
 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 ; ::_thesis: A ` ,B are_independent
then  prob ((A `) /\ B) = (1 * (prob B)) - ((prob A) * (prob B)) by A1, Def3;
then  prob ((A `) /\ B) = (1 - (prob A)) * (prob B) ;
then  prob ((A `) /\ B) = (prob (A `)) * (prob B) by Th22;
hence  A ` ,B are_independent by Def3; ::_thesis: verum
end;

theorem :: RPR_1:57
for E being non empty finite set
for A, B being Event of E st A misses B & A,B are_independent & not prob A = 0 holds
prob B = 0
proof
let E be non empty finite set ; ::_thesis: for A, B being Event of E st A misses B & A,B are_independent & not prob A = 0 holds
prob B = 0
let A, B be Event of E; ::_thesis: ( A misses B & A,B are_independent & not prob A = 0 implies prob B = 0 )
assume that
A1: A misses B and
A2: A,B are_independent ; ::_thesis: ( prob A = 0 or prob B = 0 )
 prob (A /\ B) = 0 by A1, Th16;
then  (prob A) * (prob B) = 0 by A2, Def3;
hence  ( prob A = 0 or prob B = 0 ) by XCMPLX_1:6; ::_thesis: verum
end;