let f be Function; :: thesis: ( f is one-to-one iff for g, h being Function st rng g c= dom f & rng h c= dom f & dom g = dom h & f * g = f * h holds
g = h )
thus ( f is one-to-one implies for g, h being Function st rng g c= dom f & rng h c= dom f & dom g = dom h & f * g = f * h holds
g = h ) :: thesis: ( ( for g, h being Function st rng g c= dom f & rng h c= dom f & dom g = dom h & f * g = f * h holds
g = h ) implies f is one-to-one )

proof

assume A1: f is one-to-one ; :: thesis: for g, h being Function st rng g c= dom f & rng h c= dom f & dom g = dom h & f * g = f * h holds
g = h
let g, h be Function; :: thesis: ( rng g c= dom f & rng h c= dom f & dom g = dom h & f * g = f * h implies g = h )
assume that
A2: rng g c= dom f and
A3: rng h c= dom f and
A4: dom g = dom h and
A5: f * g = f * h ; :: thesis: g = h
for x being set st x in dom g holds
g . x = h . x

proof

let x be set ; :: thesis: ( x in dom g implies g . x = h . x )
assume x in dom g ; :: thesis: g . x = h . x
then ( (f * g) . x = f . (g . x) & (f * h) . x = f . (h . x) & g . x in rng g & h . x in rng h & ( g . x in rng g implies g . x in dom f ) & ( h . x in rng h implies h . x in dom f ) ) by A2, A3, A4, Def5, Th23;
hence g . x = h . x by A1, A5, Def8; :: thesis: verum

end;

hence g = h by A4, Th9; :: thesis: verum

end;

assume A6: for g, h being Function st rng g c= dom f & rng h c= dom f & dom g = dom h & f * g = f * h holds
g = h ; :: thesis: f is one-to-one
for x1, x2 being set st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2

proof

let x1, x2 be set ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that
A7: ( x1 in dom f & x2 in dom f ) and
A8: f . x1 = f . x2 ; :: thesis: x1 = x2
deffunc H₁( set ) -> set = x1;
consider g being Function such that
A9: dom g = {{} } and
A10: for x being set st x in {{} } holds
g . x = H₁(x) from FUNCT_1:sch 3();
deffunc H₂( set ) -> set = x2;
consider h being Function such that
A11: dom h = {{} } and
A12: for x being set st x in {{} } holds
h . x = H₂(x) from FUNCT_1:sch 3();
{} in {{} } by TARSKI:def 1;
then A13: ( g . {} = x1 & h . {} = x2 ) by A10, A12;
then ( rng g = {x1} & rng h = {x2} ) by A9, A11, Th14;
then A14: ( rng g c= dom f & rng h c= dom f ) by A7, ZFMISC_1:37;
then A15: ( dom (f * g) = dom g & dom (f * h) = dom h ) by RELAT_1:46;
for x being set st x in dom (f * g) holds
(f * g) . x = (f * h) . x

proof

let x be set ; :: thesis: ( x in dom (f * g) implies (f * g) . x = (f * h) . x )
assume x in dom (f * g) ; :: thesis: (f * g) . x = (f * h) . x
then ( (f * g) . x = f . (g . x) & (f * h) . x = f . (h . x) & g . x = x1 & h . x = x2 ) by A9, A10, A11, A12, A15, Th22;
hence (f * g) . x = (f * h) . x by A8; :: thesis: verum

end;

hence x1 = x2 by A6, A13, A14, A9, A11, A15, Th9; :: thesis: verum

end;

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