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 E being Element of S st
( E = dom f & E = dom g & f is_measurable_on E & g is_measurable_on E ) & f is nonnegative & g is nonnegative & ( for x being Element of X st x in dom g holds
g . x <= f . x ) holds
Integral M,g <= Integral M,f
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st ex E being Element of S st
( E = dom f & E = dom g & f is_measurable_on E & g is_measurable_on E ) & f is nonnegative & g is nonnegative & ( for x being Element of X st x in dom g holds
g . x <= f . x ) holds
Integral M,g <= Integral M,f
let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,REAL st ex E being Element of S st
( E = dom f & E = dom g & f is_measurable_on E & g is_measurable_on E ) & f is nonnegative & g is nonnegative & ( for x being Element of X st x in dom g holds
g . x <= f . x ) holds
Integral M,g <= Integral M,f
let f, g be PartFunc of X,REAL ; :: thesis: ( ex E being Element of S st
( E = dom f & E = dom g & f is_measurable_on E & g is_measurable_on E ) & f is nonnegative & g is nonnegative & ( for x being Element of X st x in dom g holds
g . x <= f . x ) implies Integral M,g <= Integral M,f )
assume that
A1: ex A being Element of S st
( A = dom f & A = dom g & f is_measurable_on A & g is_measurable_on A ) and
A2: ( f is nonnegative & g is nonnegative ) and
A3: for x being Element of X st x in dom g holds
g . x <= f . x ; :: thesis: Integral M,g <= Integral M,f
consider A being Element of S such that
A4: ( A = dom f & A = dom g & f is_measurable_on A & g is_measurable_on A ) by A1;
A5: ( A = dom (R_EAL f) & A = dom (R_EAL g) & R_EAL f is_measurable_on A & R_EAL g is_measurable_on A ) by A4, MESFUNC6:def 6;
( Integral M,g = integral+ M,(R_EAL g) & Integral M,f = integral+ M,(R_EAL f) ) by A1, A2, MESFUNC6:82;
hence Integral M,g <= Integral M,f by A2, A3, A5, MESFUNC5:91; :: thesis: verum