let f, g be Function; ( 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
; ( 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; g is one-to-one
assume
not g is one-to-one
; 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; verum