theorem Th5: :: NOMIN_8:5

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