theorem Th81: :: FUNCT_1:82

for X being set
for f being Function st f is one-to-one holds
f " (f .: X) c= X