let X be non empty set ; :: thesis: for S being SigmaField of X
for f being PartFunc of X,ExtREAL
for A being Element of S st f is_measurable_on A & A c= dom f holds
- f is_measurable_on A
let S be SigmaField of X; :: thesis: for f being PartFunc of X,ExtREAL
for A being Element of S st f is_measurable_on A & A c= dom f holds
- f is_measurable_on A
let f be PartFunc of X,ExtREAL; :: thesis: for A being Element of S st f is_measurable_on A & A c= dom f holds
- f is_measurable_on A
let A be Element of S; :: thesis: ( f is_measurable_on A & A c= dom f implies - f is_measurable_on A )
assume that
A1: f is_measurable_on A and
A2: A c= dom f ; :: thesis: - f is_measurable_on A
- f = (- 1) (#) f by MESFUNC2:9;
hence - f is_measurable_on A by A1, A2, MESFUNC1:37; :: thesis: verum