:: deftheorem Def6 defines -one-to-one FOMODEL0:def 6 :
for X being set
for f being Function holds
( f is X -one-to-one iff for x, y being set st x in X /\ (dom f) & y in X /\ (dom f) & f . x = f . y holds
x = y );