:: deftheorem defines Integral_on MESFUNC6:def 5 :
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,REAL
for B being Element of S holds Integral_on (M,B,f) = Integral (M,(f | B));