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 " ].-infty,r.[ 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 " ].-infty,r.[ 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 " ].-infty,r.[ in Sigma

let r be Real; :: thesis: ( F is Real-Valued-Random-Variable of Sigma implies F " ].-infty,r.[ in Sigma )

assume F is Real-Valued-Random-Variable of Sigma ; :: thesis: F " ].-infty,r.[ 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 " ].-infty,r.[ iff z in ([#] Sigma) /\ (less_dom (F,r)) )

for F being Function of Omega,REAL

for r being Real st F is Real-Valued-Random-Variable of Sigma holds

F " ].-infty,r.[ 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 " ].-infty,r.[ 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 " ].-infty,r.[ in Sigma

let r be Real; :: thesis: ( F is Real-Valued-Random-Variable of Sigma implies F " ].-infty,r.[ in Sigma )

assume F is Real-Valued-Random-Variable of Sigma ; :: thesis: F " ].-infty,r.[ 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 " ].-infty,r.[ iff z in ([#] Sigma) /\ (less_dom (F,r)) )

proof

hence
F " ].-infty,r.[ in Sigma
by A2, TARSKI:2; :: thesis: verum
let z be object ; :: thesis: ( z in F " ].-infty,r.[ iff z in ([#] Sigma) /\ (less_dom (F,r)) )

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 XXREAL_0:12, FUNCT_2:5, MESFUNC1:def 11, A6;

then F . z in { p where p is Real : ( -infty < p & p < r ) } ;

then F . z in ].-infty,r.[ by RCOMP_1:def 2;

hence z in F " ].-infty,r.[ by A7, FUNCT_1:def 7; :: thesis: verum

end;hereby :: thesis: ( z in ([#] Sigma) /\ (less_dom (F,r)) implies z in F " ].-infty,r.[ )

assume
z in ([#] Sigma) /\ (less_dom (F,r))
; :: thesis: z in F " ].-infty,r.[assume A3:
z in F " ].-infty,r.[
; :: thesis: z in ([#] Sigma) /\ (less_dom (F,r))

then A4: ( z in dom F & F . z in ].-infty,r.[ ) 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 A4, A5, MESFUNC1:def 11;

hence z in ([#] Sigma) /\ (less_dom (F,r)) by A3, XBOOLE_0:def 4; :: thesis: verum

end;then A4: ( z in dom F & F . z in ].-infty,r.[ ) 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 A4, A5, MESFUNC1:def 11;

hence z in ([#] Sigma) /\ (less_dom (F,r)) by A3, XBOOLE_0:def 4; :: thesis: verum

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 XXREAL_0:12, FUNCT_2:5, MESFUNC1:def 11, A6;

then F . z in { p where p is Real : ( -infty < p & p < r ) } ;

then F . z in ].-infty,r.[ by RCOMP_1:def 2;

hence z in F " ].-infty,r.[ by A7, FUNCT_1:def 7; :: thesis: verum