for f being Function st ex g being Function st g * f = id (dom f) holds
f is one-to-one