:: deftheorem defines set_of_random_variables_on FINANCE1:def 6 :
for Omega, Omega2 being set
for F being SigmaField of Omega
for F2 being SigmaField of Omega2 holds set_of_random_variables_on (F,F2) = { f where f is Function of Omega,Omega2 : f is_random_variable_on F,F2 } ;