let X be non empty set ; for S being SigmaField of X
for f being PartFunc of X,ExtREAL
for A being Element of S st A c= dom f holds
( f is A -measurable iff for r being Real holds A /\ (great_eq_dom (f,r)) in S )
let S be SigmaField of X; for f being PartFunc of X,ExtREAL
for A being Element of S st A c= dom f holds
( f is A -measurable iff for r being Real holds A /\ (great_eq_dom (f,r)) in S )
let f be PartFunc of X,ExtREAL; for A being Element of S st A c= dom f holds
( f is A -measurable iff for r being Real holds A /\ (great_eq_dom (f,r)) in S )
let A be Element of S; ( A c= dom f implies ( f is A -measurable iff for r being Real holds A /\ (great_eq_dom (f,r)) in S ) )
assume A1:
A c= dom f
; ( f is A -measurable iff for r being Real holds A /\ (great_eq_dom (f,r)) in S )
A2:
( f is A -measurable implies for r being Real holds A /\ (great_eq_dom (f,r)) in S )
( ( for r being Real holds A /\ (great_eq_dom (f,r)) in S ) implies f is A -measurable )
hence
( f is A -measurable iff for r being Real holds A /\ (great_eq_dom (f,r)) in S )
by A2; verum