let f, g be Function; :: thesis: ( g is one-to-one & f | (rng g) is one-to-one & rng g c= dom f implies f * g is one-to-one )
assume that
A1: g is one-to-one and
A2: f | (rng g) is one-to-one and
A3: rng g c= dom f ; :: thesis: f * g is one-to-one
set h = f * g;
A4: dom (f * g) c= dom g by FUNCT_1:11;
dom g c= dom (f * g)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom g or x in dom (f * g) )
assume A5: x in dom g ; :: thesis: x in dom (f * g)
g . x in rng g by A5, FUNCT_1:3;
hence x in dom (f * g) by A3, A5, FUNCT_1:11; :: thesis: verum

end;

then A6: dom (f * g) = dom g by A4;
for x1, x2 being object st x1 in dom (f * g) & x2 in dom (f * g) & (f * g) . x1 = (f * g) . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in dom (f * g) & x2 in dom (f * g) & (f * g) . x1 = (f * g) . x2 implies x1 = x2 )
assume that
A7: x1 in dom (f * g) and
A8: x2 in dom (f * g) and
A9: (f * g) . x1 = (f * g) . x2 ; :: thesis: x1 = x2
A10: ( (f * g) . x1 = f . (g . x1) & (f * g) . x2 = f . (g . x2) ) by A7, A8, FUNCT_1:12;
dom (f | (rng g)) = rng g by A3, RELAT_1:62;
then A11: g . x1 in dom (f | (rng g)) by A4, A7, FUNCT_1:3;
g . x2 in rng g by A4, A8, FUNCT_1:3;
then A12: g . x2 in dom (f | (rng g)) by A3, RELAT_1:62;
( f . (g . x1) = (f | (rng g)) . (g . x1) & f . (g . x2) = (f | (rng g)) . (g . x2) ) by A6, A7, A8, FUNCT_1:3, FUNCT_1:49;
then g . x1 = g . x2 by A2, A9, A10, A11, A12;
hence x1 = x2 by A1, A4, A7, A8; :: thesis: verum

end;

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