( p in Pr D & q in Pr D ) by PARTFUN1:45;
hence (PPdisjunction D) . (p,q) is PartialPredicate of D by PARTFUN1:46, BINOP_1:17; :: thesis: verum