theorem Th102: :: MESFUNC5:102

for X being non empty set
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) )