let f be Function; :: thesis: ( f is one-to-one iff for x1, x2, y being object st [x1,y] in f & [x2,y] in f holds
x1 = x2 )
thus ( f is one-to-one implies for x1, x2, y being object st [x1,y] in f & [x2,y] in f holds
x1 = x2 ) :: thesis: ( ( for x1, x2, y being object 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 object st [x1,y] in f & [x2,y] in f holds
x1 = x2
let x1, x2, y be object ; :: thesis: ( [x1,y] in f & [x2,y] in f implies x1 = x2 )
assume A2: ( [x1,y] in f & [x2,y] in f ) ; :: thesis: x1 = x2
then A3: ( f . x1 = y & f . x2 = y ) by FUNCT_1:1;
( x1 in dom f & x2 in dom f ) by A2, FUNCT_1:1;
hence x1 = x2 by A1, A3; :: thesis: verum

end;

assume A4: for x1, x2, y being object st [x1,y] in f & [x2,y] in f holds
x1 = x2 ; :: thesis: f is one-to-one
let x1 be object ; :: according to FUNCT_1:def 4 :: thesis: for b₁ being object holds
( not x1 in proj1 f or not b₁ in proj1 f or not f . x1 = f . b₁ or x1 = b₁ )
let x2 be object ; :: thesis: ( not x1 in proj1 f or not x2 in proj1 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:1;
hence x1 = x2 by A4; :: thesis: verum