theorem Th9: :: GRFUNC_1:9

for f being Function holds
( f is one-to-one iff for x1, x2, y being object st [x1,y] in f & [x2,y] in f holds
x1 = x2 )