let Omega be non empty set ; :: thesis:
let Sigma be SigmaField of Omega; :: thesis:
let X be Function of Omega,REAL; :: thesis:
assume A1: X is_random_variable_on Sigma, Borel_Sets ; :: thesis:
A2: for k being real number holds
( { w where w is Element of Omega : X . w >= k } is Element of Sigma & { w where w is Element of Omega : X . w < k } is Element of Sigma )

let k be real number ; :: thesis:
A3: for q being set holds
( ex w being Element of Omega st
( q = w & X . w >= k ) iff ex w being Element of Omega st
( q = w & X . w in [.k,+infty.] ) )

let q be set ; :: thesis:

now :: thesis:

assume ex w being Element of Omega st
( q = w & X . w in [.k,+infty.] ) ; :: thesis:
then consider w being Element of Omega such that
A4: ( q = w & X . w in [.k,+infty.] ) ;
X . w in { z where z is Element of ExtREAL : ( k <= z & z <= +infty ) } by A4, XXREAL_1:def 1;
then ex z being Element of ExtREAL st
( X . w = z & k <= z & z <= +infty ) ;
hence ex w being Element of Omega st
( q = w & X . w >= k ) by A4; :: thesis:

end;

hence ( ex w being Element of Omega st
( q = w & X . w >= k ) iff ex w being Element of Omega st
( q = w & X . w in [.k,+infty.] ) ) by XXREAL_1:219; :: thesis:

end;

A5: for x being set holds
( x in { w where w is Element of Omega : X . w >= k } iff x in { w where w is Element of Omega : X . w in [.k,+infty.[ } )

proof

let x be set ; :: thesis:
( x in { w where w is Element of Omega : X . w >= k } iff ex w being Element of Omega st
( x = w & X . w >= k ) ) ;
then A6: ( x in { w where w is Element of Omega : X . w >= k } iff ex w being Element of Omega st
( x = w & X . w in [.k,+infty.] ) ) by A3;
( x in { w where w is Element of Omega : X . w in [.k,+infty.] } iff x in { w where w is Element of Omega : X . w in [.k,+infty.[ } )

proof

hereby :: thesis:

assume x in { w where w is Element of Omega : X . w in [.k,+infty.] } ; :: thesis:
then consider w being Element of Omega such that
A7: ( w = x & X . w in [.k,+infty.] ) ;
X . w in { a where a is Element of ExtREAL : ( k <= a & a <= +infty ) } by A7, XXREAL_1:def 1;
then consider a being Element of ExtREAL such that
A8: ( X . w = a & k <= a & a <= +infty ) ;
A9: ( X . w = a & k <= a & a < +infty ) by A8, XXREAL_0:9;
{ z where z is Element of ExtREAL : ( k <= z & z < +infty ) } = [.k,+infty.[ by XXREAL_1:def 2;
then X . w in [.k,+infty.[ by A9;
hence x in { g where g is Element of Omega : X . g in [.k,+infty.[ } by A7; :: thesis:

end;

assume x in { w where w is Element of Omega : X . w in [.k,+infty.[ } ; :: thesis:
then consider w being Element of Omega such that
A10: ( w = x & X . w in [.k,+infty.[ ) ;
( w = x & X . w in { u where u is Element of ExtREAL : ( k <= u & u < +infty ) } ) by A10, XXREAL_1:def 2;
then ( w = x & ex u being Element of ExtREAL st
( u = X . w & k <= u & u < +infty ) ) ;
then ( w = x & X . w in { u where u is Element of ExtREAL : ( k <= u & u <= +infty ) } ) ;
then ( w = x & X . w in [.k,+infty.] ) by XXREAL_1:def 1;
hence x in { w where w is Element of Omega : X . w in [.k,+infty.] } ; :: thesis:

end;

hence ( x in { w where w is Element of Omega : X . w >= k } iff x in { w where w is Element of Omega : X . w in [.k,+infty.[ } ) by A6; :: thesis:

end;

k in REAL by XREAL_0:def 1;
then A11: not [.k,+infty.[ is empty by XXREAL_0:9, XXREAL_1:31;
A12: { w where w is Element of Omega : X . w >= k } = { w where w is Element of Omega : X . w is Element of [.k,+infty.[ }

proof

{ w where w is Element of Omega : X . w in [.k,+infty.[ } = { w where w is Element of Omega : X . w is Element of [.k,+infty.[ }

proof

for x being set holds
( x in { w where w is Element of Omega : X . w in [.k,+infty.[ } iff x in { w where w is Element of Omega : X . w is Element of [.k,+infty.[ } )

proof

let x be set ; :: thesis:

hereby :: thesis:

assume x in { w where w is Element of Omega : X . w in [.k,+infty.[ } ; :: thesis:
then ex w being Element of Omega st
( w = x & X . w in [.k,+infty.[ ) ;
hence x in { w where w is Element of Omega : X . w is Element of [.k,+infty.[ } ; :: thesis:

end;

assume x in { w where w is Element of Omega : X . w is Element of [.k,+infty.[ } ; :: thesis:
then consider w being Element of Omega such that
A13: ( w = x & X . w is Element of [.k,+infty.[ ) ;
thus x in { w where w is Element of Omega : X . w in [.k,+infty.[ } by A13, A11; :: thesis:

end;

hence { w where w is Element of Omega : X . w in [.k,+infty.[ } = { w where w is Element of Omega : X . w is Element of [.k,+infty.[ } by TARSKI:1; :: thesis:

end;

hence { w where w is Element of Omega : X . w >= k } = { w where w is Element of Omega : X . w is Element of [.k,+infty.[ } by A5, TARSKI:1; :: thesis:

end;

A14: ( [.k,+infty.[ is Element of Borel_Sets & ].-infty,k.[ is Element of Borel_Sets ) by Th3;
A15: for q being set holds
( ex w being Element of Omega st
( q = w & X . w < k ) iff ex w being Element of Omega st
( q = w & X . w in [.-infty,k.[ ) )

proof

let q be set ; :: thesis:

now :: thesis:

assume ex w being Element of Omega st
( q = w & X . w in [.-infty,k.[ ) ; :: thesis:
then consider w being Element of Omega such that
A16: ( q = w & X . w in [.-infty,k.[ ) ;
X . w in { z where z is Element of ExtREAL : ( -infty <= z & z < k ) } by A16, XXREAL_1:def 2;
then ex z being Element of ExtREAL st
( X . w = z & -infty <= z & z < k ) ;
hence ex w being Element of Omega st
( q = w & X . w < k ) by A16; :: thesis:

end;

hence ( ex w being Element of Omega st
( q = w & X . w < k ) iff ex w being Element of Omega st
( q = w & X . w in [.-infty,k.[ ) ) by XXREAL_1:221; :: thesis:

end;

for x being set holds
( x in { w where w is Element of Omega : X . w < k } iff x in { w where w is Element of Omega : X . w in ].-infty,k.[ } )

proof

let x be set ; :: thesis:
( x in { w where w is Element of Omega : X . w < k } iff ex w being Element of Omega st
( x = w & X . w < k ) ) ;
then A17: ( x in { w where w is Element of Omega : X . w < k } iff ex w being Element of Omega st
( x = w & X . w in [.-infty,k.[ ) ) by A15;
( x in { w where w is Element of Omega : X . w in [.-infty,k.[ } iff x in { w where w is Element of Omega : X . w in ].-infty,k.[ } )

proof

hereby :: thesis:

assume x in { w where w is Element of Omega : X . w in [.-infty,k.[ } ; :: thesis:
then consider w being Element of Omega such that
A18: ( w = x & X . w in [.-infty,k.[ ) ;
X . w in { a where a is Element of ExtREAL : ( -infty <= a & a < k ) } by A18, XXREAL_1:def 2;
then consider a being Element of ExtREAL such that
A19: ( X . w = a & -infty <= a & a < k ) ;
A20: ( X . w = a & -infty < a & a < k ) by A19, XXREAL_0:12;
{ z where z is Element of ExtREAL : ( -infty < z & z < k ) } = ].-infty,k.[ by XXREAL_1:def 4;
then X . w in ].-infty,k.[ by A20;
hence x in { g where g is Element of Omega : X . g in ].-infty,k.[ } by A18; :: thesis:

end;

assume x in { w where w is Element of Omega : X . w in ].-infty,k.[ } ; :: thesis:
then consider w being Element of Omega such that
A21: ( w = x & X . w in ].-infty,k.[ ) ;
( w = x & X . w in { u where u is Element of ExtREAL : ( -infty < u & u < k ) } ) by A21, XXREAL_1:def 4;
then ( w = x & ex u being Element of ExtREAL st
( u = X . w & -infty < u & u < k ) ) ;
then ( w = x & X . w in { u where u is Element of ExtREAL : ( -infty <= u & u < k ) } ) ;
then ( w = x & X . w in [.-infty,k.[ ) by XXREAL_1:def 2;
hence x in { w where w is Element of Omega : X . w in [.-infty,k.[ } ; :: thesis:

end;

hence ( x in { w where w is Element of Omega : X . w < k } iff x in { w where w is Element of Omega : X . w in ].-infty,k.[ } ) by A17; :: thesis:

end;

then A22: { w where w is Element of Omega : X . w < k } = { w where w is Element of Omega : X . w in ].-infty,k.[ } by TARSKI:1;
{ w where w is Element of Omega : X . w < k } is Element of Sigma

proof

A23: ( [.k,+infty.[ is Element of Borel_Sets & ].-infty,k.[ is Element of Borel_Sets ) by Th3;
k in REAL by XREAL_0:def 1;
then A24: not ].-infty,k.[ is empty by XXREAL_0:12, XXREAL_1:33;
for x being set holds
( x in { w where w is Element of Omega : X . w in ].-infty,k.[ } iff x in { w where w is Element of Omega : X . w is Element of ].-infty,k.[ } )

proof

let x be set ; :: thesis:

hereby :: thesis:

assume x in { w where w is Element of Omega : X . w in ].-infty,k.[ } ; :: thesis:
then ex w being Element of Omega st
( w = x & X . w in ].-infty,k.[ ) ;
hence x in { w where w is Element of Omega : X . w is Element of ].-infty,k.[ } ; :: thesis:

end;

assume x in { w where w is Element of Omega : X . w is Element of ].-infty,k.[ } ; :: thesis:
then consider w being Element of Omega such that
A25: ( w = x & X . w is Element of ].-infty,k.[ ) ;
thus x in { w where w is Element of Omega : X . w in ].-infty,k.[ } by A25, A24; :: thesis:

end;

then { w where w is Element of Omega : X . w < k } = { w where w is Element of Omega : X . w is Element of ].-infty,k.[ } by A22, TARSKI:1;
hence { w where w is Element of Omega : X . w < k } is Element of Sigma by A23, A1, Def5; :: thesis:

end;

hence ( { w where w is Element of Omega : X . w >= k } is Element of Sigma & { w where w is Element of Omega : X . w < k } is Element of Sigma ) by A14, A1, Def5, A12; :: thesis:

end;

A26: for k1, k2 being real number st k1 < k2 holds
{ w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } is Element of Sigma

proof

let k1, k2 be real number ; :: thesis:
assume A27: k1 < k2 ; :: thesis:
{ w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } is Element of Sigma

proof

for x being set holds
( x in { w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } iff x in { w where w is Element of Omega : X . w is Element of [.k1,k2.[ } )

proof

let x be set ; :: thesis:

hereby :: thesis:

assume x in { w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } ; :: thesis:
then consider w being Element of Omega such that
A28: ( x = w & k1 <= X . w & X . w < k2 ) ;
consider a being Element of ExtREAL such that
A29: a = R_EAL (X . w) ;
a = X . w by A29, MEASURE6:def 1;
then X . w in { z where z is Element of ExtREAL : ( k1 <= z & z < k2 ) } by A28;
then X . w is Element of [.k1,k2.[ by XXREAL_1:def 2;
hence x in { w1 where w1 is Element of Omega : X . w1 is Element of [.k1,k2.[ } by A28; :: thesis:

end;

assume x in { w where w is Element of Omega : X . w is Element of [.k1,k2.[ } ; :: thesis:
then consider w being Element of Omega such that
A30: ( x = w & X . w is Element of [.k1,k2.[ ) ;
A31: not [.k1,k2.[ is empty by A27, XXREAL_1:31;
X . w in [.k1,k2.[ by A30, A31;
then X . w in { a where a is Element of ExtREAL : ( k1 <= a & a < k2 ) } by XXREAL_1:def 2;
then ex a being Element of ExtREAL st
( a = X . w & k1 <= a & a < k2 ) ;
hence x in { w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } by A30; :: thesis:

end;

then A32: { w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } = { w where w is Element of Omega : X . w is Element of [.k1,k2.[ } by TARSKI:1;
( [.k2,k1.[ is Element of Borel_Sets & [.k1,k2.[ is Element of Borel_Sets ) by Th4;
hence { w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } is Element of Sigma by A1, Def5, A32; :: thesis:

end;

hence { w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } is Element of Sigma ; :: thesis:

end;

A33: for k1, k2 being real number st k1 <= k2 holds
{ w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } is Element of Sigma

proof

let k1, k2 be real number ; :: thesis:
assume A34: k1 <= k2 ; :: thesis:
for x being set holds
( x in { w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } iff x in { w where w is Element of Omega : X . w is Element of [.k1,k2.] } )

proof

let x be set ; :: thesis:

hereby :: thesis:

assume x in { w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } ; :: thesis:
then consider w being Element of Omega such that
A35: ( x = w & k1 <= X . w & X . w <= k2 ) ;
consider a being Element of ExtREAL such that
A36: a = R_EAL (X . w) ;
a = X . w by A36, MEASURE6:def 1;
then X . w in { z where z is Element of ExtREAL : ( k1 <= z & z <= k2 ) } by A35;
then X . w is Element of [.k1,k2.] by XXREAL_1:def 1;
hence x in { w1 where w1 is Element of Omega : X . w1 is Element of [.k1,k2.] } by A35; :: thesis:

end;

assume x in { w where w is Element of Omega : X . w is Element of [.k1,k2.] } ; :: thesis:
then consider w being Element of Omega such that
A37: ( x = w & X . w is Element of [.k1,k2.] ) ;
A38: not [.k1,k2.] is empty by A34, XXREAL_1:30;
X . w in [.k1,k2.] by A37, A38;
then X . w in { a where a is Element of ExtREAL : ( k1 <= a & a <= k2 ) } by XXREAL_1:def 1;
then ex a being Element of ExtREAL st
( a = X . w & k1 <= a & a <= k2 ) ;
hence x in { w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } by A37; :: thesis:

end;

then A39: { w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } = { w where w is Element of Omega : X . w is Element of [.k1,k2.] } by TARSKI:1;
( [.k1,k2.[ is Element of Borel_Sets & [.k1,k2.] is Element of Borel_Sets ) by Th8, Th4;
hence { w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } is Element of Sigma by A1, Def5, A39; :: thesis:

end;

A40: for r being real number holds less_dom (X,r) = { w where w is Element of Omega : X . w < r }

proof

let r be real number ; :: thesis:
for x being set holds
( x in less_dom (X,r) iff x in { w where w is Element of Omega : X . w < r } )

proof

let x be set ; :: thesis:
( x in less_dom (X,r) iff ( x in dom X & X . x < r ) ) by MESFUNC1:def 11;
then ( x in less_dom (X,r) iff ( x in Omega & X . x < r ) ) by FUNCT_2:def 1;
then ( x in less_dom (X,r) iff ex q being Element of Omega st
( q = x & X . q < r ) ) ;
hence ( x in less_dom (X,r) iff x in { w where w is Element of Omega : X . w < r } ) ; :: thesis:

end;

hence less_dom (X,r) = { w where w is Element of Omega : X . w < r } by TARSKI:1; :: thesis:

end;

A41: for r being real number holds great_eq_dom (X,r) = { w where w is Element of Omega : X . w >= r }

proof

let r be real number ; :: thesis:
for x being set holds
( x in great_eq_dom (X,r) iff x in { w where w is Element of Omega : X . w >= r } )

proof

let x be set ; :: thesis:
( x in great_eq_dom (X,r) iff ( x in dom X & X . x >= r ) ) by MESFUNC1:def 14;
then ( x in great_eq_dom (X,r) iff ( x in Omega & X . x >= r ) ) by FUNCT_2:def 1;
then ( x in great_eq_dom (X,r) iff ex q being Element of Omega st
( q = x & X . q >= r ) ) ;
hence ( x in great_eq_dom (X,r) iff x in { w where w is Element of Omega : X . w >= r } ) ; :: thesis:

end;

hence great_eq_dom (X,r) = { w where w is Element of Omega : X . w >= r } by TARSKI:1; :: thesis:

end;

A42: for r being real number holds eq_dom (X,r) = { w where w is Element of Omega : X . w = r }

proof

let r be real number ; :: thesis:
for x being set holds
( x in eq_dom (X,r) iff x in { w where w is Element of Omega : X . w = r } )

proof

let x be set ; :: thesis:
( x in eq_dom (X,r) iff ( x in dom X & X . x = r ) ) by MESFUNC1:def 15;
then ( x in eq_dom (X,r) iff ( x in Omega & X . x = r ) ) by FUNCT_2:def 1;
then ( x in eq_dom (X,r) iff ex q being Element of Omega st
( q = x & X . q = r ) ) ;
hence ( x in eq_dom (X,r) iff x in { w where w is Element of Omega : X . w = r } ) ; :: thesis:

end;

hence eq_dom (X,r) = { w where w is Element of Omega : X . w = r } by TARSKI:1; :: thesis:

end;

for r being real number holds eq_dom (X,r) is Element of Sigma

proof

let r be real number ; :: thesis:
for x being set holds
( x in { w where w is Element of Omega : ( r <= X . w & X . w <= r ) } iff x in { w where w is Element of Omega : X . w = r } )

proof

let x be set ; :: thesis:
( x in { w where w is Element of Omega : ( r <= X . w & X . w <= r ) } iff ex q being Element of Omega st
( x = q & r <= X . q & X . q <= r ) ) ;
then ( x in { w where w is Element of Omega : ( r <= X . w & X . w <= r ) } iff ex q being Element of Omega st
( x = q & X . q = r ) ) by XXREAL_0:1;
hence ( x in { w where w is Element of Omega : ( r <= X . w & X . w <= r ) } iff x in { w where w is Element of Omega : X . w = r } ) ; :: thesis:

end;

then { w where w is Element of Omega : ( r <= X . w & X . w <= r ) } = { w where w is Element of Omega : X . w = r } by TARSKI:1;
then { w where w is Element of Omega : X . w = r } is Element of Sigma by A33;
hence eq_dom (X,r) is Element of Sigma by A42; :: thesis:

end;

hence ( ( for k being real number holds
( { w where w is Element of Omega : X . w >= k } is Element of Sigma & { w where w is Element of Omega : X . w < k } is Element of Sigma ) ) & ( for k1, k2 being real number st k1 < k2 holds
{ w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } is Element of Sigma ) & ( for k1, k2 being real number st k1 <= k2 holds
{ w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } is Element of Sigma ) & ( for r being real number holds less_dom (X,r) = { w where w is Element of Omega : X . w < r } ) & ( for r being real number holds great_eq_dom (X,r) = { w where w is Element of Omega : X . w >= r } ) & ( for r being real number holds eq_dom (X,r) = { w where w is Element of Omega : X . w = r } ) & ( for r being real number holds eq_dom (X,r) is Element of Sigma ) ) by A2, A26, A33, A40, A41, A42; :: thesis: