theorem :: NOMIN_5:1

for D being non empty set
for f1, f2, f3 being BinominativeFunction of D
for p, q, r, w being PartialPredicate of D st <*p,f1,q*> is SFHT of D & <*q,f2,r*> is SFHT of D & <*r,f3,w*> is SFHT of D & <*(PP_inversion q),f2,r*> is SFHT of D & <*(PP_inversion r),f3,w*> is SFHT of D holds
<*p,(PP_composition (f1,f2,f3)),w*> is SFHT of D