:: deftheorem Def1 defines Category-yielding INDEX_1:def 1 :
for IT being Function holds
( IT is Category-yielding iff for x being set st x in dom IT holds
IT . x is Category );