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