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
f . x <= a ) holds
Integral M,(f | E) <= (R_EAL a) * (M . 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
f . x <= a ) holds
Integral M,(f | E) <= (R_EAL a) * (M . 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
f . x <= a ) holds
Integral M,(f | E) <= (R_EAL a) * (M . 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
f . x <= a ) holds
Integral M,(f | E) <= (R_EAL a) * (M . 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
f . x <= a ) holds
Integral M,(f | E) <= (R_EAL a) * (M . 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
f . x <= a ) implies Integral M,(f | E) <= (R_EAL a) * (M . 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 f . x <= a ) or Integral M,(f | E) <= (R_EAL a) * (M . 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 f . x <= a ) or Integral M,(f | E) <= (R_EAL a) * (M . E) ) by LMMarkov3; :: thesis: verum