:: deftheorem Def6 defines Function-yielding_on_second INDEX_1:def 6 :
for A, B being set
for IT being ManySortedSet of A,B holds
( IT is Function-yielding_on_second iff IT `2 is Function-yielding );