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 & A c= dom f 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 & A c= dom f holds
max- f is A -measurable
let S be SigmaField of X; :: thesis: for A being Element of S st f is A -measurable & A c= dom f holds
max- f is A -measurable
let A be Element of S; :: thesis: ( f is A -measurable & A c= dom f implies max- f is A -measurable )
assume A1: ( f is A -measurable & A c= dom f ) ; :: 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

(- 1) (#) f is A -measurable by A1, MESFUNC1:37;
then A3: - f is A -measurable by Th9;
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 A4: x in less_dom ((max- f),r) ; :: thesis: x in less_dom ((- f),r)
then A5: x in dom (max- f) by MESFUNC1:def 11;
A6: (max- f) . x < r by A4, MESFUNC1:def 11;
reconsider x = x as Element of X by A4;
A7: max ((- (f . x)),0.) < r by A5, A6, Def3;
then A8: - (f . x) <= r by XXREAL_0:30;
- (f . x) <> r

proof

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

end;

then A10: - (f . x) < r by A8, XXREAL_0:1;
x in dom f by A5, Def3;
then A11: x in dom (- f) by MESFUNC1:def 7;
then (- f) . x = - (f . x) by MESFUNC1:def 7;
hence x in less_dom ((- f),r) by A10, A11, MESFUNC1:def 11; :: thesis: verum

end;

then A12: 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 A13: x in less_dom ((- f),r) ; :: thesis: x in less_dom ((max- f),r)
then A14: x in dom (- f) by MESFUNC1:def 11;
A15: (- f) . x < r by A13, MESFUNC1:def 11;
reconsider x = x as Element of X by A13;
x in dom f by A14, MESFUNC1:def 7;
then A16: x in dom (max- f) by Def3;

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 A16, Def3
.= (- f) . x by A14, MESFUNC1:def 7 ;
hence x in less_dom ((max- f),r) by A15, A16, 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 A16, Def3;
hence x in less_dom ((max- f),r) by A2, A16, 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 A12;
hence A /\ (less_dom ((max- f),r)) in S by A3; :: thesis: verum

end;

suppose A17: 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 A18: x in less_dom ((max- f),r) ; :: thesis: contradiction
then A19: x in dom (max- f) by MESFUNC1:def 11;
A20: (max- f) . x < r by A18, MESFUNC1:def 11;
(max- f) . x = max ((- (f . x)),0.) by A19, Def3;
hence contradiction by A17, A20, 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