:: deftheorem Def6 defines Function-yielding FUNCOP_1:def 6 :
for IT being Function holds
( IT is Function-yielding iff for x being object st x in dom IT holds
IT . x is Function );