theorem Th14: :: DIST_2:14

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