let x be set ; :: according to FUNCT_1:def 1 :: thesis: for y1, y2 being set st [x,y1] in f ~ & [x,y2] in f ~ holds
y1 = y2
let y1, y2 be set ; :: thesis: ( [x,y1] in f ~ & [x,y2] in f ~ implies y1 = y2 )
assume ( [x,y1] in f ~ & [x,y2] in f ~ ) ; :: thesis: y1 = y2
then A1: ( [y1,x] in f & [y2,x] in f ) by RELAT_1:def 7;
then A2: ( y1 in dom f & y2 in dom f ) by RELAT_1:def 4;
then ( x = f . y1 & x = f . y2 ) by A1, Def4;
hence y1 = y2 by A2, Def8; :: thesis: verum