theorem :: DIST_2:20

for S being non empty finite set
for s being Element of S *
for f being Function of S,BOOLEAN
for F being SigmaField of (dom s) st F = bool (dom s) holds
Coim ((f * s),TRUE) is Event of F by Th18;