let X be non empty set ; :: thesis: for S being SigmaField of X
for E being Element of S
for f being PartFunc of X,ExtREAL st E = {} holds
f is E -measurable
let S be SigmaField of X; :: thesis: for E being Element of S
for f being PartFunc of X,ExtREAL st E = {} holds
f is E -measurable
let E be Element of S; :: thesis: for f being PartFunc of X,ExtREAL st E = {} holds
f is E -measurable
let f be PartFunc of X,ExtREAL; :: thesis: ( E = {} implies f is E -measurable )
assume E = {} ; :: thesis: f is E -measurable
then for r being Real holds E /\ (less_dom (f,r)) in S ;
hence f is E -measurable by MESFUNC1:def 16; :: thesis: verum