:: deftheorem Def9 defines non-empty FUNCT_1:def 9 :
for F being Function holds
( F is non-empty iff for n being object st n in dom F holds
not F . n is empty );