let S be non empty finite set ; :: thesis: 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; :: thesis: 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 ; :: thesis: 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; :: thesis: ( 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) ) ; :: thesis: 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)) = {}

proof

assume (trueEVENT (f * the Element of D)) /\ (trueEVENT (g * the Element of D)) <> {} ; :: thesis: contradiction
then consider x being object such that
A3: x in (trueEVENT (f * the Element of D)) /\ (trueEVENT (g * the Element of D)) by XBOOLE_0:def 1;
A4: trueEVENT (f * the Element of D) = the Element of D " (trueEVENT f) by Th14
.= the Element of D " (f " {TRUE}) ;
A5: trueEVENT (g * the Element of D) = the Element of D " (trueEVENT g) by Th14
.= the Element of D " (g " {TRUE}) ;
( x in the Element of D " (f " {TRUE}) & x in the Element of D " (g " {TRUE}) ) by A4, A5, A3, XBOOLE_0:def 4;
then ( x in dom the Element of D & the Element of D . x in f " {TRUE} & the Element of D . x in g " {TRUE} ) by FUNCT_1:def 7;
then ( f . ( the Element of D . x) in {1} & g . ( the Element of D . x) in {1} ) by FUNCT_1:def 7;
then ( f . ( the Element of D . x) = 1 & g . ( the Element of D . x) = 1 ) by TARSKI:def 1;
then ( the Element of D . x in A & the Element of D . x in B ) by A1, FUNCT_3:36;
then the Element of D . x in A /\ B by XBOOLE_0:def 4;
hence contradiction by A1, XBOOLE_0:def 7; :: thesis: verum

end;

hence Prob ((f '&' g),D) = 0 by A2; :: thesis: verum