:: deftheorem defines PP_FH PARTPR_2:def 14 :
for D being non empty set
for p, q being PartialPredicate of D
for f being BinominativeFunction of D holds PP_FH (p,f,q) = (PPFH D) . (p,f,q);