for X being set
for f being PartFunc of X,ExtREAL holds great_eq_dom (f,+infty) = eq_dom (f,+infty)