for f, g being Function st g * f is one-to-one & rng f c= dom g holds
f is one-to-one