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 A -measurable holds
max+ f is A -measurable
let f be PartFunc of X,ExtREAL; :: thesis: for S being SigmaField of X
for A being Element of S st f is A -measurable holds
max+ f is A -measurable
let S be SigmaField of X; :: thesis: for A being Element of S st f is A -measurable holds
max+ f is A -measurable
let A be Element of S; :: thesis: ( f is A -measurable implies max+ f is A -measurable )
assume A1: f is A -measurable ; :: thesis: max+ f is A -measurable
for r being Real holds A /\ (less_dom ((max+ f),r)) in S

proof

let r be Real; :: thesis: A /\ (less_dom ((max+ f),r)) in S
reconsider r = r as Real ;

now :: thesis: A /\ (less_dom ((max+ f),r)) in S

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

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

for x being object st x in less_dom ((max+ f),r) holds
x in less_dom (f,r)

proof

let x be object ; :: thesis: ( x in less_dom ((max+ f),r) implies x in less_dom (f,r) )
assume A3: x in less_dom ((max+ f),r) ; :: thesis: x in less_dom (f,r)
then A4: x in dom (max+ f) by MESFUNC1:def 11;
A5: (max+ f) . x < r by A3, MESFUNC1:def 11;
reconsider x = x as Element of X by A3;
A6: max ((f . x),0.) < r by A4, A5, Def2;
then A7: f . x <= r by XXREAL_0:30;
f . x <> r

proof

assume A8: f . x = 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 by A7, XXREAL_0:1;
x in dom f by A4, Def2;
hence x in less_dom (f,r) by A9, MESFUNC1:def 11; :: thesis: verum

end;

then A10: less_dom ((max+ f),r) c= less_dom (f,r) ;
for x being object st x in less_dom (f,r) holds
x in less_dom ((max+ f),r)

proof

let x be object ; :: thesis: ( x in less_dom (f,r) implies x in less_dom ((max+ f),r) )
assume A11: x in less_dom (f,r) ; :: thesis: x in less_dom ((max+ f),r)
then A12: x in dom f by MESFUNC1:def 11;
A13: f . x < 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 :: thesis: x in less_dom ((max+ f),r)

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

suppose 0. <= f . x ; :: thesis: x in less_dom ((max+ f),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) by A13, A14, MESFUNC1:def 11; :: thesis: verum

end;

suppose not 0. <= f . x ; :: thesis: x in less_dom ((max+ f),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) by A2, A14, MESFUNC1:def 11; :: thesis: verum

end;

end;

end;

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

end;

then less_dom (f,r) c= less_dom ((max+ f),r) ;
then less_dom ((max+ f),r) = less_dom (f,r) by A10;
hence A /\ (less_dom ((max+ f),r)) in S by A1; :: thesis: verum

end;

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

for x being Element of X holds not x in less_dom ((max+ f),r)

proof

let x be Element of X; :: thesis: not x in less_dom ((max+ f),r)
assume A16: x in less_dom ((max+ f),r) ; :: thesis: contradiction
then A17: x in dom (max+ f) by MESFUNC1:def 11;
A18: (max+ f) . x < 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) = {} by SUBSET_1:4;
hence A /\ (less_dom ((max+ f),r)) in S by PROB_1:4; :: thesis: verum

end;

end;

end;

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

end;

hence max+ f is A -measurable ; :: thesis: verum