:: deftheorem defines PP_prediction PARTPR_2:def 7 :
for D being set
for f being BinominativeFunction of D
for p being PartialPredicate of D holds PP_prediction (f,p) = (PPprediction D) . (f,p);