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

for M being sigma_Measure of S

for f, g being PartFunc of X,ExtREAL st ex A being Element of S st

( A = dom f & f is A -measurable ) & dom f = dom g & g is_integrable_on M & ( for x being Element of X st x in dom f holds

|.(f . x).| <= g . x ) holds

( f is_integrable_on M & Integral (M,|.f.|) <= Integral (M,g) )

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

for f, g being PartFunc of X,ExtREAL st ex A being Element of S st

( A = dom f & f is A -measurable ) & dom f = dom g & g is_integrable_on M & ( for x being Element of X st x in dom f holds

|.(f . x).| <= g . x ) holds

( f is_integrable_on M & Integral (M,|.f.|) <= Integral (M,g) )

let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,ExtREAL st ex A being Element of S st

( A = dom f & f is A -measurable ) & dom f = dom g & g is_integrable_on M & ( for x being Element of X st x in dom f holds

|.(f . x).| <= g . x ) holds

( f is_integrable_on M & Integral (M,|.f.|) <= Integral (M,g) )

let f, g be PartFunc of X,ExtREAL; :: thesis: ( ex A being Element of S st

( A = dom f & f is A -measurable ) & dom f = dom g & g is_integrable_on M & ( for x being Element of X st x in dom f holds

|.(f . x).| <= g . x ) implies ( f is_integrable_on M & Integral (M,|.f.|) <= Integral (M,g) ) )

assume that

A1: ex A being Element of S st

( A = dom f & f is A -measurable ) and

A2: dom f = dom g and

A3: g is_integrable_on M and

A4: for x being Element of X st x in dom f holds

|.(f . x).| <= g . x ; :: thesis: ( f is_integrable_on M & Integral (M,|.f.|) <= Integral (M,g) )

A5: ex AA being Element of S st

( AA = dom g & g is AA -measurable ) by A3;

A8: dom g = dom (max+ g) by MESFUNC2:def 2;

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

consider A being Element of S such that

A16: A = dom f and

A17: f is A -measurable by A1;

A18: |.f.| is A -measurable by A16, A17, MESFUNC2:27;

A19: A = dom |.f.| by A16, MESFUNC1:def 10;

A20: for x being Element of X st x in dom |.f.| holds

|.f.| . x <= g . x

then A23: integral+ (M,|.f.|) <= integral+ (M,g) by A2, A16, A5, A19, A18, A7, A20, Th85;

A24: dom |.f.| = dom (max- |.f.|) by MESFUNC2:def 3;

integral+ (M,(max+ g)) < +infty by A3;

then integral+ (M,(max+ |.f.|)) < +infty by A15, A10, A23, XXREAL_0:2;

then |.f.| is_integrable_on M by A19, A18, A25;

hence f is_integrable_on M by A1, Th100; :: thesis: Integral (M,|.f.|) <= Integral (M,g)

Integral (M,g) = integral+ (M,g) by A5, A6, Th88, SUPINF_2:52;

hence Integral (M,|.f.|) <= Integral (M,g) by A19, A18, A22, A23, Th88, SUPINF_2:52; :: thesis: verum

for M being sigma_Measure of S

for f, g being PartFunc of X,ExtREAL st ex A being Element of S st

( A = dom f & f is A -measurable ) & dom f = dom g & g is_integrable_on M & ( for x being Element of X st x in dom f holds

|.(f . x).| <= g . x ) holds

( f is_integrable_on M & Integral (M,|.f.|) <= Integral (M,g) )

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

for f, g being PartFunc of X,ExtREAL st ex A being Element of S st

( A = dom f & f is A -measurable ) & dom f = dom g & g is_integrable_on M & ( for x being Element of X st x in dom f holds

|.(f . x).| <= g . x ) holds

( f is_integrable_on M & Integral (M,|.f.|) <= Integral (M,g) )

let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,ExtREAL st ex A being Element of S st

( A = dom f & f is A -measurable ) & dom f = dom g & g is_integrable_on M & ( for x being Element of X st x in dom f holds

|.(f . x).| <= g . x ) holds

( f is_integrable_on M & Integral (M,|.f.|) <= Integral (M,g) )

let f, g be PartFunc of X,ExtREAL; :: thesis: ( ex A being Element of S st

( A = dom f & f is A -measurable ) & dom f = dom g & g is_integrable_on M & ( for x being Element of X st x in dom f holds

|.(f . x).| <= g . x ) implies ( f is_integrable_on M & Integral (M,|.f.|) <= Integral (M,g) ) )

assume that

A1: ex A being Element of S st

( A = dom f & f is A -measurable ) and

A2: dom f = dom g and

A3: g is_integrable_on M and

A4: for x being Element of X st x in dom f holds

|.(f . x).| <= g . x ; :: thesis: ( f is_integrable_on M & Integral (M,|.f.|) <= Integral (M,g) )

A5: ex AA being Element of S st

( AA = dom g & g is AA -measurable ) by A3;

A6: now :: thesis: for x being object st x in dom g holds

0 <= g . x

then A7:
g is nonnegative
by SUPINF_2:52;0 <= g . x

let x be object ; :: thesis: ( x in dom g implies 0 <= g . x )

assume x in dom g ; :: thesis: 0 <= g . x

then |.(f . x).| <= g . x by A2, A4;

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

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

then |.(f . x).| <= g . x by A2, A4;

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

A8: dom g = dom (max+ g) by MESFUNC2:def 2;

now :: thesis: for x being object st x in dom g holds

(max+ g) . x = g . x

then A10:
g = max+ g
by A8, FUNCT_1:2;(max+ g) . x = g . x

let x be object ; :: thesis: ( x in dom g implies (max+ g) . x = g . x )

A9: 0 <= g . x by A7, SUPINF_2:51;

assume x in dom g ; :: thesis: (max+ g) . x = g . x

hence (max+ g) . x = max ((g . x),0) by A8, MESFUNC2:def 2

.= g . x by A9, XXREAL_0:def 10 ;

:: thesis: verum

end;A9: 0 <= g . x by A7, SUPINF_2:51;

assume x in dom g ; :: thesis: (max+ g) . x = g . x

hence (max+ g) . x = max ((g . x),0) by A8, MESFUNC2:def 2

.= g . x by A9, XXREAL_0:def 10 ;

:: thesis: verum

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

A12: now :: thesis: for x being object st x in dom |.f.| holds

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

then A15:
|.f.| = max+ |.f.|
by A11, FUNCT_1:2;(max+ |.f.|) . x = |.f.| . x

let x be object ; :: thesis: ( x in dom |.f.| implies (max+ |.f.|) . x = |.f.| . x )

assume A13: x in dom |.f.| ; :: thesis: (max+ |.f.|) . x = |.f.| . x

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

then A14: 0 <= |.f.| . x by EXTREAL1:14;

thus (max+ |.f.|) . x = max ((|.f.| . x),0) by A11, A13, MESFUNC2:def 2

.= |.f.| . x by A14, XXREAL_0:def 10 ; :: thesis: verum

end;assume A13: x in dom |.f.| ; :: thesis: (max+ |.f.|) . x = |.f.| . x

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

then A14: 0 <= |.f.| . x by EXTREAL1:14;

thus (max+ |.f.|) . x = max ((|.f.| . x),0) by A11, A13, MESFUNC2:def 2

.= |.f.| . x by A14, XXREAL_0:def 10 ; :: thesis: verum

consider A being Element of S such that

A16: A = dom f and

A17: f is A -measurable by A1;

A18: |.f.| is A -measurable by A16, A17, MESFUNC2:27;

A19: A = dom |.f.| by A16, MESFUNC1:def 10;

A20: for x being Element of X st x in dom |.f.| holds

|.f.| . x <= g . x

proof

let x be Element of X; :: thesis: ( x in dom |.f.| implies |.f.| . x <= g . x )

assume A21: x in dom |.f.| ; :: thesis: |.f.| . x <= g . x

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

hence |.f.| . x <= g . x by A4, A16, A19, A21; :: thesis: verum

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

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

hence |.f.| . x <= g . x by A4, A16, A19, A21; :: thesis: verum

A22: now :: thesis: for x being object st x in dom |.f.| holds

0 <= |.f.| . x

then
|.f.| is nonnegative
by SUPINF_2:52;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

then A23: integral+ (M,|.f.|) <= integral+ (M,g) by A2, A16, A5, A19, A18, A7, A20, Th85;

A24: dom |.f.| = dom (max- |.f.|) by MESFUNC2:def 3;

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

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

then A25:
integral+ (M,(max- |.f.|)) = 0
by A19, A18, A24, 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 A24, A12;

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 A24, A12;

hence (max- |.f.|) . x = 0 by MESFUNC2:19; :: thesis: verum

integral+ (M,(max+ g)) < +infty by A3;

then integral+ (M,(max+ |.f.|)) < +infty by A15, A10, A23, XXREAL_0:2;

then |.f.| is_integrable_on M by A19, A18, A25;

hence f is_integrable_on M by A1, Th100; :: thesis: Integral (M,|.f.|) <= Integral (M,g)

Integral (M,g) = integral+ (M,g) by A5, A6, Th88, SUPINF_2:52;

hence Integral (M,|.f.|) <= Integral (M,g) by A19, A18, A22, A23, Th88, SUPINF_2:52; :: thesis: verum