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 & 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,(abs 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,REAL 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,(abs f)) <= Integral (M,g) )
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 & 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,(abs f)) <= Integral (M,g) )
let f, g be PartFunc of X,REAL; :: 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,(abs 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,(abs f)) <= Integral (M,g) )
A5: R_EAL g is_integrable_on M by A3;

A6: now :: thesis: for x being Element of X st x in dom (R_EAL f) holds
|.((R_EAL f) . x).| <= (R_EAL g) . x

let x be Element of X; :: thesis: ( x in dom (R_EAL f) implies |.((R_EAL f) . x).| <= (R_EAL g) . x )
A7: |.(f . x).| = |.((R_EAL f) . x).| by EXTREAL1:12;
assume x in dom (R_EAL f) ; :: thesis: |.((R_EAL f) . x).| <= (R_EAL g) . x
hence |.((R_EAL f) . x).| <= (R_EAL g) . x by A4, A7; :: thesis: verum

end;

consider A being Element of S such that
A8: A = dom f and
A9: f is A -measurable by A1;
R_EAL f is A -measurable by A9;
then ( R_EAL f is_integrable_on M & Integral (M,|.(R_EAL f).|) <= Integral (M,(R_EAL g)) ) by A2, A8, A5, A6, MESFUNC5:102;
hence ( f is_integrable_on M & Integral (M,(abs f)) <= Integral (M,g) ) by Th1; :: thesis: verum