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,REAL st ex A being Element of S st

( A = (dom f) /\ (dom g) & f is A -measurable & g is A -measurable ) & f is_integrable_on M & g is_integrable_on M & g - f is nonnegative holds

ex E being Element of S st

( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) )

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

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

( A = (dom f) /\ (dom g) & f is A -measurable & g is A -measurable ) & f is_integrable_on M & g is_integrable_on M & g - f is nonnegative holds

ex E being Element of S st

( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) )

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

( A = (dom f) /\ (dom g) & f is A -measurable & g is A -measurable ) & f is_integrable_on M & g is_integrable_on M & g - f is nonnegative holds

ex E being Element of S st

( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) )

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

( A = (dom f) /\ (dom g) & f is A -measurable & g is A -measurable ) & f is_integrable_on M & g is_integrable_on M & g - f is nonnegative implies ex E being Element of S st

( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) ) )

assume that

A1: ex A being Element of S st

( A = (dom f) /\ (dom g) & f is A -measurable & g is A -measurable ) and

A2: f is_integrable_on M and

A3: g is_integrable_on M and

A4: g - f is nonnegative ; :: thesis: ex E being Element of S st

( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) )

set h = (- 1) (#) f;

(- 1) (#) f is_integrable_on M by A2, MESFUNC6:102;

then consider E being Element of S such that

A5: E = (dom ((- 1) (#) f)) /\ (dom g) and

A6: Integral (M,(((- 1) (#) f) + g)) = (Integral (M,(((- 1) (#) f) | E))) + (Integral (M,(g | E))) by A3, MESFUNC6:101;

A7: f | E is_integrable_on M by A2, MESFUNC6:91;

then A8: Integral (M,(f | E)) < +infty by MESFUNC6:90;

-infty < Integral (M,(f | E)) by A7, MESFUNC6:90;

then reconsider c1 = Integral (M,(f | E)) as Element of REAL by A8, XXREAL_0:14;

A9: (- 1) * (Integral (M,(f | E))) = (- 1) * c1 by EXTREAL1:1;

A10: g | E is_integrable_on M by A3, MESFUNC6:91;

then A11: Integral (M,(g | E)) < +infty by MESFUNC6:90;

-infty < Integral (M,(g | E)) by A10, MESFUNC6:90;

then reconsider c2 = Integral (M,(g | E)) as Element of REAL by A11, XXREAL_0:14;

take E ; :: thesis: ( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) )

A12: ((- 1) (#) f) | E = (- 1) (#) (f | E) by Th41;

consider A being Element of S such that

A13: A = (dom f) /\ (dom g) and

A14: f is A -measurable and

A15: g is A -measurable by A1;

dom ((- 1) (#) f) = dom f by VALUED_1:def 5;

then A16: dom (((- 1) (#) f) + g) = A by A13, VALUED_1:def 1;

(- 1) (#) f is A -measurable by A13, A14, MESFUNC6:21, XBOOLE_1:17;

then 0 <= (Integral (M,(((- 1) (#) f) | E))) + (Integral (M,(g | E))) by A4, A6, A15, A16, MESFUNC6:26, MESFUNC6:84;

then 0 <= ((- 1) * (Integral (M,(f | E)))) + (Integral (M,(g | E))) by A7, A12, MESFUNC6:102;

then 0 <= (- c1) + c2 by A9, SUPINF_2:1;

then 0 + c1 <= ((- c1) + c2) + c1 by XREAL_1:6;

hence ( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) ) by A5, VALUED_1:def 5; :: thesis: verum

for M being sigma_Measure of S

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

( A = (dom f) /\ (dom g) & f is A -measurable & g is A -measurable ) & f is_integrable_on M & g is_integrable_on M & g - f is nonnegative holds

ex E being Element of S st

( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) )

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

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

( A = (dom f) /\ (dom g) & f is A -measurable & g is A -measurable ) & f is_integrable_on M & g is_integrable_on M & g - f is nonnegative holds

ex E being Element of S st

( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) )

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

( A = (dom f) /\ (dom g) & f is A -measurable & g is A -measurable ) & f is_integrable_on M & g is_integrable_on M & g - f is nonnegative holds

ex E being Element of S st

( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) )

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

( A = (dom f) /\ (dom g) & f is A -measurable & g is A -measurable ) & f is_integrable_on M & g is_integrable_on M & g - f is nonnegative implies ex E being Element of S st

( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) ) )

assume that

A1: ex A being Element of S st

( A = (dom f) /\ (dom g) & f is A -measurable & g is A -measurable ) and

A2: f is_integrable_on M and

A3: g is_integrable_on M and

A4: g - f is nonnegative ; :: thesis: ex E being Element of S st

( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) )

set h = (- 1) (#) f;

(- 1) (#) f is_integrable_on M by A2, MESFUNC6:102;

then consider E being Element of S such that

A5: E = (dom ((- 1) (#) f)) /\ (dom g) and

A6: Integral (M,(((- 1) (#) f) + g)) = (Integral (M,(((- 1) (#) f) | E))) + (Integral (M,(g | E))) by A3, MESFUNC6:101;

A7: f | E is_integrable_on M by A2, MESFUNC6:91;

then A8: Integral (M,(f | E)) < +infty by MESFUNC6:90;

-infty < Integral (M,(f | E)) by A7, MESFUNC6:90;

then reconsider c1 = Integral (M,(f | E)) as Element of REAL by A8, XXREAL_0:14;

A9: (- 1) * (Integral (M,(f | E))) = (- 1) * c1 by EXTREAL1:1;

A10: g | E is_integrable_on M by A3, MESFUNC6:91;

then A11: Integral (M,(g | E)) < +infty by MESFUNC6:90;

-infty < Integral (M,(g | E)) by A10, MESFUNC6:90;

then reconsider c2 = Integral (M,(g | E)) as Element of REAL by A11, XXREAL_0:14;

take E ; :: thesis: ( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) )

A12: ((- 1) (#) f) | E = (- 1) (#) (f | E) by Th41;

consider A being Element of S such that

A13: A = (dom f) /\ (dom g) and

A14: f is A -measurable and

A15: g is A -measurable by A1;

dom ((- 1) (#) f) = dom f by VALUED_1:def 5;

then A16: dom (((- 1) (#) f) + g) = A by A13, VALUED_1:def 1;

(- 1) (#) f is A -measurable by A13, A14, MESFUNC6:21, XBOOLE_1:17;

then 0 <= (Integral (M,(((- 1) (#) f) | E))) + (Integral (M,(g | E))) by A4, A6, A15, A16, MESFUNC6:26, MESFUNC6:84;

then 0 <= ((- 1) * (Integral (M,(f | E)))) + (Integral (M,(g | E))) by A7, A12, MESFUNC6:102;

then 0 <= (- c1) + c2 by A9, SUPINF_2:1;

then 0 + c1 <= ((- c1) + c2) + c1 by XREAL_1:6;

hence ( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) ) by A5, VALUED_1:def 5; :: thesis: verum