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
A2: 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;
A3: 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)))
A5: x in dom |.f.| by A4, 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;
A9: - (R_EAL r) < f . x by A8, 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;
A13: x in great_dom f,(R_EAL (- r)) by A7, A9, A11, MESFUNC1:def 14;
thus x in (less_dom f,(R_EAL r)) /\ (great_dom f,(R_EAL (- r))) by A12, A13, XBOOLE_0:def 4; :: thesis: verum

end;

A14: less_dom |.f.|,(R_EAL r) c= (less_dom f,(R_EAL r)) /\ (great_dom f,(R_EAL (- r))) by A3, TARSKI:def 3;
A15: 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)
A17: x in less_dom f,(R_EAL r) by A16, 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;
A23: - (R_EAL r) = - r by SUPINF_2:3;
A24: |.(f . x).| < R_EAL r by A20, A21, A23, EXTREAL2:59;
A25: |.f.| . x < R_EAL r by A22, A24, MESFUNC1:def 10;
thus x in less_dom |.f.|,(R_EAL r) by A22, A25, MESFUNC1:def 12; :: thesis: verum

end;

A26: (less_dom f,(R_EAL r)) /\ (great_dom f,(R_EAL (- r))) c= less_dom |.f.|,(R_EAL r) by A15, TARSKI:def 3;
A27: less_dom |.f.|,(R_EAL r) = (less_dom f,(R_EAL r)) /\ (great_dom f,(R_EAL (- r))) by A14, A26, XBOOLE_0:def 10;
A28: (A /\ (great_dom f,(R_EAL (- r)))) /\ (less_dom f,(R_EAL r)) in S by A1, MESFUNC1:36;
thus A /\ (less_dom |.f.|,(R_EAL r)) in S by A27, A28, XBOOLE_1:16; :: thesis: verum

end;

thus |.f.| is_measurable_on A by A2, MESFUNC1:def 17; :: thesis: verum