let f be Function; :: thesis: for x being set holds
( f is_one-to-one_at x iff ( x in dom f & ( for z being set st z in dom f & x <> z holds
f . x <> f . z ) ) )
let x be set ; :: thesis: ( f is_one-to-one_at x iff ( x in dom f & ( for z being set 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 set st z in dom f & x <> z holds
f . x <> f . z ) ) ) :: thesis: ( x in dom f & ( for z being set 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 set st z in dom f & x <> z holds
f . x <> f . z ) )
hence x in dom f by Th2; :: thesis: for z being set st z in dom f & x <> z holds
f . x <> f . z
let z be set ; :: 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 13;
then z in {x} by A1, Th3;
hence contradiction by A3, TARSKI:def 1; :: thesis: verum

end;

assume that
A5: x in dom f and
A6: for z being set 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, Th3;
then consider y being set 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 13;

now

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 13;
then A11: f . y = f . x by TARSKI:def 1;
( y in dom f & x <> y ) by A10, FUNCT_1:def 13, 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