:: deftheorem Def14 defines integral' MESFUNC5:def 14 :
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 holds
( ( dom f <> {} implies integral' (M,f) = integral (M,f) ) & ( not dom f <> {} implies integral' (M,f) = 0. ) );