:: deftheorem Def1 defines Function-like FUNCT_1:def 1 :
for X being set holds
( X is Function-like iff for x, y1, y2 being object st [x,y1] in X & [x,y2] in X holds
y1 = y2 );