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_measurable_on A ) & dom f = dom g & g is_integrable_on M & ( for x being Element of X st x in dom f holds
abs (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_measurable_on A ) & dom f = dom g & g is_integrable_on M & ( for x being Element of X st x in dom f holds
abs (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_measurable_on A ) & dom f = dom g & g is_integrable_on M & ( for x being Element of X st x in dom f holds
abs (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_measurable_on A ) & dom f = dom g & g is_integrable_on M & ( for x being Element of X st x in dom f holds
abs (f . x) <= g . x ) implies ( f is_integrable_on M & Integral M,(abs f) <= Integral M,g ) )
assume A1: ( ex A being Element of S st
( A = dom f & f is_measurable_on A ) & dom f = dom g & g is_integrable_on M & ( for x being Element of X st x in dom f holds
abs (f . x) <= g . x ) ) ; :: thesis: ( f is_integrable_on M & Integral M,(abs f) <= Integral M,g )
then consider A being Element of S such that
A2: ( A = dom f & f is_measurable_on A ) ;
A3: ( A = dom (R_EAL f) & R_EAL f is_measurable_on A ) by A2, Def6;
A4: ( dom (R_EAL f) = dom (R_EAL g) & R_EAL g is_integrable_on M ) by A1, Def9;

now

let x be Element of X; :: thesis: ( x in dom (R_EAL f) implies |.((R_EAL f) . x).| <= (R_EAL g) . x )
assume A5: x in dom (R_EAL f) ; :: thesis: |.((R_EAL f) . x).| <= (R_EAL g) . x
( abs (f . x) = |.((R_EAL f) . x).| & g . x = (R_EAL g) . x ) by EXTREAL2:49;
hence |.((R_EAL f) . x).| <= (R_EAL g) . x by A1, A5; :: thesis: verum

end;

then ( R_EAL f is_integrable_on M & Integral M,|.(R_EAL f).| <= Integral M,(R_EAL g) ) by A3, A4, MESFUNC5:108;
hence ( f is_integrable_on M & Integral M,(abs f) <= Integral M,g ) by Def9, Th1; :: thesis: verum