:: deftheorem Def13 defines PPIF PARTPR_2:def 11 :
for D being non empty set
for b₂ being Function of [:(Pr D),(FPrg D),(FPrg D):],(FPrg D) holds
( b₂ = PPIF D iff for p being PartialPredicate of D
for f, g being BinominativeFunction of D holds
( dom (b₂ . (p,f,g)) = { d where d is Element of D : ( ( d in dom p & p . d = TRUE & d in dom f ) or ( d in dom p & p . d = FALSE & d in dom g ) ) } & ( for d being object holds
( ( d in dom p & p . d = TRUE & d in dom f implies (b₂ . (p,f,g)) . d = f . d ) & ( d in dom p & p . d = FALSE & d in dom g implies (b₂ . (p,f,g)) . d = g . d ) ) ) ) );