let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for F being Function of Omega,REAL st F is Real-Valued-Random-Variable of Sigma holds
{ x where x is Element of Borel_Sets : F " x is Element of Sigma } is SigmaField of REAL

let Sigma be SigmaField of Omega; :: thesis: for F being Function of Omega,REAL st F is Real-Valued-Random-Variable of Sigma holds
{ x where x is Element of Borel_Sets : F " x is Element of Sigma } is SigmaField of REAL

let F be Function of Omega,REAL; :: thesis: ( F is Real-Valued-Random-Variable of Sigma implies { x where x is Element of Borel_Sets : F " x is Element of Sigma } is SigmaField of REAL )
assume A1: F is Real-Valued-Random-Variable of Sigma ; :: thesis: { x where x is Element of Borel_Sets : F " x is Element of Sigma } is SigmaField of REAL
set S = { x where x is Element of Borel_Sets : F " x is Element of Sigma } ;
for x being object st x in { x where x is Element of Borel_Sets : F " x is Element of Sigma } holds
x in Borel_Sets
proof
let z be object ; :: thesis: ( z in { x where x is Element of Borel_Sets : F " x is Element of Sigma } implies z in Borel_Sets )
assume z in { x where x is Element of Borel_Sets : F " x is Element of Sigma } ; :: thesis:
then ex x being Element of Borel_Sets st
( x = z & F " x is Element of Sigma ) ;
hence z in Borel_Sets ; :: thesis: verum
end;
then A2: { x where x is Element of Borel_Sets : F " x is Element of Sigma } c= Borel_Sets ;
set r0 = the Element of REAL ;
A3: halfline the Element of REAL in Family_of_halflines ;
Family_of_halflines c= sigma Family_of_halflines by PROB_1:def 9;
then reconsider y0 = halfline the Element of REAL as Element of Borel_Sets by A3;
F " y0 is Element of Sigma by ;
then A4: y0 in { x where x is Element of Borel_Sets : F " x is Element of Sigma } ;
A5: for A being Subset of REAL st A in { x where x is Element of Borel_Sets : F " x is Element of Sigma } holds
A ` in { x where x is Element of Borel_Sets : F " x is Element of Sigma }
proof
let A be Subset of REAL; :: thesis: ( A in { x where x is Element of Borel_Sets : F " x is Element of Sigma } implies A ` in { x where x is Element of Borel_Sets : F " x is Element of Sigma } )
assume A in { x where x is Element of Borel_Sets : F " x is Element of Sigma } ; :: thesis: A ` in { x where x is Element of Borel_Sets : F " x is Element of Sigma }
then consider x being Element of Borel_Sets such that
A6: ( A = x & F " x is Element of Sigma ) ;
A7: F " () = () \ (F " x) by FUNCT_1:69
.= Omega \ (F " x) by FUNCT_2:40 ;
REAL is Element of Borel_Sets by PROB_1:5;
then A8: REAL \ x is Element of Borel_Sets by PROB_1:6;
Omega is Element of Sigma by PROB_1:5;
then Omega \ (F " x) is Element of Sigma by ;
hence A ` in { x where x is Element of Borel_Sets : F " x is Element of Sigma } by A6, A7, A8; :: thesis: verum
end;
for A1 being SetSequence of REAL st rng A1 c= { x where x is Element of Borel_Sets : F " x is Element of Sigma } holds
Intersection A1 in { x where x is Element of Borel_Sets : F " x is Element of Sigma }
proof
let A1 be SetSequence of REAL; :: thesis: ( rng A1 c= { x where x is Element of Borel_Sets : F " x is Element of Sigma } implies Intersection A1 in { x where x is Element of Borel_Sets : F " x is Element of Sigma } )
assume A9: rng A1 c= { x where x is Element of Borel_Sets : F " x is Element of Sigma } ; :: thesis: Intersection A1 in { x where x is Element of Borel_Sets : F " x is Element of Sigma }
then A10: rng A1 c= Borel_Sets by A2;
then A11: Intersection A1 in Borel_Sets by PROB_1:15;
reconsider B1 = Intersection A1 as Element of Borel_Sets by ;
deffunc H1( set ) -> Element of bool Omega = F " (A1 . \$1);
A12: for n being Element of NAT holds H1(n) is Element of Sigma
proof
let n be Element of NAT ; :: thesis: H1(n) is Element of Sigma
A1 . n in rng A1 by FUNCT_2:112;
then A1 . n in { x where x is Element of Borel_Sets : F " x is Element of Sigma } by A9;
then ex x being Element of Borel_Sets st
( x = A1 . n & F " x is Element of Sigma ) ;
hence H1(n) is Element of Sigma ; :: thesis: verum
end;
consider D being Function of NAT,Sigma such that
A13: for n being Element of NAT holds D . n = H1(n) from D in Funcs (NAT,Sigma) by FUNCT_2:8;
then A14: ex f being Function st
( D = f & dom f = NAT & rng f c= Sigma ) by FUNCT_2:def 2;
rng D c= bool Omega ;
then reconsider D = D as SetSequence of Omega by FUNCT_2:6;
A15: Intersection D in Sigma by ;
F " () = Intersection D by ;
hence Intersection A1 in { x where x is Element of Borel_Sets : F " x is Element of Sigma } by ; :: thesis: verum
end;
hence { x where x is Element of Borel_Sets : F " x is Element of Sigma } is SigmaField of REAL by ; :: thesis: verum