theorem Th13: :: DIST_2:13

for S being non empty finite set
for f being b₁ -valued Function
for judgefunc being Function of S,BOOLEAN
for n being set st n in dom f holds
( n in trueEVENT (judgefunc * f) iff f . n in trueEVENT judgefunc )