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 A -measurable ) 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 A -measurable ) 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 A -measurable ) 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 A -measurable ) 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;

A5: |.f.| = (max+ f) + (max- f) by MESFUNC2:24;

A6: max+ f is nonnegative by Lm1;

assume A7: ex A being Element of S st

( A = dom f & f is A -measurable ) ; :: 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 A -measurable ;

A10: max- f is A -measurable by A8, A9, MESFUNC2:26;

A11: |.f.| is A -measurable by A8, A9, MESFUNC2:27;

A12: A = dom |.f.| by A8, MESFUNC1:def 10;

A13: max+ f is A -measurable by A9, MESFUNC2:25;

A14: dom |.f.| = dom (max+ |.f.|) by MESFUNC2:def 2;

then Integral (M,|.f.|) < +infty by Th96;

then A23: integral+ (M,((max+ f) + (max- f))) < +infty by A12, A11, A5, A3, Th88, SUPINF_2:52;

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, Th79;

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, Th79;

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; :: thesis: verum

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 A -measurable ) 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 A -measurable ) 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 A -measurable ) 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 A -measurable ) 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 :: thesis: for x being object st x in dom |.f.| holds

0 <= |.f.| . x

A4:
dom f = dom (max+ f)
by MESFUNC2:def 2;0 <= |.f.| . x

let x be object ; :: 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 EXTREAL1:14; :: thesis: verum

end;assume x in dom |.f.| ; :: thesis: 0 <= |.f.| . x

then |.f.| . x = |.(f . x).| by MESFUNC1:def 10;

hence 0 <= |.f.| . x by EXTREAL1:14; :: thesis: verum

A5: |.f.| = (max+ f) + (max- f) by MESFUNC2:24;

A6: max+ f is nonnegative by Lm1;

assume A7: ex A being Element of S st

( A = dom f & f is A -measurable ) ; :: 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 A -measurable ;

A10: max- f is A -measurable by A8, A9, MESFUNC2:26;

A11: |.f.| is A -measurable by A8, A9, MESFUNC2:27;

A12: A = dom |.f.| by A8, MESFUNC1:def 10;

A13: max+ f is A -measurable by A9, MESFUNC2:25;

A14: dom |.f.| = dom (max+ |.f.|) by MESFUNC2:def 2;

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

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 ;

A22: integral+ (M,(max- f)) < +infty by A20;

|.f.| = max+ |.f.| by A14, A15, FUNCT_1:2;

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; :: thesis: verum

end;

assume
|.f.| is_integrable_on M
; :: thesis: f is_integrable_on MA15: now :: thesis: for x being object st x in dom |.f.| holds

(max+ |.f.|) . x = |.f.| . x

(max+ |.f.|) . x = |.f.| . x

let x be object ; :: 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 EXTREAL1:14;

(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;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 EXTREAL1:14;

(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

now :: thesis: for x being Element of X st x in dom (max- |.f.|) holds

(max- |.f.|) . x = 0

then A18:
integral+ (M,(max- |.f.|)) = 0
by A1, A12, A11, Th87, MESFUNC2:26;(max- |.f.|) . x = 0

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:19; :: thesis: verum

end;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:19; :: thesis: verum

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 ;

A22: integral+ (M,(max- f)) < +infty by A20;

|.f.| = max+ |.f.| by A14, A15, FUNCT_1:2;

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; :: thesis: verum

then Integral (M,|.f.|) < +infty by Th96;

then A23: integral+ (M,((max+ f) + (max- f))) < +infty by A12, A11, A5, A3, Th88, SUPINF_2:52;

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, Th79;

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, Th79;

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; :: thesis: verum