let X be non empty set ; :: thesis: for S being SigmaField of X

for f being PartFunc of X,ExtREAL

for A being Element of S st A c= dom f holds

( f is A -measurable iff ( max+ f is A -measurable & max- f is A -measurable ) )

let S be SigmaField of X; :: thesis: for f being PartFunc of X,ExtREAL

for A being Element of S st A c= dom f holds

( f is A -measurable iff ( max+ f is A -measurable & max- f is A -measurable ) )

let f be PartFunc of X,ExtREAL; :: thesis: for A being Element of S st A c= dom f holds

( f is A -measurable iff ( max+ f is A -measurable & max- f is A -measurable ) )

let A be Element of S; :: thesis: ( A c= dom f implies ( f is A -measurable iff ( max+ f is A -measurable & max- f is A -measurable ) ) )

assume A1: A c= dom f ; :: thesis: ( f is A -measurable iff ( max+ f is A -measurable & max- f is A -measurable ) )

hence ( f is A -measurable implies ( max+ f is A -measurable & max- f is A -measurable ) ) by MESFUNC2:25, MESFUNC2:26; :: thesis: ( max+ f is A -measurable & max- f is A -measurable implies f is A -measurable )

assume A2: ( max+ f is A -measurable & max- f is A -measurable ) ; :: thesis: f is A -measurable

A3: dom (max- f) = dom f by MESFUNC2:def 3;

for f being PartFunc of X,ExtREAL

for A being Element of S st A c= dom f holds

( f is A -measurable iff ( max+ f is A -measurable & max- f is A -measurable ) )

let S be SigmaField of X; :: thesis: for f being PartFunc of X,ExtREAL

for A being Element of S st A c= dom f holds

( f is A -measurable iff ( max+ f is A -measurable & max- f is A -measurable ) )

let f be PartFunc of X,ExtREAL; :: thesis: for A being Element of S st A c= dom f holds

( f is A -measurable iff ( max+ f is A -measurable & max- f is A -measurable ) )

let A be Element of S; :: thesis: ( A c= dom f implies ( f is A -measurable iff ( max+ f is A -measurable & max- f is A -measurable ) ) )

assume A1: A c= dom f ; :: thesis: ( f is A -measurable iff ( max+ f is A -measurable & max- f is A -measurable ) )

hence ( f is A -measurable implies ( max+ f is A -measurable & max- f is A -measurable ) ) by MESFUNC2:25, MESFUNC2:26; :: thesis: ( max+ f is A -measurable & max- f is A -measurable implies f is A -measurable )

assume A2: ( max+ f is A -measurable & max- f is A -measurable ) ; :: thesis: f is A -measurable

A3: dom (max- f) = dom f by MESFUNC2:def 3;

now :: thesis: for r being Real holds A /\ (less_dom (f,r)) in S

hence
f is A -measurable
by MESFUNC1:def 16; :: thesis: verumlet r be Real; :: thesis: A /\ (less_dom (f,b_{1})) in S

end;