:: deftheorem defines one-to-one WAYBEL_1:def 1 :
for L1, L2 being non empty 1-sorted
for f being Function of L1,L2 holds
( f is one-to-one iff for x, y being Element of L1 st f . x = f . y holds
x = y );