Description: Restriction of a disjoint union to the domain of the first function. (Contributed by Thierry Arnoux, 9-Dec-2021)