theorem :: PARTFUN1:17

for x being object
for Y being set
for f being PartFunc of {x},Y holds f is one-to-one