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 A -measurable & A c= dom f holds
|.f.| is A -measurable
let S be SigmaField of X; :: thesis: for f being PartFunc of X,ExtREAL
for A being Element of S st f is A -measurable & A c= dom f holds
|.f.| is A -measurable
let f be PartFunc of X,ExtREAL; :: thesis: for A being Element of S st f is A -measurable & A c= dom f holds
|.f.| is A -measurable
let A be Element of S; :: thesis: ( f is A -measurable & A c= dom f implies |.f.| is A -measurable )
assume A1: ( f is A -measurable & A c= dom f ) ; :: thesis: |.f.| is A -measurable
for r being Real holds A /\ (less_dom (|.f.|,r)) in S

proof

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

proof

let x be object ; :: thesis: ( x in less_dom (|.f.|,r) implies x in (less_dom (f,r)) /\ (great_dom (f,(- r))) )
assume A2: x in less_dom (|.f.|,r) ; :: thesis: x in (less_dom (f,r)) /\ (great_dom (f,(- r)))
then A3: x in dom |.f.| by MESFUNC1:def 11;
A4: |.f.| . x < 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 by A3, A4, MESFUNC1:def 10;
then A7: - r < f . x by EXTREAL1:21;
A8: f . x < r by A6, EXTREAL1:21;
A9: x in less_dom (f,r) by A5, A8, MESFUNC1:def 11;
x in great_dom (f,(- r)) by A5, A7, MESFUNC1:def 13;
hence x in (less_dom (f,r)) /\ (great_dom (f,(- r))) by A9, XBOOLE_0:def 4; :: thesis: verum

end;

then A10: less_dom (|.f.|,r) c= (less_dom (f,r)) /\ (great_dom (f,(- r))) ;
for x being object st x in (less_dom (f,r)) /\ (great_dom (f,(- r))) holds
x in less_dom (|.f.|,r)

proof

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

end;

then (less_dom (f,r)) /\ (great_dom (f,(- r))) c= less_dom (|.f.|,r) ;
then A18: less_dom (|.f.|,r) = (less_dom (f,r)) /\ (great_dom (f,(- r))) by A10;
(A /\ (great_dom (f,(- r)))) /\ (less_dom (f,r)) in S by A1, MESFUNC1:32;
hence A /\ (less_dom (|.f.|,r)) in S by A18, XBOOLE_1:16; :: thesis: verum

end;

hence |.f.| is A -measurable ; :: thesis: verum