Definition 1.5.8.  Let X be a set, A ⊆ X, B be a set, Y ⊆ B, f:X → Y be a function. We define:
Remarks.

This definition is a slight extension of $restriction that simultaneously extends the codomain to a superset B of Y.

It might seem tempting to remove the need for this definition by implicitly treating a function to Y as a function to a superset B of Y, without explicitly specifying B. However, this could lead to confusion as the resulting function may not be surjective even though the original function is.