for x being object
for D being set
for p being PartialPredicate of D
for f being BinominativeFunction of D st x in dom (PP_prediction (f,p)) holds
( x in dom (p * f) & ( (p * f) . x = TRUE or (p * f) . x = FALSE ) )