:: deftheorem defines Integral MESFUNC6:def 3 :
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 holds Integral (M,f) = Integral (M,(R_EAL f));