for x being object st x in set_of_chi_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_chi_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_chi_RV F ; :: thesis: ex f being Function of Omega,REAL st
( f = x & f is_random_variable_on F, Borel_Sets )
then consider A being Element of F such that
A1: ( x = chi (A,Omega) & chi (A,Omega) is_random_variable_on F, Borel_Sets ) ;
chi (A,Omega) is Function of Omega,REAL by ZZZ;
hence 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_chi_RV F is F -random-membered ; :: thesis: verum