let R be Relation; :: thesis: ( R is empty-yielding implies R is Function-like )
assume R is empty-yielding ; :: thesis: R is Function-like
then R is {{}} -valued ;
hence R is Function-like ; :: thesis: verum