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