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: z in Borel_Sets
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 Th4, A1;
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 " (REAL \ x) = (F " REAL) \ (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 A6, PROB_1:6;
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 PROB_1:15, A10;
deffunc H₁( set ) -> Element of bool Omega = F " (A1 . $1);
A12: for n being Element of NAT holds H₁(n) is Element of Sigma

proof

let n be Element of NAT ; :: thesis: H₁(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 H₁(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 = H₁(n) from FUNCT_2:sch 9(A12);
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 A14, PROB_1:15;
F " (Intersection A1) = Intersection D by A13, Th3;
hence Intersection A1 in { x where x is Element of Borel_Sets : F " x is Element of Sigma } by A11, A15; :: thesis: verum

end;

hence { x where x is Element of Borel_Sets : F " x is Element of Sigma } is SigmaField of REAL by PROB_1:15, A4, A5, XBOOLE_1:1, A2; :: thesis: verum