Description: Our definition of the function predicate df-funALTV (based on a more general, converse reflexive, relation) and the original definition of function in set.mm df-fun , are always the same and interchangeable. (Contributed by Peter Mazsa, 27-Jul-2021)