let f be set ; :: thesis: ( f is empty implies f is Function-like )
assume f is empty ; :: thesis: f is Function-like
hence for x, y1, y2 being set st [x,y1] in f & [x,y2] in f holds
y1 = y2 ; :: according to FUNCT_1:def 1 :: thesis: verum