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

for f being Function of Omega,REAL st f is Sigma, Borel_Sets -random_variable-like holds

( f is [#] Sigma -measurable & f is Real-Valued-Random-Variable of Sigma )

let Sigma be SigmaField of Omega; :: thesis: for f being Function of Omega,REAL st f is Sigma, Borel_Sets -random_variable-like holds

( f is [#] Sigma -measurable & f is Real-Valued-Random-Variable of Sigma )

let f be Function of Omega,REAL; :: thesis: ( f is Sigma, Borel_Sets -random_variable-like implies ( f is [#] Sigma -measurable & f is Real-Valued-Random-Variable of Sigma ) )

assume A1: f is Sigma, Borel_Sets -random_variable-like ; :: thesis: ( f is [#] Sigma -measurable & f is Real-Valued-Random-Variable of Sigma )

A2: for r being Element of REAL holds Omega /\ (less_dom (f,r)) in Sigma

for f being Function of Omega,REAL st f is Sigma, Borel_Sets -random_variable-like holds

( f is [#] Sigma -measurable & f is Real-Valued-Random-Variable of Sigma )

let Sigma be SigmaField of Omega; :: thesis: for f being Function of Omega,REAL st f is Sigma, Borel_Sets -random_variable-like holds

( f is [#] Sigma -measurable & f is Real-Valued-Random-Variable of Sigma )

let f be Function of Omega,REAL; :: thesis: ( f is Sigma, Borel_Sets -random_variable-like implies ( f is [#] Sigma -measurable & f is Real-Valued-Random-Variable of Sigma ) )

assume A1: f is Sigma, Borel_Sets -random_variable-like ; :: thesis: ( f is [#] Sigma -measurable & f is Real-Valued-Random-Variable of Sigma )

A2: for r being Element of REAL holds Omega /\ (less_dom (f,r)) in Sigma

proof

for r being Real holds ([#] Sigma) /\ (less_dom (f,r)) in Sigma
let r be Element of REAL ; :: thesis: Omega /\ (less_dom (f,r)) in Sigma

less_dom (f,r) = { w where w is Element of Omega : f . w < r } by A1, Th9;

then less_dom (f,r) is Element of Sigma by A1, Th9;

then less_dom (f,r) in Sigma ;

hence Omega /\ (less_dom (f,r)) in Sigma by XBOOLE_1:28; :: thesis: verum

end;less_dom (f,r) = { w where w is Element of Omega : f . w < r } by A1, Th9;

then less_dom (f,r) is Element of Sigma by A1, Th9;

then less_dom (f,r) in Sigma ;

hence Omega /\ (less_dom (f,r)) in Sigma by XBOOLE_1:28; :: thesis: verum

proof

hence
( f is [#] Sigma -measurable & f is Real-Valued-Random-Variable of Sigma )
by MESFUNC6:12; :: thesis: verum
let r be Real; :: thesis: ([#] Sigma) /\ (less_dom (f,r)) in Sigma

reconsider r = r as Element of REAL by XREAL_0:def 1;

([#] Sigma) /\ (less_dom (f,r)) in Sigma by A2;

hence ([#] Sigma) /\ (less_dom (f,r)) in Sigma ; :: thesis: verum

end;reconsider r = r as Element of REAL by XREAL_0:def 1;

([#] Sigma) /\ (less_dom (f,r)) in Sigma by A2;

hence ([#] Sigma) /\ (less_dom (f,r)) in Sigma ; :: thesis: verum