:: deftheorem defines not-one-to-one CARDFIN2:def 4 :
for s, t being set holds not-one-to-one (s,t) = { f where f is Function of s,t : not f is one-to-one } ;