for D being non empty set
for f1, f2, f3 being BinominativeFunction of D
for p1, p2 being PartialPredicate of D
for q1, q2 being total PartialPredicate of D st <*p1,f1,q1*> is SFHT of D & <*q1,f2,q2*> is SFHT of D & <*q2,f3,p2*> is SFHT of D holds
<*p1,(PP_composition (f1,f2,f3)),p2*> is SFHT of D