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