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