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 A4: x in less_dom (|.f.|,(R_EAL r)) ; :: thesis: x in (less_dom (f,(R_EAL r))) /\ (great_dom (f,(R_EAL (- r))))
then A5: x in dom |.f.| by MESFUNC1:def 12;
A6: |.f.| . x < R_EAL r by A4, MESFUNC1:def 12;
reconsider x = x as Element of X by A4;
A7: x in dom f by A5, MESFUNC1:def 10;
A8: |.(f . x).| < R_EAL r by A5, A6, MESFUNC1:def 10;
then A9: - (R_EAL r) < f . x by EXTREAL2:58;
A10: f . x < R_EAL r by A8, EXTREAL2:58;
A11: - (R_EAL r) = - r by SUPINF_2:3;
A12: x in less_dom (f,(R_EAL r)) by A7, A10, MESFUNC1:def 12;
x in great_dom (f,(R_EAL (- r))) by A7, A9, A11, MESFUNC1:def 14;
hence x in (less_dom (f,(R_EAL r))) /\ (great_dom (f,(R_EAL (- r)))) by A12, XBOOLE_0:def 4; :: thesis: verum

end;

then A14: 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 A16: x in (less_dom (f,(R_EAL r))) /\ (great_dom (f,(R_EAL (- r)))) ; :: thesis: x in less_dom (|.f.|,(R_EAL r))
then A17: x in less_dom (f,(R_EAL r)) by XBOOLE_0:def 4;
A18: x in great_dom (f,(R_EAL (- r))) by A16, XBOOLE_0:def 4;
A19: x in dom f by A17, MESFUNC1:def 12;
A20: f . x < R_EAL r by A17, MESFUNC1:def 12;
A21: R_EAL (- r) < f . x by A18, MESFUNC1:def 14;
reconsider x = x as Element of X by A16;
A22: x in dom |.f.| by A19, MESFUNC1:def 10;
- (R_EAL r) = - r by SUPINF_2:3;
then |.(f . x).| < R_EAL r by A20, A21, EXTREAL2:59;
then |.f.| . x < R_EAL r by A22, MESFUNC1:def 10;
hence x in less_dom (|.f.|,(R_EAL r)) by A22, MESFUNC1:def 12; :: 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 A27: less_dom (|.f.|,(R_EAL r)) = (less_dom (f,(R_EAL r))) /\ (great_dom (f,(R_EAL (- r)))) by A14, XBOOLE_0:def 10;
(A /\ (great_dom (f,(R_EAL (- r))))) /\ (less_dom (f,(R_EAL r))) in S by A1, MESFUNC1:36;
hence A /\ (less_dom (|.f.|,(R_EAL r))) in S by A27, XBOOLE_1:16; :: thesis: verum

end;

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