reconsider E = {} as Relation ;
take E ; :: thesis: E is Function-like
for x, y1, y2 being set st [x,y1] in E & [x,y2] in E holds
y1 = y2 ;
hence E is Function-like by Def1; :: thesis: verum