A1: dom (Z --> y) = Z by FUNCOP_1:13;
rng (Z --> y) c= {y} by FUNCOP_1:13;
hence Z --> y is PartFunc of (X *),Y by A1, FINSEQ_2:90, RELSET_1:4; :: thesis: verum