( p in Pr D & f in FPrg D & g in FPrg D ) by PARTFUN1:45;
hence (PPIF D) . (p,f,g) is BinominativeFunction of D by PARTFUN1:46, Th1; :: thesis: verum