let X be non empty set ; :: thesis: for f being PartFunc of X,ExtREAL
for S being SigmaField of X
for A being Element of S st f is_measurable_on A & A c= dom f holds
max- f is_measurable_on A
let f be PartFunc of X,ExtREAL ; :: thesis: for S being SigmaField of X
for A being Element of S st f is_measurable_on A & A c= dom f holds
max- f is_measurable_on A
let S be SigmaField of X; :: thesis: for A being Element of S st f is_measurable_on A & A c= dom f holds
max- f is_measurable_on A
let A be Element of S; :: thesis: ( f is_measurable_on A & A c= dom f implies max- f is_measurable_on A )
assume A1: ( f is_measurable_on A & A c= dom f ) ; :: thesis: max- f is_measurable_on A
A2: for r being real number holds A /\ (less_dom (max- f),(R_EAL r)) in S

proof

let r be real number ; :: thesis: A /\ (less_dom (max- f),(R_EAL r)) in S
reconsider r = r as Real by XREAL_0:def 1;

A3: now

per cases ( 0 < r or r <= 0 ) ;

suppose A4: 0 < r ; :: thesis: A /\ (less_dom (max- f),(R_EAL r)) in S

A5: (- 1) (#) f is_measurable_on A by A1, MESFUNC1:41;
A6: - f is_measurable_on A by A5, Th11;
A7: for x being set st x in less_dom (max- f),(R_EAL r) holds
x in less_dom (- f),(R_EAL r)

proof

let x be set ; :: thesis: ( x in less_dom (max- f),(R_EAL r) implies x in less_dom (- f),(R_EAL r) )
assume A8: x in less_dom (max- f),(R_EAL r) ; :: thesis: x in less_dom (- f),(R_EAL r)
A9: x in dom (max- f) by A8, MESFUNC1:def 12;
A10: (max- f) . x < R_EAL r by A8, MESFUNC1:def 12;
reconsider x = x as Element of X by A8;
A11: max (- (f . x)),0. < R_EAL r by A9, A10, Def3;
A12: - (f . x) <= R_EAL r by A11, XXREAL_0:30;
A13: - (f . x) <> R_EAL r

proof

assume A14: - (f . x) = R_EAL r ; :: thesis: contradiction
A15: max (- (f . x)),0. = 0. by A11, A14, XXREAL_0:16;
thus contradiction by A11, A14, A15, XXREAL_0:def 10; :: thesis: verum

end;

A16: - (f . x) < R_EAL r by A12, A13, XXREAL_0:1;
A17: x in dom f by A9, Def3;
A18: x in dom (- f) by A17, MESFUNC1:def 7;
A19: (- f) . x = - (f . x) by A18, MESFUNC1:def 7;
thus x in less_dom (- f),(R_EAL r) by A16, A18, A19, MESFUNC1:def 12; :: thesis: verum

end;

A20: less_dom (max- f),(R_EAL r) c= less_dom (- f),(R_EAL r) by A7, TARSKI:def 3;
A21: for x being set st x in less_dom (- f),(R_EAL r) holds
x in less_dom (max- f),(R_EAL r)

proof

let x be set ; :: thesis: ( x in less_dom (- f),(R_EAL r) implies x in less_dom (max- f),(R_EAL r) )
assume A22: x in less_dom (- f),(R_EAL r) ; :: thesis: x in less_dom (max- f),(R_EAL r)
A23: x in dom (- f) by A22, MESFUNC1:def 12;
A24: (- f) . x < R_EAL r by A22, MESFUNC1:def 12;
reconsider x = x as Element of X by A22;
A25: x in dom f by A23, MESFUNC1:def 7;
A26: x in dom (max- f) by A25, Def3;

A27: now

per cases ( 0. <= - (f . x) or not 0. <= - (f . x) ) ;

suppose A28: 0. <= - (f . x) ; :: thesis: x in less_dom (max- f),(R_EAL r)

A29: max (- (f . x)),0. = - (f . x) by A28, XXREAL_0:def 10;
A30: (max- f) . x = - (f . x) by A26, A29, Def3
.= (- f) . x by A23, MESFUNC1:def 7 ;
thus x in less_dom (max- f),(R_EAL r) by A24, A26, A30, MESFUNC1:def 12; :: thesis: verum

end;

suppose A31: not 0. <= - (f . x) ; :: thesis: x in less_dom (max- f),(R_EAL r)

A32: max (- (f . x)),0. = 0. by A31, XXREAL_0:def 10;
A33: (max- f) . x = 0. by A26, A32, Def3;
thus x in less_dom (max- f),(R_EAL r) by A4, A26, A33, MESFUNC1:def 12; :: thesis: verum

end;

end;

end;

thus x in less_dom (max- f),(R_EAL r) by A27; :: thesis: verum

end;

A34: less_dom (- f),(R_EAL r) c= less_dom (max- f),(R_EAL r) by A21, TARSKI:def 3;
A35: less_dom (max- f),(R_EAL r) = less_dom (- f),(R_EAL r) by A20, A34, XBOOLE_0:def 10;
thus A /\ (less_dom (max- f),(R_EAL r)) in S by A6, A35, MESFUNC1:def 17; :: thesis: verum

end;

suppose A36: r <= 0 ; :: thesis: A /\ (less_dom (max- f),(R_EAL r)) in S

A37: for x being Element of X holds not x in less_dom (max- f),(R_EAL r)

proof

let x be Element of X; :: thesis: not x in less_dom (max- f),(R_EAL r)
assume A38: x in less_dom (max- f),(R_EAL r) ; :: thesis: contradiction
A39: x in dom (max- f) by A38, MESFUNC1:def 12;
A40: (max- f) . x < R_EAL r by A38, MESFUNC1:def 12;
A41: (max- f) . x = max (- (f . x)),0. by A39, Def3;
thus contradiction by A36, A40, A41, XXREAL_0:25; :: thesis: verum

end;

A42: less_dom (max- f),(R_EAL r) = {} by A37, SUBSET_1:10;
thus A /\ (less_dom (max- f),(R_EAL r)) in S by A42, PROB_1:10; :: thesis: verum

end;

end;

end;

thus A /\ (less_dom (max- f),(R_EAL r)) in S by A3; :: thesis: verum

end;

thus max- f is_measurable_on A by A2, MESFUNC1:def 17; :: thesis: verum