let f be Function; :: thesis: for x being object holds
( f is_one-to-one_at x iff ( x in dom f & ( for z being object st z in dom f & x <> z holds
f . x <> f . z ) ) )
let x be object ; :: thesis: ( f is_one-to-one_at x iff ( x in dom f & ( for z being object st z in dom f & x <> z holds
f . x <> f . z ) ) )
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: ( x in dom f & ( for z being object st z in dom f & x <> z holds
f . x <> f . z ) implies f is_one-to-one_at x )

proof

assume A1: f is_one-to-one_at x ; :: thesis: ( x in dom f & ( for z being object st z in dom f & x <> z holds
f . x <> f . z ) )
hence x in dom f by Th1; :: thesis: for z being object st z in dom f & x <> z holds
f . x <> f . z
let z be object ; :: thesis: ( z in dom f & x <> z implies f . x <> f . z )
assume that
A2: z in dom f and
A3: x <> z and
A4: f . x = f . z ; :: thesis: contradiction
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: verum

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: contradiction
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;

now :: thesis: contradiction

per cases ( ( y in f " {(f . x)} & not y in {x} ) or ( not y in f " {(f . x)} & y in {x} ) ) by A8;

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

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: verum

end;

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

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

end;

end;

end;

hence contradiction ; :: thesis: verum