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

now

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

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

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 A3: x in less_dom ((max+ f),(R_EAL r)) ; :: thesis: x in less_dom (f,(R_EAL r))
then A4: x in dom (max+ f) by MESFUNC1:def 11;
A5: (max+ f) . x < R_EAL r by A3, MESFUNC1:def 11;
reconsider x = x as Element of X by A3;
A6: max ((f . x),0.) < R_EAL r by A4, A5, Def2;
then A7: f . x <= R_EAL r by XXREAL_0:30;
f . x <> R_EAL r

proof

assume A8: f . x = R_EAL r ; :: thesis: contradiction
then max ((f . x),0.) = 0. by A6, XXREAL_0:16;
hence contradiction by A6, A8, XXREAL_0:def 10; :: thesis: verum

end;

then A9: f . x < R_EAL r by A7, XXREAL_0:1;
x in dom f by A4, Def2;
hence x in less_dom (f,(R_EAL r)) by A9, MESFUNC1:def 11; :: thesis: verum

end;

then A10: less_dom ((max+ f),(R_EAL r)) c= less_dom (f,(R_EAL r)) by TARSKI:def 3;
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 A11: x in less_dom (f,(R_EAL r)) ; :: thesis: x in less_dom ((max+ f),(R_EAL r))
then A12: x in dom f by MESFUNC1:def 11;
A13: f . x < R_EAL r by A11, MESFUNC1:def 11;
reconsider x = x as Element of X by A11;
A14: x in dom (max+ f) by A12, Def2;

now

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

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

then max ((f . x),0.) = f . x by XXREAL_0:def 10;
then (max+ f) . x = f . x by A14, Def2;
hence x in less_dom ((max+ f),(R_EAL r)) by A13, A14, MESFUNC1:def 11; :: thesis: verum

end;

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

then max ((f . x),0.) = 0. by XXREAL_0:def 10;
then (max+ f) . x = 0. by A14, Def2;
hence x in less_dom ((max+ f),(R_EAL r)) by A2, A14, MESFUNC1:def 11; :: thesis: verum

end;

end;

end;

hence x in less_dom ((max+ f),(R_EAL r)) ; :: thesis: verum

end;

then less_dom (f,(R_EAL r)) c= less_dom ((max+ f),(R_EAL r)) by TARSKI:def 3;
then less_dom ((max+ f),(R_EAL r)) = less_dom (f,(R_EAL r)) by A10, XBOOLE_0:def 10;
hence A /\ (less_dom ((max+ f),(R_EAL r))) in S by A1, MESFUNC1:def 16; :: thesis: verum

end;

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

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 A16: x in less_dom ((max+ f),(R_EAL r)) ; :: thesis: contradiction
then A17: x in dom (max+ f) by MESFUNC1:def 11;
A18: (max+ f) . x < R_EAL r by A16, MESFUNC1:def 11;
(max+ f) . x = max ((f . x),0.) by A17, Def2;
hence contradiction by A15, A18, XXREAL_0:25; :: thesis: verum

end;

then less_dom ((max+ f),(R_EAL r)) = {} by SUBSET_1:4;
hence A /\ (less_dom ((max+ f),(R_EAL r))) in S by PROB_1:4; :: thesis: verum

end;

end;

end;

hence A /\ (less_dom ((max+ f),(R_EAL r))) in S ; :: thesis: verum

end;

hence max+ f is_measurable_on A by MESFUNC1:def 16; :: thesis: verum