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 A1: ( f is_measurable_on A & A c= dom f ) ; :: thesis: |.f.| is_measurable_on A
for r being real number holds A /\ (less_dom (|.f.|,(R_EAL r))) in S

proof

let r be real number ; :: thesis: A /\ (less_dom (|.f.|,(R_EAL r))) in S
reconsider r = r as Real by XREAL_0:def 1;
for x being set st x in less_dom (|.f.|,(R_EAL r)) holds
x in (less_dom (f,(R_EAL r))) /\ (great_dom (f,(R_EAL (- r))))

proof

let x be set ; :: thesis: ( x in less_dom (|.f.|,(R_EAL r)) implies x in (less_dom (f,(R_EAL r))) /\ (great_dom (f,(R_EAL (- r)))) )
assume A2: x in less_dom (|.f.|,(R_EAL r)) ; :: thesis: x in (less_dom (f,(R_EAL r))) /\ (great_dom (f,(R_EAL (- r))))
then A3: x in dom |.f.| by MESFUNC1:def 11;
A4: |.f.| . x < R_EAL r by A2, MESFUNC1:def 11;
reconsider x = x as Element of X by A2;
A5: x in dom f by A3, MESFUNC1:def 10;
A6: |.(f . x).| < R_EAL r by A3, A4, MESFUNC1:def 10;
then A7: - (R_EAL r) < f . x by EXTREAL2:10;
A8: f . x < R_EAL r by A6, EXTREAL2:10;
A9: - (R_EAL r) = - r by SUPINF_2:2;
A10: x in less_dom (f,(R_EAL r)) by A5, A8, MESFUNC1:def 11;
x in great_dom (f,(R_EAL (- r))) by A5, A7, A9, MESFUNC1:def 13;
hence x in (less_dom (f,(R_EAL r))) /\ (great_dom (f,(R_EAL (- r)))) by A10, XBOOLE_0:def 4; :: thesis: verum

end;

then A11: less_dom (|.f.|,(R_EAL r)) c= (less_dom (f,(R_EAL r))) /\ (great_dom (f,(R_EAL (- r)))) by TARSKI:def 3;
for x being set st x in (less_dom (f,(R_EAL r))) /\ (great_dom (f,(R_EAL (- r)))) holds
x in less_dom (|.f.|,(R_EAL r))

proof

let x be set ; :: thesis: ( x in (less_dom (f,(R_EAL r))) /\ (great_dom (f,(R_EAL (- r)))) implies x in less_dom (|.f.|,(R_EAL r)) )
assume A12: x in (less_dom (f,(R_EAL r))) /\ (great_dom (f,(R_EAL (- r)))) ; :: thesis: x in less_dom (|.f.|,(R_EAL r))
then A13: x in less_dom (f,(R_EAL r)) by XBOOLE_0:def 4;
A14: x in great_dom (f,(R_EAL (- r))) by A12, XBOOLE_0:def 4;
A15: x in dom f by A13, MESFUNC1:def 11;
A16: f . x < R_EAL r by A13, MESFUNC1:def 11;
A17: R_EAL (- r) < f . x by A14, MESFUNC1:def 13;
reconsider x = x as Element of X by A12;
A18: x in dom |.f.| by A15, MESFUNC1:def 10;
- (R_EAL r) = - r by SUPINF_2:2;
then |.(f . x).| < R_EAL r by A16, A17, EXTREAL2:11;
then |.f.| . x < R_EAL r by A18, MESFUNC1:def 10;
hence x in less_dom (|.f.|,(R_EAL r)) by A18, MESFUNC1:def 11; :: thesis: verum

end;

then (less_dom (f,(R_EAL r))) /\ (great_dom (f,(R_EAL (- r)))) c= less_dom (|.f.|,(R_EAL r)) by TARSKI:def 3;
then A19: less_dom (|.f.|,(R_EAL r)) = (less_dom (f,(R_EAL r))) /\ (great_dom (f,(R_EAL (- r)))) by A11, XBOOLE_0:def 10;
(A /\ (great_dom (f,(R_EAL (- r))))) /\ (less_dom (f,(R_EAL r))) in S by A1, MESFUNC1:32;
hence A /\ (less_dom (|.f.|,(R_EAL r))) in S by A19, XBOOLE_1:16; :: thesis: verum

end;

hence |.f.| is_measurable_on A by MESFUNC1:def 16; :: thesis: verum