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