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 ) )
assume A1: 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
A2: ( A = dom f & f is_measurable_on A ) ;
A3: ( dom |.f.| = dom (max+ |.f.|) & dom |.f.| = dom (max- |.f.|) & dom f = dom (max+ f) & dom f = dom (max- f) ) by MESFUNC2:def 2, MESFUNC2:def 3;
A4: ( A = dom |.f.| & |.f.| is_measurable_on A ) by A2, MESFUNC1:def 10, MESFUNC2:29;
A6: ( max+ f is_measurable_on A & max- f is_measurable_on A ) by A2, MESFUNC2:27, MESFUNC2:28;
A7: max+ f is nonnegative by Lm1;
then A8: -infty <> integral+ M,(max+ f) by A2, A3, A6, Th85;
A9: |.f.| = (max+ f) + (max- f) by MESFUNC2:26;

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

assume A10: f is_integrable_on M ; :: thesis: |.f.| is_integrable_on M

A11: now

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

end;

then A14: |.f.| = max+ |.f.| by A3, FUNCT_1:9;

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 A3, A11;
hence (max- |.f.|) . x = 0 by MESFUNC2:21; :: thesis: verum

end;

then A15: integral+ M,(max- |.f.|) = 0 by A3, A4, Th93, MESFUNC2:28;
A16: ( integral+ M,(max+ f) < +infty & integral+ M,(max- f) < +infty ) by A10, Def17;
max- f is nonnegative by Lm1;
then integral+ M,((max+ f) + (max- f)) = (integral+ M,(max+ f)) + (integral+ M,(max- f)) by A2, A3, A6, A7, Lm11;
then integral+ M,(max+ |.f.|) < +infty by A9, A14, A16, XXREAL_0:4, XXREAL_3:16;
hence |.f.| is_integrable_on M by A4, A15, Def17; :: thesis: verum

end;

assume A17: |.f.| is_integrable_on M ; :: thesis: f is_integrable_on M

B18: 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;

A19: max- f is nonnegative by Lm1;
then A20: -infty <> integral+ M,(max- f) by A2, A3, A6, Th85;
A21: integral+ M,((max+ f) + (max- f)) = (integral+ M,(max+ f)) + (integral+ M,(max- f)) by A2, A3, A6, A7, A19, Lm11;
( 0 <= integral+ M,(max+ |.f.|) & 0 <= integral+ M,(max- |.f.|) & -infty < Integral M,|.f.| & Integral M,|.f.| < +infty ) by A17, Th102;
then integral+ M,((max+ f) + (max- f)) < +infty by A4, A9, B18, Th94, SUPINF_2:71;
then ( integral+ M,(max+ f) <> +infty & integral+ M,(max- f) <> +infty ) by A8, A20, A21, XXREAL_3:def 2;
then ( integral+ M,(max+ f) < +infty & integral+ M,(max- f) < +infty ) by XXREAL_0:4;
hence f is_integrable_on M by A1, Def17; :: thesis: verum