let Omega be non empty set ; 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; for A being Element of F holds chi (A,Omega) is random_variable of F, Borel_Sets
let A be Element of F; 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; verum