:: deftheorem Def8 defines empty-yielding FUNCT_1:def 8 :
for f being Function holds
( f is empty-yielding iff for x being object st x in dom f holds
f . x is empty );