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