:: deftheorem defines Prob DIST_2:def 15 :
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 (f,(ConditionalSS X));