dom f = X by Z1, Def1;
then dom (p * f) = X by Z, RELAT_1:46;
then p * f is total by PARTFUN1:def 4;
hence p * f is Function of X,Z ; :: thesis: verum