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