( p in Pr D & f in FPrg D & q in Pr D ) by PARTFUN1:45;
hence (PPFH D) . (p,f,q) is PartialPredicate of D by PARTFUN1:46, Th1; :: thesis: verum