theorem Th8: :: RANDOM_1:8

for Omega being non empty finite set
for f being PartFunc of Omega,REAL ex X being Element of Trivial-SigmaField Omega st
( dom f = X & f is X -measurable )