:: deftheorem defines "1-1" MSUALG_3:def 2 :
for IT being Function holds
( IT is "1-1" iff for i being set
for f being Function st i in dom IT & IT . i = f holds
f is one-to-one );