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