let g, f be Function; :: thesis: ( g * f is one-to-one & rng f = dom g implies ( f is one-to-one & g is one-to-one ) )
assume that
A1: g * f is one-to-one and
A2: rng f = dom g ; :: thesis: ( f is one-to-one & g is one-to-one )
thus f is one-to-one by A1, A2, Th47; :: thesis: g is one-to-one
assume not g is one-to-one ; :: thesis: contradiction
then consider y1, y2 being set such that
A3: y1 in dom g and
A4: y2 in dom g and
A5: g . y1 = g . y2 and
A6: y1 <> y2 by Def8;
consider x1 being set such that
A7: x1 in dom f and
A8: f . x1 = y1 by A2, A3, Def5;
consider x2 being set such that
A9: x2 in dom f and
A10: f . x2 = y2 by A2, A4, Def5;
( dom (g * f) = dom f & (g * f) . x1 = g . (f . x1) & (g * f) . x2 = g . (f . x2) ) by A2, A7, A9, Th23, RELAT_1:46;
hence contradiction by A1, A5, A6, A7, A8, A9, A10, Def8; :: thesis: verum