let f, g be Function; :: thesis: ( g * f is one-to-one & rng f c= dom g implies f is one-to-one )
assume that
A1: g * f is one-to-one and
A2: rng f c= dom g ; :: thesis: f is one-to-one

now :: thesis: for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that
A3: ( x1 in dom f & x2 in dom f ) and
A4: f . x1 = f . x2 ; :: thesis: x1 = x2
A5: ( x1 in dom (g * f) & x2 in dom (g * f) ) by A2, A3, RELAT_1:27;
( (g * f) . x1 = g . (f . x1) & (g * f) . x2 = g . (f . x2) ) by A3, Th13;
hence x1 = x2 by A1, A4, A5; :: thesis: verum

end;

hence f is one-to-one ; :: thesis: verum