theorem :: MESFUN13:3

for X being set
for f being PartFunc of X,ExtREAL holds less_eq_dom (f,-infty) = eq_dom (f,-infty)