:: deftheorem defines set_of_chi_RV FINANCE6:def 8 :
for Omega being non empty set
for F being SigmaField of Omega holds set_of_chi_RV F = { f where f is Function of Omega,REAL : ex A being Element of F st
( chi (A,Omega) is_random_variable_on F, Borel_Sets & chi (A,Omega) = f ) } ;