let f be Function; :: thesis:
let x be object ; :: thesis:
thus ( f is_one-to-one_at x implies ( x in dom f & ( for z being object st z in dom f & x <> z holds
f . x <> f . z ) ) ) :: thesis:

assume A1: f is_one-to-one_at x ; :: thesis:
hence x in dom f by Th1; :: thesis:
let z be object ; :: thesis:
assume that
A2: z in dom f and
A3: x <> z and
A4: f . x = f . z ; :: thesis:
f . x in {(f . x)} by TARSKI:def 1;
then z in f " {(f . x)} by A2, A4, FUNCT_1:def 7;
then z in {x} by A1, Th2;
hence contradiction by A3, TARSKI:def 1; :: thesis:

end;

assume that
A5: x in dom f and
A6: for z being object st z in dom f & x <> z holds
f . x <> f . z and
A7: not f is_one-to-one_at x ; :: thesis:
f " {(f . x)} <> {x} by A5, A7, Th2;
then consider y being object such that
A8: ( ( y in f " {(f . x)} & not y in {x} ) or ( y in {x} & not y in f " {(f . x)} ) ) by TARSKI:2;
f . x in {(f . x)} by TARSKI:def 1;
then A9: x in f " {(f . x)} by A5, FUNCT_1:def 7;

per cases by A8;

suppose A10: ( y in f " {(f . x)} & not y in {x} ) ; :: thesis:

then f . y in {(f . x)} by FUNCT_1:def 7;
then A11: f . y = f . x by TARSKI:def 1;
( y in dom f & x <> y ) by A10, FUNCT_1:def 7, TARSKI:def 1;
hence contradiction by A6, A11; :: thesis:

end;

suppose ( not y in f " {(f . x)} & y in {x} ) ; :: thesis:

hence contradiction by A9, TARSKI:def 1; :: thesis:

end;

end;

end;

hence contradiction ; :: thesis: