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

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

hence
|.f.| is A -measurable
; :: thesis: verum
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)))

for x being object st x in (less_dom (f,r)) /\ (great_dom (f,(- r))) holds

x in 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;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

then A10:
less_dom (|.f.|,r) c= (less_dom (f,r)) /\ (great_dom (f,(- r)))
;
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;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

for x being object st x in (less_dom (f,r)) /\ (great_dom (f,(- r))) holds

x in less_dom (|.f.|,r)

proof

then
(less_dom (f,r)) /\ (great_dom (f,(- r))) c= less_dom (|.f.|,r)
;
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;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

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