let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega

for s being Real

for f being Function of Omega,REAL st f = Omega --> s holds

f is Sigma, Borel_Sets -random_variable-like

let Sigma be SigmaField of Omega; :: thesis: for s being Real

for f being Function of Omega,REAL st f = Omega --> s holds

f is Sigma, Borel_Sets -random_variable-like

let s be Real; :: thesis: for f being Function of Omega,REAL st f = Omega --> s holds

f is Sigma, Borel_Sets -random_variable-like

let X be Function of Omega,REAL; :: thesis: ( X = Omega --> s implies X is Sigma, Borel_Sets -random_variable-like )

assume A0: X = Omega --> s ; :: thesis: X is Sigma, Borel_Sets -random_variable-like

X is Sigma, Borel_Sets -random_variable-like

for s being Real

for f being Function of Omega,REAL st f = Omega --> s holds

f is Sigma, Borel_Sets -random_variable-like

let Sigma be SigmaField of Omega; :: thesis: for s being Real

for f being Function of Omega,REAL st f = Omega --> s holds

f is Sigma, Borel_Sets -random_variable-like

let s be Real; :: thesis: for f being Function of Omega,REAL st f = Omega --> s holds

f is Sigma, Borel_Sets -random_variable-like

let X be Function of Omega,REAL; :: thesis: ( X = Omega --> s implies X is Sigma, Borel_Sets -random_variable-like )

assume A0: X = Omega --> s ; :: thesis: X is Sigma, Borel_Sets -random_variable-like

X is Sigma, Borel_Sets -random_variable-like

proof

hence
X is Sigma, Borel_Sets -random_variable-like
; :: thesis: verum
let x be set ; :: according to FINANCE1:def 5 :: thesis: ( x in Borel_Sets implies X " x in Sigma )

end;per cases
( s in x or not s in x )
;

end;

suppose A1:
s in x
; :: thesis: ( x in Borel_Sets implies X " x in Sigma )

for q being object holds

( q in { w where w is Element of Omega : X . w is Element of x } iff q in Omega )

not x is empty by A1;

then { w where w is Element of Omega : X . w is Element of x } = X " x by Lm1;

then X " x = Omega by A2;

then X " x is Element of Sigma by PROB_1:23;

hence ( x in Borel_Sets implies X " x in Sigma ) ; :: thesis: verum

end;( q in { w where w is Element of Omega : X . w is Element of x } iff q in Omega )

proof

then A2:
{ w where w is Element of Omega : X . w is Element of x } = Omega
by TARSKI:2;
let q be object ; :: thesis: ( q in { w where w is Element of Omega : X . w is Element of x } iff q in Omega )

then reconsider w = q as Element of Omega ;

X . w is Element of x by A1, FUNCOP_1:7, A0;

hence q in { w where w is Element of Omega : X . w is Element of x } ; :: thesis: verum

end;hereby :: thesis: ( q in Omega implies q in { w where w is Element of Omega : X . w is Element of x } )

assume
q in Omega
; :: thesis: q in { w where w is Element of Omega : X . w is Element of x } assume
q in { w where w is Element of Omega : X . w is Element of x }
; :: thesis: q in Omega

then ex w being Element of Omega st

( w = q & X . w is Element of x ) ;

hence q in Omega ; :: thesis: verum

end;then ex w being Element of Omega st

( w = q & X . w is Element of x ) ;

hence q in Omega ; :: thesis: verum

then reconsider w = q as Element of Omega ;

X . w is Element of x by A1, FUNCOP_1:7, A0;

hence q in { w where w is Element of Omega : X . w is Element of x } ; :: thesis: verum

not x is empty by A1;

then { w where w is Element of Omega : X . w is Element of x } = X " x by Lm1;

then X " x = Omega by A2;

then X " x is Element of Sigma by PROB_1:23;

hence ( x in Borel_Sets implies X " x in Sigma ) ; :: thesis: verum

suppose A3:
not s in x
; :: thesis: ( x in Borel_Sets implies X " x in Sigma )

for q being object holds

( q in X " x iff q in {} )

then X " x is Element of Sigma by PROB_1:22;

hence ( x in Borel_Sets implies X " x in Sigma ) ; :: thesis: verum

end;( q in X " x iff q in {} )

proof

then
X " x = {}
by TARSKI:2;
let q be object ; :: thesis: ( q in X " x iff q in {} )

end;now :: thesis: ( q in X " x implies q in {} )

hence
( q in X " x iff q in {} )
; :: thesis: verumassume
q in X " x
; :: thesis: q in {}

then ( q in dom X & X . q in x ) by FUNCT_1:def 7;

hence q in {} by A3, FUNCOP_1:7, A0; :: thesis: verum

end;then ( q in dom X & X . q in x ) by FUNCT_1:def 7;

hence q in {} by A3, FUNCOP_1:7, A0; :: thesis: verum

then X " x is Element of Sigma by PROB_1:22;

hence ( x in Borel_Sets implies X " x in Sigma ) ; :: thesis: verum