theorem :: MESFUN13:22

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for f being b₄ -measurable PartFunc of X,ExtREAL st dom f = E holds
( f is_a.e.finite M iff M . ((eq_dom (f,+infty)) \/ (eq_dom (f,-infty))) = 0 )