theorem :: MESFUNC6:90

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 st f is_integrable_on M holds
( -infty < Integral (M,f) & Integral (M,f) < +infty ) by MESFUNC5:96;