Definition 1.5.6.  Let S, T be sets,  be a mapping from S to T. We define:
Remarks.

This definition shows that mappings and functions, as defined in this library, are interchangeable. (The other direction is straightforward as well.)