let f, g be Function; ( 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
; 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)
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 ;
( 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
;
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;
verum
end;
hence
f * g is one-to-one
; verum