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;
then rng f c= dom g by Th15;
hence f is one-to-one by A1, Th25; :: thesis: verum