let x be object ; FUNCT_1:def 1 for y1, y2 being object st [x,y1] in f ~ & [x,y2] in f ~ holds
y1 = y2
let y1, y2 be object ; ( [x,y1] in f ~ & [x,y2] in f ~ implies y1 = y2 )
assume that
A1:
[x,y1] in f ~
and
A2:
[x,y2] in f ~
; y1 = y2
A3:
[y2,x] in f
by A2, RELAT_1:def 7;
then A4:
y2 in dom f
by XTUPLE_0:def 12;
reconsider x = x as set by TARSKI:1;
A5:
x = f . y2
by A3, Def2, A4;
A6:
[y1,x] in f
by A1, RELAT_1:def 7;
then A7:
y1 in dom f
by XTUPLE_0:def 12;
then
x = f . y1
by A6, Def2;
hence
y1 = y2
by A7, A4, A5, Def4; verum