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 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 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 holds
max+ f is_measurable_on A
let A be Element of S; :: thesis: ( f is_measurable_on A implies max+ f is_measurable_on A )
assume A1: f is_measurable_on A ; :: 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: 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 A6: x in less_dom (max+ f),(R_EAL r) ; :: thesis: x in less_dom f,(R_EAL r)
A7: x in dom (max+ f) by A6, MESFUNC1:def 12;
A8: (max+ f) . x < R_EAL r by A6, MESFUNC1:def 12;
reconsider x = x as Element of X by A6;
A9: max (f . x),0. < R_EAL r by A7, A8, Def2;
A10: f . x <= R_EAL r by A9, XXREAL_0:30;
A11: f . x <> R_EAL r

proof

assume A12: f . x = R_EAL r ; :: thesis: contradiction
A13: max (f . x),0. = 0. by A9, A12, XXREAL_0:16;
thus contradiction by A9, A12, A13, XXREAL_0:def 10; :: thesis: verum

end;

A14: f . x < R_EAL r by A10, A11, XXREAL_0:1;
A15: x in dom f by A7, Def2;
thus x in less_dom f,(R_EAL r) by A14, A15, MESFUNC1:def 12; :: thesis: verum

end;

A16: less_dom (max+ f),(R_EAL r) c= less_dom f,(R_EAL r) by A5, TARSKI:def 3;
A17: 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 A18: x in less_dom f,(R_EAL r) ; :: thesis: x in less_dom (max+ f),(R_EAL r)
A19: x in dom f by A18, MESFUNC1:def 12;
A20: f . x < R_EAL r by A18, MESFUNC1:def 12;
reconsider x = x as Element of X by A18;
A21: x in dom (max+ f) by A19, Def2;

A22: now

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

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

A24: max (f . x),0. = f . x by A23, XXREAL_0:def 10;
A25: (max+ f) . x = f . x by A21, A24, Def2;
thus x in less_dom (max+ f),(R_EAL r) by A20, A21, A25, MESFUNC1:def 12; :: thesis: verum

end;

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

A27: max (f . x),0. = 0. by A26, XXREAL_0:def 10;
A28: (max+ f) . x = 0. by A21, A27, Def2;
thus x in less_dom (max+ f),(R_EAL r) by A4, A21, A28, MESFUNC1:def 12; :: thesis: verum

end;

end;

end;

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

end;

A29: less_dom f,(R_EAL r) c= less_dom (max+ f),(R_EAL r) by A17, TARSKI:def 3;
A30: less_dom (max+ f),(R_EAL r) = less_dom f,(R_EAL r) by A16, A29, XBOOLE_0:def 10;
thus A /\ (less_dom (max+ f),(R_EAL r)) in S by A1, A30, MESFUNC1:def 17; :: thesis: verum

end;

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

A32: 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 A33: x in less_dom (max+ f),(R_EAL r) ; :: thesis: contradiction
A34: x in dom (max+ f) by A33, MESFUNC1:def 12;
A35: (max+ f) . x < R_EAL r by A33, MESFUNC1:def 12;
A36: (max+ f) . x = max (f . x),0. by A34, Def2;
thus contradiction by A31, A35, A36, XXREAL_0:25; :: thesis: verum

end;

A37: less_dom (max+ f),(R_EAL r) = {} by A32, SUBSET_1:10;
thus A /\ (less_dom (max+ f),(R_EAL r)) in S by A37, 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