:: deftheorem Def4 defines one-to-one FUNCT_1:def 4 :
for f being Function holds
( f is one-to-one iff for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2 );