reconsider MyOmega = Omega as Element of F by PROB_1:5;
set g2 = chi (Omega,Omega);
( chi (Omega,Omega) is Function of Omega,{0,1} & rng (chi (Omega,Omega)) c= REAL ) by H0;
then Fin1: ( chi (Omega,Omega) is Function of (dom (chi (Omega,Omega))),REAL & dom (chi (Omega,Omega)) = Omega ) by FUNCT_2:2, FUNCT_2:def 1;
chi (Omega,Omega) is_random_variable_on F, Borel_Sets by ChiRandom;
then chi (MyOmega,MyOmega) in set_of_chi_RV F by Fin1;
hence not set_of_chi_RV F is empty ; :: thesis: verum