let x be object ; FUNCT_1:def 1 for y1, y2 being object st [x,y1] in f | X & [x,y2] in f | X holds
y1 = y2
let y1, y2 be object ; ( [x,y1] in f | X & [x,y2] in f | X implies y1 = y2 )
assume
( [x,y1] in f | X & [x,y2] in f | X )
; y1 = y2
then
( [x,y1] in f & [x,y2] in f )
by RELAT_1:def 11;
hence
y1 = y2
by Def1; verum