:: deftheorem defines nonpair-yielding FACIRC_1:def 3 :
for IT being Function holds
( IT is nonpair-yielding iff for x being set st x in dom IT holds
not IT . x is pair );