theorem :: DIST_2:39

for S being non empty finite set
for D being EqSampleSpaces of S
for X being samplingRNG of D
for f being Function of S,BOOLEAN holds (Prob (f,X)) * (Prob X) = Prob ((f '&' (MembershipDecision X)),D)