:: deftheorem defines PP_while PARTPR_2:def 16 :
for D being non empty set
for p being PartialPredicate of D
for f being BinominativeFunction of D holds PP_while (p,f) = (PPwhile D) . (p,f);