let f, g 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 )
A3: dom (g * f) = dom f by A2, RELAT_1:27;
thus f is one-to-one by A1, A2, Th25; :: thesis: g is one-to-one
assume not g is one-to-one ; :: thesis: contradiction
then consider y1, y2 being object such that
A4: y1 in dom g and
A5: y2 in dom g and
A6: ( g . y1 = g . y2 & y1 <> y2 ) ;
consider x2 being object such that
A7: x2 in dom f and
A8: f . x2 = y2 by A2, A5, Def3;
A9: (g * f) . x2 = g . (f . x2) by A7, Th13;
consider x1 being object such that
A10: x1 in dom f and
A11: f . x1 = y1 by A2, A4, Def3;
(g * f) . x1 = g . (f . x1) by A10, Th13;
hence contradiction by A1, A6, A10, A11, A7, A8, A3, A9; :: thesis: verum