theorem :: PARTFUN1:8

for X, Y being set
for f being PartFunc of X,Y st ( for x1, x2 being Element of X st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2 ) holds
f is one-to-one ;