:: deftheorem defines set_of_constant_RV FINANCE6:def 7 :
for Omega being non empty set
for F being SigmaField of Omega holds set_of_constant_RV F = { f where f is Function of Omega,REAL : ex K being Element of REAL st
( f is_random_variable_on F, Borel_Sets & f = Omega --> K ) } ;