theorem :: MESFUN13:5

for X being set
for f being PartFunc of X,ExtREAL holds dom f = ((eq_dom (f,-infty)) \/ ((great_dom (f,-infty)) /\ (less_dom (f,+infty)))) \/ (eq_dom (f,+infty))