:: deftheorem defines Integral_on MESFUNC5:def 18 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for B being Element of S holds Integral_on (M,B,f) = Integral (M,(f | B));