:: deftheorem Def2 defines random_variable_family-like RANDOM_3:def 2 :
for F being Function holds
( F is random_variable_family-like iff for x being set st x in dom F holds
ex Omega1, Omega2 being non empty set ex S1 being SigmaField of Omega1 ex S2 being SigmaField of Omega2 ex f being random_variable of S1,S2 st F . x = f );