:: deftheorem defines finite-yielding FINSET_1:def 5 :
for I being set
for IT being b₁ -defined Function holds
( IT is finite-yielding iff for i being object st i in I holds
IT . i is finite );