theorem :: FUNCT_1:52

for X being set
for f being Function st f is one-to-one holds
f | X is one-to-one