for f being Function st [:f,f:] is one-to-one holds
f is one-to-one