let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for F being Function of Omega,REAL
for r being Real st F is Real-Valued-Random-Variable of Sigma holds
F " in Sigma

let Sigma be SigmaField of Omega; :: thesis: for F being Function of Omega,REAL
for r being Real st F is Real-Valued-Random-Variable of Sigma holds
F " in Sigma

let F be Function of Omega,REAL; :: thesis: for r being Real st F is Real-Valued-Random-Variable of Sigma holds
F " in Sigma

let r be Real; :: thesis: ( F is Real-Valued-Random-Variable of Sigma implies F " in Sigma )
assume F is Real-Valued-Random-Variable of Sigma ; :: thesis: F " in Sigma
then F is [#] Sigma -measurable by RANDOM_1:def 2;
then A2: ([#] Sigma) /\ (less_dom (F,r)) in Sigma by MESFUNC6:12;
for z being object holds
( z in F " iff z in ([#] Sigma) /\ (less_dom (F,r)) )
proof
let z be object ; :: thesis: ( z in F " iff z in ([#] Sigma) /\ (less_dom (F,r)) )
hereby :: thesis: ( z in ([#] Sigma) /\ (less_dom (F,r)) implies z in F " )
assume A3: z in F " ; :: thesis: z in ([#] Sigma) /\ (less_dom (F,r))
then A4: ( z in dom F & F . z in ) by FUNCT_1:def 7;
then F . z in { p where p is Real : ( -infty < p & p < r ) } by RCOMP_1:def 2;
then consider w being Real such that
A5: ( F . z = w & -infty < w & w < r ) ;
z in less_dom (F,r) by ;
hence z in ([#] Sigma) /\ (less_dom (F,r)) by ; :: thesis: verum
end;
assume z in ([#] Sigma) /\ (less_dom (F,r)) ; :: thesis: z in F "
then A6: ( z in [#] Sigma & z in less_dom (F,r) ) by XBOOLE_0:def 4;
then A7: ( z in dom F & F . z < r ) by MESFUNC1:def 11;
( -infty < F . z & F . z < r ) by ;
then F . z in { p where p is Real : ( -infty < p & p < r ) } ;
then F . z in by RCOMP_1:def 2;
hence z in F " by ; :: thesis: verum
end;
hence F " in Sigma by ; :: thesis: verum