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

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL holds

( f is_integrable_on M iff ( max+ f is_integrable_on M & max- f is_integrable_on M ) )

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL holds

( f is_integrable_on M iff ( max+ f is_integrable_on M & max- f is_integrable_on M ) )

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL holds

( f is_integrable_on M iff ( max+ f is_integrable_on M & max- f is_integrable_on M ) )

let f be PartFunc of X,ExtREAL; :: thesis: ( f is_integrable_on M iff ( max+ f is_integrable_on M & max- f is_integrable_on M ) )

A8: max+ f is_integrable_on M and

A9: max- f is_integrable_on M ; :: thesis: f is_integrable_on M

consider E1 being Element of S such that

A10: ( E1 = dom (max+ f) & max+ f is E1 -measurable ) by A8, MESFUNC5:def 17;

consider E2 being Element of S such that

A11: ( E2 = dom (max- f) & max- f is E2 -measurable ) by A9, MESFUNC5:def 17;

A12: E1 = dom f by A10, MESFUNC2:def 2;

then E1 = E2 by A11, MESFUNC2:def 3;

then A13: f is E1 -measurable by A10, A11, A12, MESFUN11:10;

( max+ f is nonnegative & max- f is nonnegative ) by MESFUN11:5;

then ( max+ (max+ f) = max+ f & max+ (max- f) = max- f ) by MESFUN11:31;

then ( integral+ (M,(max+ f)) < +infty & integral+ (M,(max- f)) < +infty ) by A8, A9, MESFUNC5:def 17;

hence f is_integrable_on M by A12, A13, MESFUNC5:def 17; :: thesis: verum

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL holds

( f is_integrable_on M iff ( max+ f is_integrable_on M & max- f is_integrable_on M ) )

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL holds

( f is_integrable_on M iff ( max+ f is_integrable_on M & max- f is_integrable_on M ) )

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL holds

( f is_integrable_on M iff ( max+ f is_integrable_on M & max- f is_integrable_on M ) )

let f be PartFunc of X,ExtREAL; :: thesis: ( f is_integrable_on M iff ( max+ f is_integrable_on M & max- f is_integrable_on M ) )

hereby :: thesis: ( max+ f is_integrable_on M & max- f is_integrable_on M implies f is_integrable_on M )

assume that assume A1:
f is_integrable_on M
; :: thesis: ( max+ f is_integrable_on M & max- f is_integrable_on M )

then consider E being Element of S such that

A2: ( E = dom f & f is E -measurable ) by MESFUNC5:def 17;

A3: ( integral+ (M,(max+ f)) < +infty & integral+ (M,(max- f)) < +infty ) by A1, MESFUNC5:def 17;

A4: ( E = dom (max+ f) & E = dom (max- f) ) by A2, MESFUNC2:def 2, MESFUNC2:def 3;

A5: ( max+ f is E -measurable & max- f is E -measurable ) by A2, MESFUN11:10;

A6: ( max+ f is nonnegative & max- f is nonnegative ) by MESFUN11:5;

then A7: ( integral+ (M,(max+ (max+ f))) < +infty & integral+ (M,(max+ (max- f))) < +infty ) by A3, MESFUN11:31;

( integral+ (M,(max- (max+ f))) < +infty & integral+ (M,(max- (max- f))) < +infty ) by A4, A5, A6, MESFUN11:53;

hence ( max+ f is_integrable_on M & max- f is_integrable_on M ) by A4, A5, A7, MESFUNC5:def 17; :: thesis: verum

end;then consider E being Element of S such that

A2: ( E = dom f & f is E -measurable ) by MESFUNC5:def 17;

A3: ( integral+ (M,(max+ f)) < +infty & integral+ (M,(max- f)) < +infty ) by A1, MESFUNC5:def 17;

A4: ( E = dom (max+ f) & E = dom (max- f) ) by A2, MESFUNC2:def 2, MESFUNC2:def 3;

A5: ( max+ f is E -measurable & max- f is E -measurable ) by A2, MESFUN11:10;

A6: ( max+ f is nonnegative & max- f is nonnegative ) by MESFUN11:5;

then A7: ( integral+ (M,(max+ (max+ f))) < +infty & integral+ (M,(max+ (max- f))) < +infty ) by A3, MESFUN11:31;

( integral+ (M,(max- (max+ f))) < +infty & integral+ (M,(max- (max- f))) < +infty ) by A4, A5, A6, MESFUN11:53;

hence ( max+ f is_integrable_on M & max- f is_integrable_on M ) by A4, A5, A7, MESFUNC5:def 17; :: thesis: verum

A8: max+ f is_integrable_on M and

A9: max- f is_integrable_on M ; :: thesis: f is_integrable_on M

consider E1 being Element of S such that

A10: ( E1 = dom (max+ f) & max+ f is E1 -measurable ) by A8, MESFUNC5:def 17;

consider E2 being Element of S such that

A11: ( E2 = dom (max- f) & max- f is E2 -measurable ) by A9, MESFUNC5:def 17;

A12: E1 = dom f by A10, MESFUNC2:def 2;

then E1 = E2 by A11, MESFUNC2:def 3;

then A13: f is E1 -measurable by A10, A11, A12, MESFUN11:10;

( max+ f is nonnegative & max- f is nonnegative ) by MESFUN11:5;

then ( max+ (max+ f) = max+ f & max+ (max- f) = max- f ) by MESFUN11:31;

then ( integral+ (M,(max+ f)) < +infty & integral+ (M,(max- f)) < +infty ) by A8, A9, MESFUNC5:def 17;

hence f is_integrable_on M by A12, A13, MESFUNC5:def 17; :: thesis: verum