:: deftheorem Def4 defines finite-yielding FINSET_1:def 4 :
for f being Function holds
( f is finite-yielding iff for i being object st i in dom f holds
f . i is finite );