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