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

for f being Function of Omega,REAL holds

( f is Sigma, Borel_Sets -random_variable-like iff f is Real-Valued-Random-Variable of Sigma )

let Sigma be SigmaField of Omega; :: thesis: for f being Function of Omega,REAL holds

( f is Sigma, Borel_Sets -random_variable-like iff f is Real-Valued-Random-Variable of Sigma )

let f be Function of Omega,REAL; :: thesis: ( f is Sigma, Borel_Sets -random_variable-like iff f is Real-Valued-Random-Variable of Sigma )

thus ( f is Sigma, Borel_Sets -random_variable-like implies f is Real-Valued-Random-Variable of Sigma ) by FINANCE1:15; :: thesis: ( f is Real-Valued-Random-Variable of Sigma implies f is Sigma, Borel_Sets -random_variable-like )

assume A1: f is Real-Valued-Random-Variable of Sigma ; :: thesis: f is Sigma, Borel_Sets -random_variable-like

set B = { x where x is Element of Borel_Sets : f " x is Element of Sigma } ;

A2: { x where x is Element of Borel_Sets : f " x is Element of Sigma } = Borel_Sets by Th6, A1;

for x being set st x in Borel_Sets holds

f " x in Sigma

for f being Function of Omega,REAL holds

( f is Sigma, Borel_Sets -random_variable-like iff f is Real-Valued-Random-Variable of Sigma )

let Sigma be SigmaField of Omega; :: thesis: for f being Function of Omega,REAL holds

( f is Sigma, Borel_Sets -random_variable-like iff f is Real-Valued-Random-Variable of Sigma )

let f be Function of Omega,REAL; :: thesis: ( f is Sigma, Borel_Sets -random_variable-like iff f is Real-Valued-Random-Variable of Sigma )

thus ( f is Sigma, Borel_Sets -random_variable-like implies f is Real-Valued-Random-Variable of Sigma ) by FINANCE1:15; :: thesis: ( f is Real-Valued-Random-Variable of Sigma implies f is Sigma, Borel_Sets -random_variable-like )

assume A1: f is Real-Valued-Random-Variable of Sigma ; :: thesis: f is Sigma, Borel_Sets -random_variable-like

set B = { x where x is Element of Borel_Sets : f " x is Element of Sigma } ;

A2: { x where x is Element of Borel_Sets : f " x is Element of Sigma } = Borel_Sets by Th6, A1;

for x being set st x in Borel_Sets holds

f " x in Sigma

proof

hence
f is Sigma, Borel_Sets -random_variable-like
; :: thesis: verum
let x be set ; :: thesis: ( x in Borel_Sets implies f " x in Sigma )

assume x in Borel_Sets ; :: thesis: f " x in Sigma

then ex z being Element of Borel_Sets st

( z = x & f " z is Element of Sigma ) by A2;

hence f " x in Sigma ; :: thesis: verum

end;assume x in Borel_Sets ; :: thesis: f " x in Sigma

then ex z being Element of Borel_Sets st

( z = x & f " z is Element of Sigma ) by A2;

hence f " x in Sigma ; :: thesis: verum