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

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 }

Intersection A1 in { x where x is Element of Borel_Sets : F " x is Element of Sigma }

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

then A2:
{ x where x is Element of Borel_Sets : F " x is Element of Sigma } c= Borel_Sets
;
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;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

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

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
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;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

Intersection A1 in { x where x is Element of Borel_Sets : F " x is Element of Sigma }

proof

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
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_{1}( set ) -> Element of bool Omega = F " (A1 . $1);

A12: for n being Element of NAT holds H_{1}(n) is Element of Sigma

A13: for n being Element of NAT holds D . n = H_{1}(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;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

A12: for n being Element of NAT holds H

proof

consider D being Function of NAT,Sigma such that
let n be Element of NAT ; :: thesis: H_{1}(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_{1}(n) is Element of Sigma
; :: thesis: verum

end;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

A13: for n being Element of NAT holds D . n = H

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