let Omega be non empty set ; :: thesis: for F being SigmaField of Omega
for RV being random_variable of F, Borel_Sets
for K being Real holds chi ((((Omega --> K) - RV) " [.0,+infty.[),Omega) is Function of Omega,REAL
let F be SigmaField of Omega; :: thesis: for RV being random_variable of F, Borel_Sets
for K being Real holds chi ((((Omega --> K) - RV) " [.0,+infty.[),Omega) is Function of Omega,REAL
let RV be random_variable of F, Borel_Sets ; :: thesis: for K being Real holds chi ((((Omega --> K) - RV) " [.0,+infty.[),Omega) is Function of Omega,REAL
let K be Real; :: thesis: chi ((((Omega --> K) - RV) " [.0,+infty.[),Omega) is Function of Omega,REAL
set g2 = chi ((((Omega --> K) - RV) " [.0,+infty.[),Omega);
( chi ((((Omega --> K) - RV) " [.0,+infty.[),Omega) is Function of Omega,{0,1} & rng (chi ((((Omega --> K) - RV) " [.0,+infty.[),Omega)) c= REAL ) by H0;
then ( chi ((((Omega --> K) - RV) " [.0,+infty.[),Omega) is Function of (dom (chi ((((Omega --> K) - RV) " [.0,+infty.[),Omega))),REAL & dom (chi ((((Omega --> K) - RV) " [.0,+infty.[),Omega)) = Omega ) by FUNCT_2:2, FUNCT_2:def 1;
hence chi ((((Omega --> K) - RV) " [.0,+infty.[),Omega) is Function of Omega,REAL ; :: thesis: verum