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, COMPUT_1:10, RELSET_1:4; :: thesis: verum