let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for f being Function of Omega,REAL st f is_random_variable_on Sigma, Borel_Sets holds
( f is_measurable_on [#] Sigma & 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_random_variable_on Sigma, Borel_Sets holds
( f is_measurable_on [#] Sigma & f is Real-Valued-Random-Variable of Sigma )
let f be Function of Omega,REAL; :: thesis: ( f is_random_variable_on Sigma, Borel_Sets implies ( f is_measurable_on [#] Sigma & f is Real-Valued-Random-Variable of Sigma ) )
assume A1: f is_random_variable_on Sigma, Borel_Sets ; :: thesis: ( f is_measurable_on [#] Sigma & f is Real-Valued-Random-Variable of Sigma )
A2: for r being Element of REAL holds Omega /\ (less_dom (f,r)) in Sigma

proof

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;

A3: for r being Real holds ([#] Sigma) /\ (less_dom (f,r)) in Sigma

proof

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;

f is Real-Valued-Random-Variable of Sigma by A3, MESFUNC6:12, RANDOM_1:def 2;
hence ( f is_measurable_on [#] Sigma & f is Real-Valued-Random-Variable of Sigma ) by A3, MESFUNC6:12; :: thesis: verum