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 st ex A being Element of S st
( A = dom f & f is_measurable_on A ) holds
( f is_integrable_on M iff |.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 st ex A being Element of S st
( A = dom f & f is_measurable_on A ) holds
( f is_integrable_on M iff |.f.| is_integrable_on M )
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL st ex A being Element of S st
( A = dom f & f is_measurable_on A ) holds
( f is_integrable_on M iff |.f.| is_integrable_on M )
let f be PartFunc of X,ExtREAL; :: thesis: ( ex A being Element of S st
( A = dom f & f is_measurable_on A ) implies ( f is_integrable_on M iff |.f.| is_integrable_on M ) )
A1: dom |.f.| = dom (max- |.f.|) by MESFUNC2:def 3;
A2: dom f = dom (max- f) by MESFUNC2:def 3;

A3: now

let x be set ; :: thesis: ( x in dom |.f.| implies 0 <= |.f.| . x )
assume x in dom |.f.| ; :: thesis: 0 <= |.f.| . x
then |.f.| . x = |.(f . x).| by MESFUNC1:def 10;
hence 0 <= |.f.| . x by EXTREAL2:51; :: thesis: verum

end;

A4: dom f = dom (max+ f) by MESFUNC2:def 2;
A5: |.f.| = (max+ f) + (max- f) by MESFUNC2:26;
A6: max+ f is nonnegative by Lm1;
assume A7: ex A being Element of S st
( A = dom f & f is_measurable_on A ) ; :: thesis: ( f is_integrable_on M iff |.f.| is_integrable_on M )
then consider A being Element of S such that
A8: A = dom f and
A9: f is_measurable_on A ;
A10: max- f is_measurable_on A by A8, A9, MESFUNC2:28;
A11: |.f.| is_measurable_on A by A8, A9, MESFUNC2:29;
A12: A = dom |.f.| by A8, MESFUNC1:def 10;
A13: max+ f is_measurable_on A by A9, MESFUNC2:27;
A14: dom |.f.| = dom (max+ |.f.|) by MESFUNC2:def 2;

hereby :: thesis: ( |.f.| is_integrable_on M implies f is_integrable_on M )

A15: now

let x be set ; :: thesis: ( x in dom |.f.| implies (max+ |.f.|) . x = |.f.| . x )
assume A16: x in dom |.f.| ; :: thesis: (max+ |.f.|) . x = |.f.| . x
then |.f.| . x = |.(f . x).| by MESFUNC1:def 10;
then A17: 0 <= |.f.| . x by EXTREAL2:51;
(max+ |.f.|) . x = max ((|.f.| . x),0) by A14, A16, MESFUNC2:def 2;
hence (max+ |.f.|) . x = |.f.| . x by A17, XXREAL_0:def 10; :: thesis: verum

end;

now

let x be Element of X; :: thesis: ( x in dom (max- |.f.|) implies (max- |.f.|) . x = 0 )
assume x in dom (max- |.f.|) ; :: thesis: (max- |.f.|) . x = 0
then (max+ |.f.|) . x = |.f.| . x by A1, A15;
hence (max- |.f.|) . x = 0 by MESFUNC2:21; :: thesis: verum

end;

then A18: integral+ (M,(max- |.f.|)) = 0 by A1, A12, A11, Th93, MESFUNC2:28;
max- f is nonnegative by Lm1;
then A19: integral+ (M,((max+ f) + (max- f))) = (integral+ (M,(max+ f))) + (integral+ (M,(max- f))) by A8, A4, A2, A13, A10, A6, Lm10;
assume A20: f is_integrable_on M ; :: thesis: |.f.| is_integrable_on M
then A21: integral+ (M,(max+ f)) < +infty by Def17;
A22: integral+ (M,(max- f)) < +infty by A20, Def17;
|.f.| = max+ |.f.| by A14, A15, FUNCT_1:9;
then integral+ (M,(max+ |.f.|)) < +infty by A5, A21, A22, A19, XXREAL_0:4, XXREAL_3:16;
hence |.f.| is_integrable_on M by A12, A11, A18, Def17; :: thesis: verum

end;

assume |.f.| is_integrable_on M ; :: thesis: f is_integrable_on M
then Integral (M,|.f.|) < +infty by Th102;
then A23: integral+ (M,((max+ f) + (max- f))) < +infty by A12, A11, A5, A3, Th94, SUPINF_2:71;
max- f is nonnegative by Lm1;
then A24: integral+ (M,((max+ f) + (max- f))) = (integral+ (M,(max+ f))) + (integral+ (M,(max- f))) by A8, A4, A2, A13, A10, A6, Lm10;
-infty <> integral+ (M,(max- f)) by A8, A2, A10, Lm1, Th85;
then integral+ (M,(max+ f)) <> +infty by A24, A23, XXREAL_3:def 2;
then A25: integral+ (M,(max+ f)) < +infty by XXREAL_0:4;
-infty <> integral+ (M,(max+ f)) by A8, A4, A13, Lm1, Th85;
then integral+ (M,(max- f)) <> +infty by A24, A23, XXREAL_3:def 2;
then integral+ (M,(max- f)) < +infty by XXREAL_0:4;
hence f is_integrable_on M by A7, A25, Def17; :: thesis: verum