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

less_dom (max+ f),(R_EAL r) = less_dom f,(R_EAL r)

proof

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

proof

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

end;

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

end;

then A9: 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 A10: x in less_dom f,(R_EAL r) ; :: thesis: x in less_dom (max+ f),(R_EAL r)
then A11: ( x in dom f & f . x < R_EAL r ) by MESFUNC1:def 12;
A12: f . x < R_EAL r by A10, MESFUNC1:def 12;
reconsider x = x as Element of X by A10;
A13: x in dom (max+ f) by A11, 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 A13, Def2;
hence x in less_dom (max+ f),(R_EAL r) by A12, A13, MESFUNC1:def 12; :: 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 A13, Def2;
hence x in less_dom (max+ f),(R_EAL r) by A2, A13, MESFUNC1:def 12; :: 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;
hence less_dom (max+ f),(R_EAL r) = less_dom f,(R_EAL r) by A9, XBOOLE_0:def 10; :: thesis: verum

end;

hence A /\ (less_dom (max+ f),(R_EAL r)) in S by A1, MESFUNC1:def 17; :: thesis: verum

end;

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

end;

then less_dom (max+ f),(R_EAL r) = {} by SUBSET_1:10;
hence A /\ (less_dom (max+ f),(R_EAL r)) in S by PROB_1:10; :: 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 17; :: thesis: verum