let Omega be non empty set ; :: thesis: for F being SigmaField of Omega
for A being Element of F holds chi (A,Omega) is random_variable of F, Borel_Sets
let F be SigmaField of Omega; :: thesis: for A being Element of F holds chi (A,Omega) is random_variable of F, Borel_Sets
let A be Element of F; :: thesis: chi (A,Omega) is random_variable of F, Borel_Sets
set chij = chi (A,Omega);
( chi (A,Omega) is Function & rng (chi (A,Omega)) c= REAL & dom (chi (A,Omega)) = Omega ) by FUNCT_3:def 3, VALUED_0:def 3;
then reconsider chij2 = chi (A,Omega) as Function of Omega,REAL by FUNCT_2:2;
reconsider MyOmega = Omega as Element of F by PROB_1:5;
chij2 is [#] F -measurable by MESFUNC2:29;
then chij2 is Real-Valued-Random-Variable of F ;
hence chi (A,Omega) is random_variable of F, Borel_Sets by RANDOM_3:7; :: thesis: verum