let Omega be non empty set ; :: thesis: for F being SigmaField of Omega holds chi (Omega,Omega) is_random_variable_on F, Borel_Sets
let F be SigmaField of Omega; :: thesis: chi (Omega,Omega) is_random_variable_on F, Borel_Sets
set g2 = chi (Omega,Omega);
( chi (Omega,Omega) is Function of Omega,{0,1} & rng (chi (Omega,Omega)) c= REAL ) by H0;
then ( chi (Omega,Omega) is Function of (dom (chi (Omega,Omega))),REAL & dom (chi (Omega,Omega)) = Omega ) by FUNCT_2:2, FUNCT_2:def 1;
then reconsider g2 = chi (Omega,Omega) as Function of Omega,REAL ;
for x being set st x in Borel_Sets holds
g2 " x in F

proof

let x be set ; :: thesis: ( x in Borel_Sets implies g2 " x in F )
assume x in Borel_Sets ; :: thesis: g2 " x in F
then reconsider x = x as Element of Borel_Sets ;
g2 " x in F

proof

per cases ( ( 1 in x & 0 in x ) or ( 1 in x & not 0 in x ) or ( not 1 in x & 0 in x ) or ( not 1 in x & not 0 in x ) ) ;

suppose SB1: ( 1 in x & 0 in x ) ; :: thesis: g2 " x in F

g2 " x = Omega

proof

for x2 being object holds
( x2 in g2 " x iff x2 in Omega )

proof

let x2 be object ; :: thesis: ( x2 in g2 " x iff x2 in Omega )
( x2 in Omega implies x2 in g2 " x )

proof

assume ASSI: x2 in Omega ; :: thesis: x2 in g2 " x
then L0: g2 . x2 in x by SB1, FUNCT_3:def 3;
x2 in dom g2 by ASSI, FUNCT_2:def 1;
hence x2 in g2 " x by L0, FUNCT_1:def 7; :: thesis: verum

end;

hence ( x2 in g2 " x iff x2 in Omega ) ; :: thesis: verum

end;

hence g2 " x = Omega by TARSKI:2; :: thesis: verum

end;

hence g2 " x in F by PROB_1:5; :: thesis: verum

end;

suppose SB1: ( 1 in x & not 0 in x ) ; :: thesis: g2 " x in F

for x2 being object holds
( x2 in g2 " x iff x2 in Omega )

proof

let x2 be object ; :: thesis: ( x2 in g2 " x iff x2 in Omega )
( x2 in Omega implies x2 in g2 " x )

proof

assume x2 in Omega ; :: thesis: x2 in g2 " x
then reconsider x2 = x2 as Element of Omega ;
l0: dom g2 = Omega by FUNCT_2:def 1;
g2 . x2 = 1 by FUNCT_3:def 3;
hence x2 in g2 " x by l0, FUNCT_1:def 7, SB1; :: thesis: verum

end;

hence ( x2 in g2 " x iff x2 in Omega ) ; :: thesis: verum

end;

then g2 " x = Omega by TARSKI:2;
hence g2 " x in F by PROB_1:5; :: thesis: verum

end;

suppose SB1: ( not 1 in x & 0 in x ) ; :: thesis: g2 " x in F

g2 " x c= {}

proof

let x2 be object ; :: according to TARSKI:def 3 :: thesis: ( not x2 in g2 " x or x2 in {} )
assume ASSK: x2 in g2 " x ; :: thesis: x2 in {}
then reconsider x2 = x2 as Element of Omega ;
g2 . x2 in x by ASSK, FUNCT_1:def 7;
hence x2 in {} by FUNCT_3:def 3, SB1; :: thesis: verum

end;

then P1: g2 " x = {} ;
{} is Event of F by PROB_1:22;
hence g2 " x in F by P1; :: thesis: verum

end;

suppose SB1: ( not 1 in x & not 0 in x ) ; :: thesis: g2 " x in F

g2 " x c= {}

proof

let w3 be object ; :: according to TARSKI:def 3 :: thesis: ( not w3 in g2 " x or w3 in {} )
assume w3 in g2 " x ; :: thesis: w3 in {}
then consider w3 being object such that
L1: w3 in g2 " x ;
reconsider w3 = w3 as Element of Omega by L1;
not g2 . w3 in x by SB1, FUNCT_3:def 3;
hence w3 in {} by L1, FUNCT_1:def 7; :: thesis: verum

end;

then g2 " x = {} ;
hence g2 " x in F by PROB_1:4; :: thesis: verum

end;

end;

end;

hence g2 " x in F ; :: thesis: verum

end;

hence chi (Omega,Omega) is_random_variable_on F, Borel_Sets ; :: thesis: verum