let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for E being Element of S
for a being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds
a <= f . x ) holds
(R_EAL a) * (M . E) <= Integral M,(f | E)
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL
for E being Element of S
for a being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds
a <= f . x ) holds
(R_EAL a) * (M . E) <= Integral M,(f | E)
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,REAL
for E being Element of S
for a being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds
a <= f . x ) holds
(R_EAL a) * (M . E) <= Integral M,(f | E)
let f be PartFunc of X,REAL ; :: thesis: for E being Element of S
for a being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds
a <= f . x ) holds
(R_EAL a) * (M . E) <= Integral M,(f | E)
let E be Element of S; :: thesis: for a being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds
a <= f . x ) holds
(R_EAL a) * (M . E) <= Integral M,(f | E)
let a be Real; :: thesis: ( f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds
a <= f . x ) implies (R_EAL a) * (M . E) <= Integral M,(f | E) )
assume f is_integrable_on M ; :: thesis: ( not E c= dom f or not M . E < +infty or ex x being Element of X st
( x in E & not a <= f . x ) or (R_EAL a) * (M . E) <= Integral M,(f | E) )
then R_EAL f is_integrable_on M by MESFUNC6:def 9;
hence ( not E c= dom f or not M . E < +infty or ex x being Element of X st
( x in E & not a <= f . x ) or (R_EAL a) * (M . E) <= Integral M,(f | E) ) by Th1; :: thesis: verum