let f be Function; :: thesis: ( ( for x being set st x in dom f holds
f is_one-to-one_at x ) iff f is one-to-one )
thus ( ( for x being set st x in dom f holds
f is_one-to-one_at x ) implies f is one-to-one ) :: thesis: ( f is one-to-one implies for x being set st x in dom f holds
f is_one-to-one_at x )

proof

assume A1: for x being set st x in dom f holds
f is_one-to-one_at x ; :: thesis: f is one-to-one
let x1 be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not x1 in proj1 f or not b₁ in proj1 f or not f . x1 = f . b₁ or x1 = b₁ )
let x2 be set ; :: thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )
assume that
A2: x1 in dom f and
A3: ( x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
f is_one-to-one_at x1 by A1, A2;
hence x1 = x2 by A3, Th4; :: thesis: verum

end;

assume A4: f is one-to-one ; :: thesis: for x being set st x in dom f holds
f is_one-to-one_at x
let x be set ; :: thesis: ( x in dom f implies f is_one-to-one_at x )
assume A5: x in dom f ; :: thesis: f is_one-to-one_at x
then for z being set st z in dom f & x <> z holds
f . x <> f . z by A4, FUNCT_1:def 8;
hence f is_one-to-one_at x by A5, Th4; :: thesis: verum