reconsider E = {} as Relation ;
take E ; :: thesis: E is Function-like
( ( for p being set st p in E holds
ex x, y being set st [x,y] = p ) & ( 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