theorem :: MESFUNC6:68

for X being non empty set
for f being PartFunc of X,REAL
for r being Real holds eq_dom (f,r) = f " {r}