theorem Th24: :: DIST_2:24

for S being non empty finite set
for D being EqSampleSpaces of S
for s being Element of D
for f, g being Function of S,BOOLEAN holds Prob ((f 'or' g),s) = (card ((trueEVENT (f * s)) \/ (trueEVENT (g * s)))) / (len s)