let S be non empty finite set ; :: thesis: for D being EqSampleSpaces of S
for s being Element of D
for f, g being Function of S,BOOLEAN holds Prob ((f '&' g),s) = (card ((trueEVENT (f * s)) /\ (trueEVENT (g * s)))) / (len s)
let D be EqSampleSpaces of S; :: thesis: for s being Element of D
for f, g being Function of S,BOOLEAN holds Prob ((f '&' g),s) = (card ((trueEVENT (f * s)) /\ (trueEVENT (g * s)))) / (len s)
let s be Element of D; :: thesis: for f, g being Function of S,BOOLEAN holds Prob ((f '&' g),s) = (card ((trueEVENT (f * s)) /\ (trueEVENT (g * s)))) / (len s)
let f, g be Function of S,BOOLEAN; :: thesis: Prob ((f '&' g),s) = (card ((trueEVENT (f * s)) /\ (trueEVENT (g * s)))) / (len s)
A1: s is Element of S * by FINSEQ_1:def 11;
trueEVENT ((f '&' g) * s) = Coim (((f '&' g) * s),TRUE)
.= (Coim ((f * s),TRUE)) /\ (Coim ((g * s),TRUE)) by Th22, A1
.= (trueEVENT (f * s)) /\ (trueEVENT (g * s)) ;
hence Prob ((f '&' g),s) = (card ((trueEVENT (f * s)) /\ (trueEVENT (g * s)))) / (len s) ; :: thesis: verum