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