let f be Function; :: thesis: ( f is one-to-one iff for x1, x2, y being set st [x1,y] in f & [x2,y] in f holds
x1 = x2 )
thus ( f is one-to-one implies for x1, x2, y being set st [x1,y] in f & [x2,y] in f holds
x1 = x2 ) :: thesis: ( ( for x1, x2, y being set st [x1,y] in f & [x2,y] in f holds
x1 = x2 ) implies f is one-to-one )

proof

assume A1: f is one-to-one ; :: thesis: for x1, x2, y being set st [x1,y] in f & [x2,y] in f holds
x1 = x2
let x1, x2, y be set ; :: thesis: ( [x1,y] in f & [x2,y] in f implies x1 = x2 )
assume ( [x1,y] in f & [x2,y] in f ) ; :: thesis: x1 = x2
then ( x1 in dom f & x2 in dom f & f . x1 = y & f . x2 = y ) by FUNCT_1:8;
hence x1 = x2 by A1, FUNCT_1:def 8; :: thesis: verum

end;

assume A2: for x1, x2, y being set st [x1,y] in f & [x2,y] in f holds
x1 = x2 ; :: 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 dom f or not b₁ in dom f or not f . x1 = f . b₁ or x1 = b₁ )
let x2 be set ; :: thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
assume ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
then ( [x1,(f . x1)] in f & [x2,(f . x1)] in f ) by FUNCT_1:8;
hence x1 = x2 by A2; :: thesis: verum