ConstFuncs . n in { 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 ) } ;
then ex f being Function of Omega,REAL st
( ConstFuncs . n = f & ex K being Element of REAL st
( f is_random_variable_on F, Borel_Sets & f = Omega --> K ) ) ;
hence ConstFuncs . n is random_variable of F, Borel_Sets by RANDOM_3:def 1; :: thesis: verum