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 that
A1: ex A being Element of S st
( A = dom f & f is_measurable_on A ) 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
abs (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, Def9;

A6: now

let x be Element of X; :: thesis: ( x in dom (R_EAL f) implies |.((R_EAL f) . x).| <= (R_EAL g) . x )
A7: abs (f . x) = |.((R_EAL f) . x).| by EXTREAL2:49;
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_measurable_on A by A1;
R_EAL f is_measurable_on A by A9, Def6;
then ( R_EAL f is_integrable_on M & Integral M,|.(R_EAL f).| <= Integral M,(R_EAL g) ) by A2, A8, A5, A6, MESFUNC5:108;
hence ( f is_integrable_on M & Integral M,(abs f) <= Integral M,g ) by Def9, Th1; :: thesis: verum