let Omega be non empty set ; :: thesis: for F being SigmaField of Omega holds chi (Omega,Omega) is b₁, Borel_Sets -random_variable-like Function of Omega,REAL
let F be SigmaField of Omega; :: thesis: chi (Omega,Omega) is F, Borel_Sets -random_variable-like Function of Omega,REAL
set g2 = chi (Omega,Omega);
reconsider O = Omega as Element of F by PROB_1:5;
chi (O,Omega) is random_variable of F, Borel_Sets by ZZZ;
hence chi (Omega,Omega) is F, Borel_Sets -random_variable-like Function of Omega,REAL ; :: thesis: verum