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) = dom g

proof

thus dom (f * g) c= dom g :: according to XBOOLE_0:def 10 :: thesis: dom g c= dom (f * g)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (f * g) or x in dom g )
assume A5: x in dom (f * g) ; :: thesis: x in dom g
thus x in dom g by A5, FUNCT_1:21; :: thesis: verum

end;

thus dom g c= dom (f * g) :: thesis: verum

proof

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

end;

end;

for x1, x2 being set 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 set ; :: 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) by A7, FUNCT_1:22;
A11: (f * g) . x2 = f . (g . x2) by A8, FUNCT_1:22;
A12: g . x2 in rng g by A4, A8, FUNCT_1:12;
A13: f . (g . x1) = (f | (rng g)) . (g . x1) by A4, A7, FUNCT_1:12, FUNCT_1:72;
A14: f . (g . x2) = (f | (rng g)) . (g . x2) by A4, A8, FUNCT_1:12, FUNCT_1:72;
dom (f | (rng g)) = rng g by A3, RELAT_1:91;
then A15: g . x1 in dom (f | (rng g)) by A4, A7, FUNCT_1:12;
g . x2 in dom (f | (rng g)) by A3, A12, RELAT_1:91;
then g . x1 = g . x2 by A2, A9, A10, A11, A13, A14, A15, FUNCT_1:def 8;
hence x1 = x2 by A1, A4, A7, A8, FUNCT_1:def 8; :: thesis: verum

end;

hence f * g is one-to-one by FUNCT_1:def 8; :: thesis: verum