:: deftheorem Def3 defines -Measure_valued RANDOM_3:def 3 :
for Y being non empty set
for S being SigmaField of Y
for F being Function holds
( F is S -Measure_valued iff for x being set st x in dom F holds
ex M being sigma_Measure of S st F . x = M );