Description: A function has at most one value for each argument. (Contributed by NM, 24-May-1998) (Proof shortened by SN, 19-Dec-2024)