theorem :: FUNCT_1:26

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