theorem Th55: :: FUNCT_2:56

for X being set
for f being Function of X,X holds
( f is one-to-one iff for x1, x2 being object st x1 in X & x2 in X & f . x1 = f . x2 holds
x1 = x2 )