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 & rng h c= dom f ) and
A3: dom g = dom h and
A4: f * g = f * h ; :: thesis: g = h
for x being object st x in dom g holds
g . x = h . x

proof

let x be object ; :: thesis: ( x in dom g implies g . x = h . x )
assume A5: x in dom g ; :: thesis: g . x = h . x
then A6: ( g . x in rng g & h . x in rng h ) by A3, Def3;
( (f * g) . x = f . (g . x) & (f * h) . x = f . (h . x) ) by A3, A5, Th13;
hence g . x = h . x by A1, A2, A4, A6; :: thesis: verum

end;

hence g = h by A3, Th2; :: thesis: verum

end;

assume A7: 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 object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2

proof

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

proof

let x be object ; :: thesis: ( x in dom (f * g) implies (f * g) . x = (f * h) . x )
assume A22: x in dom (f * g) ; :: thesis: (f * g) . x = (f * h) . x
then A23: g . x = x1 by A11, A12, A16;
( (f * g) . x = f . (g . x) & (f * h) . x = f . (h . x) ) by A11, A17, A16, A21, A22, Th12;
hence (f * g) . x = (f * h) . x by A10, A11, A18, A16, A22, A23; :: thesis: verum

end;

hence x1 = x2 by A7, A11, A17, A14, A19, A15, A20, A16, A21, Th2; :: thesis: verum

end;

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