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 A0: f is_random_variable_on Sigma, Borel_Sets ; :: thesis: ( f is_measurable_on [#] Sigma & f is Real-Valued-Random-Variable of Sigma )
J0: 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 A0, Th4;
then less_dom (f,r) is Element of Sigma by A0, Th4;
then less_dom (f,r) in Sigma ;
hence Omega /\ (less_dom (f,r)) in Sigma by XBOOLE_1:28; :: thesis: verum

end;

Fin0: for r being real number holds ([#] Sigma) /\ (less_dom (f,r)) in Sigma

proof

let r be real number ; :: 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 J0;
hence ([#] Sigma) /\ (less_dom (f,r)) in Sigma ; :: thesis: verum

end;

f is Real-Valued-Random-Variable of Sigma

proof

ex X being Element of Sigma st
( X = Omega & f is_measurable_on X )

proof

reconsider X = [#] Sigma as Element of Sigma ;
f is_measurable_on X by Fin0, MESFUNC6:12;
hence ex X being Element of Sigma st
( X = Omega & f is_measurable_on X ) ; :: thesis: verum

end;

hence f is Real-Valued-Random-Variable of Sigma by RANDOM_1:def 2; :: thesis: verum

end;

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