for D being non empty set
for f1, f2, f3, f4, f5, f6, f7, f8 being BinominativeFunction of D
for p1, p2 being PartialPredicate of D
for q1, q2, q3, q4, q5, q6, q7 being total PartialPredicate of D st <*p1,f1,q1*> is SFHT of D & <*q1,f2,q2*> is SFHT of D & <*q2,f3,q3*> is SFHT of D & <*q3,f4,q4*> is SFHT of D & <*q4,f5,q5*> is SFHT of D & <*q5,f6,q6*> is SFHT of D & <*q6,f7,q7*> is SFHT of D & <*q7,f8,p2*> is SFHT of D holds
<*p1,(PP_composition (f1,f2,f3,f4,f5,f6,f7,f8)),p2*> is SFHT of D