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