let S be non empty finite set ; for D being EqSampleSpaces of S
for A, B being set
for f, g being Function of S,BOOLEAN st A c= S & B c= S & A misses B & f = chi (A,S) & g = chi (B,S) holds
Prob ((f '&' g),D) = 0
let D be EqSampleSpaces of S; for A, B being set
for f, g being Function of S,BOOLEAN st A c= S & B c= S & A misses B & f = chi (A,S) & g = chi (B,S) holds
Prob ((f '&' g),D) = 0
let A, B be set ; for f, g being Function of S,BOOLEAN st A c= S & B c= S & A misses B & f = chi (A,S) & g = chi (B,S) holds
Prob ((f '&' g),D) = 0
let f, g be Function of S,BOOLEAN; ( A c= S & B c= S & A misses B & f = chi (A,S) & g = chi (B,S) implies Prob ((f '&' g),D) = 0 )
assume A1:
( A c= S & B c= S & A misses B & f = chi (A,S) & g = chi (B,S) )
; Prob ((f '&' g),D) = 0
set s = the Element of D;
A2: Prob ((f '&' g),D) =
Prob ((f '&' g), the Element of D)
by Def6
.=
(card ((trueEVENT (f * the Element of D)) /\ (trueEVENT (g * the Element of D)))) / (len the Element of D)
by Th25
;
(trueEVENT (f * the Element of D)) /\ (trueEVENT (g * the Element of D)) = {}
hence
Prob ((f '&' g),D) = 0
by A2; verum