:: deftheorem defines PP_IF PARTPR_2:def 12 :
for D being non empty set
for p being PartialPredicate of D
for f, g being BinominativeFunction of D holds PP_IF (p,f,g) = (PPIF D) . (p,f,g);