theorem Th30: :: MESFUNC5:30

for X being non empty set
for f being PartFunc of X,ExtREAL
for a being R_eal holds eq_dom (f,a) = f " {a}