:: deftheorem defines FPrg PARTPR_2:def 2 :
for D being set holds FPrg D = PFuncs (D,D);