p in Pr D by PARTFUN1:45;
hence (PPinversion D) . p is PartialPredicate of D by PARTFUN1:46, FUNCT_2:5; :: thesis: verum