:: deftheorem Def15 defines eq_dom MESFUNC1:def 14 :
for f being ext-real-valued Function
for a being ExtReal
for b₃ being set holds
( b₃ = eq_dom (f,a) iff for x being set holds
( x in b₃ iff ( x in dom f & f . x = a ) ) );