:: deftheorem defines is_a.e.finite MESFUN13:def 2 :
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
( f is_a.e.finite M iff ex A being Element of S st
( M . A = 0 & A c= dom f & f | (A `) is PartFunc of X,REAL ) );