:: deftheorem Def5 defines -Random-Variable-Family RANDOM_3:def 5 :
for Y being non empty set
for S being SigmaField of Y
for F being Function holds
( F is S -Random-Variable-Family iff for x being set st x in dom F holds
ex Z being Real-Valued-Random-Variable of S st F . x = Z );