:: deftheorem Def12 defines samplingRNG DIST_2:def 12 :
for S being non empty finite set
for D being EqSampleSpaces of S
for b₃ being non empty Subset of S holds
( b₃ is samplingRNG of D iff ex x being sample of D st x in b₃ );