Description: Alternate definition of function. (Contributed by NM, 29-Dec-1996) (Proof shortened by SN, 19-Dec-2024)