let f be Function; :: thesis: ( ex g being Function st g * f = id (dom f) implies f is one-to-one )
given g being Function such that A1: g * f = id (dom f) ; :: thesis: f is one-to-one
dom (g * f) = dom f by A1, RELAT_1:45;
then rng f c= dom g by Th27;
hence f is one-to-one by A1, Th47; :: thesis: verum