FWIW, Barr and Wells in a well respected reference on category theory
[1] use a different definition of a function than the one in this
book. Essentially they avoid insisting on the concrete model of a
function as a set of ordered pairs (which they call its graph), and
would regard two functions having identical graphs as being
nevertheless distinct if they have different co-domains (section
1.2). IMO their definition is better thought out and ultimately less
troublesome when it comes to reasoning about functions. The definition
of a function is always the first thing I check in any book about math
for a rough assessment of whether reading the rest of it might make me
dumber or smarter.