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