theorem Th9: :: MESFUN13:8
for X being non empty set
for S being SigmaField of X
for E being Element of S
for f being b3 -measurable PartFunc of X,ExtREAL st dom f = E holds
( eq_dom (f,+infty) in S & eq_dom (f,-infty) in S )