Description: The edge function of a simple graph is a function. (Contributed by Alexander van der Vekens, 18-Aug-2017) (Revised by AV, 13-Oct-2020)