for x being object st x in set_of_constant_RV F holds
ex f being Function of Omega,REAL st
( f = x & f is_random_variable_on F, Borel_Sets )

proof

let x be object ; :: thesis: ( x in set_of_constant_RV F implies ex f being Function of Omega,REAL st
( f = x & f is_random_variable_on F, Borel_Sets ) )
assume x in set_of_constant_RV F ; :: thesis: ex f being Function of Omega,REAL st
( f = x & f is_random_variable_on F, Borel_Sets )
then consider f being Function of Omega,REAL such that
A1: ( x = f & f is_random_variable_on F, Borel_Sets & f is constant ) ;
thus ex f being Function of Omega,REAL st
( f = x & f is_random_variable_on F, Borel_Sets ) by A1; :: thesis: verum

end;

hence set_of_constant_RV F is F -random-membered ; :: thesis: verum