let f be Function; :: thesis: ( f is one-to-one iff for x being set st x in dom f holds
f " {(f . x)} = {x} )

now :: thesis: ( ( ( for x being object st x in dom f holds
f is_one-to-one_at x ) implies for x being object st x in dom f holds
f " {(f . x)} = {x} ) & ( ( for x being object st x in dom f holds
f " {(f . x)} = {x} ) implies for x being object st x in dom f holds
f is_one-to-one_at x ) )

hereby :: thesis: ( ( for x being object st x in dom f holds
f " {(f . x)} = {x} ) implies for x being object st x in dom f holds
f is_one-to-one_at x )

assume A1: for x being object st x in dom f holds
f is_one-to-one_at x ; :: thesis: for x being object st x in dom f holds
f " {(f . x)} = {x}
let x be object ; :: thesis: ( x in dom f implies f " {(f . x)} = {x} )
assume x in dom f ; :: thesis: f " {(f . x)} = {x}
then f is_one-to-one_at x by A1;
hence f " {(f . x)} = {x} by FINSEQ_4:2; :: thesis: verum

end;

assume A2: for x being object st x in dom f holds
f " {(f . x)} = {x} ; :: thesis: for x being object st x in dom f holds
f is_one-to-one_at x
let x be object ; :: thesis: ( x in dom f implies f is_one-to-one_at x )
assume A3: x in dom f ; :: thesis: f is_one-to-one_at x
then f " {(f . x)} = {x} by A2;
hence f is_one-to-one_at x by A3, FINSEQ_4:2; :: thesis: verum

end;

hence ( f is one-to-one iff for x being set st x in dom f holds
f " {(f . x)} = {x} ) by FINSEQ_4:4; :: thesis: verum