:: deftheorem Def2 defines Function-yielding YELLOW14:def 2 :
for R being 1-sorted
for N being NetStr over R holds
( N is Function-yielding iff the mapping of N is Function-yielding );