theorem Th8: :: DIST_2:8

for S being non empty finite set
for f being b₁ -valued Function
for judgefunc being Function of S,BOOLEAN holds trueEVENT (judgefunc * f) is Event of (dom f)