( f in FPrg D & g in FPrg D ) by PARTFUN1:45;
hence (PPcomposition D) . (f,g) is BinominativeFunction of D by PARTFUN1:46, BINOP_1:17; :: thesis: verum