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 (((RV - (Omega --> K)) " [.0,+infty.[),Omega) is random_variable of F, Borel_Sets
let F be SigmaField of Omega; :: thesis: for RV being random_variable of F, Borel_Sets
for K being Real holds chi (((RV - (Omega --> K)) " [.0,+infty.[),Omega) is random_variable of F, Borel_Sets
let RV be random_variable of F, Borel_Sets ; :: thesis: for K being Real holds chi (((RV - (Omega --> K)) " [.0,+infty.[),Omega) is random_variable of F, Borel_Sets
let K be Real; :: thesis: chi (((RV - (Omega --> K)) " [.0,+infty.[),Omega) is random_variable of F, Borel_Sets
reconsider K = K as Element of REAL by XREAL_0:def 1;
Omega --> K is random_variable of F, Borel_Sets by FINANCE3:10;
then (RV - (Omega --> K)) " [.0,+infty.[ is Element of F by Lemma00;
hence chi (((RV - (Omega --> K)) " [.0,+infty.[),Omega) is random_variable of F, Borel_Sets by ZZZ; :: thesis: verum