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_measurable_on A & g is_measurable_on A ) & 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_measurable_on A & g is_measurable_on A ) & 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_measurable_on A & g is_measurable_on A ) & 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_measurable_on A & g is_measurable_on A ) & 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_measurable_on A & g is_measurable_on A ) and
A2: ( f is_integrable_on M & g is_integrable_on M ) and
A3: 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 & Integral M,((- 1) (#) f) = (R_EAL (- 1)) * (Integral M,f) ) by A2, MESFUNC6:102;
then consider E being Element of S such that
A5: ( E = (dom ((- 1) (#) f)) /\ (dom g) & Integral M,(((- 1) (#) f) + g) = (Integral M,(((- 1) (#) f) | E)) + (Integral M,(g | E)) ) by A2, MESFUNC6:101;
consider A being Element of S such that
B1: ( A = (dom f) /\ (dom g) & f is_measurable_on A & g is_measurable_on A ) by A1;
B2: (- 1) (#) f is_measurable_on A by B1, MESFUNC6:21, XBOOLE_1:17;
dom ((- 1) (#) f) = dom f by VALUED_1:def 5;
then dom (((- 1) (#) f) + g) = A by B1, VALUED_1:def 1;
then A7: 0 <= (Integral M,(((- 1) (#) f) | E)) + (Integral M,(g | E)) by A5, A3, B2, B1, MESFUNC6:26, MESFUNC6:84;
A8: f | E is_integrable_on M by A2, MESFUNC6:91;
take E ; :: thesis: ( E = (dom f) /\ (dom g) & Integral M,(f | E) <= Integral M,(g | E) )
((- 1) (#) f) | E = (- 1) (#) (f | E) by MES72;
then A9: 0 <= ((R_EAL (- 1)) * (Integral M,(f | E))) + (Integral M,(g | E)) by A7, A8, MESFUNC6:102;
( -infty < Integral M,(f | E) & Integral M,(f | E) < +infty ) by A8, MESFUNC6:90;
then reconsider c1 = Integral M,(f | E) as Real by XXREAL_0:14;
g | E is_integrable_on M by A2, MESFUNC6:91;
then ( -infty < Integral M,(g | E) & Integral M,(g | E) < +infty ) by MESFUNC6:90;
then reconsider c2 = Integral M,(g | E) as Real by XXREAL_0:14;
(R_EAL (- 1)) * (Integral M,(f | E)) = (- 1) * c1 by EXTREAL1:13;
then 0 <= (- c1) + c2 by A9, SUPINF_2:1;
then 0 + c1 <= ((- c1) + c2) + c1 by XREAL_1:8;
hence ( E = (dom f) /\ (dom g) & Integral M,(f | E) <= Integral M,(g | E) ) by A5, VALUED_1:def 5; :: thesis: verum