theorem Th15: :: DIST_2:15

for S being non empty finite set
for D being EqSampleSpaces of S
for s being Element of D
for judgefunc being Function of S,BOOLEAN ex A being Subset of (dom (freqSEQ s)) st
( A = trueEVENT (judgefunc * (canFS S)) & card (trueEVENT (judgefunc * s)) = Sum (extract ((freqSEQ s),A)) )