let D be non empty set ; :: thesis: 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 & <*(),f2,r*> is SFHT of D & <*(),f3,w*> is SFHT of D holds
<*p,(PP_composition (f1,f2,f3)),w*> is SFHT of D

let f1, f2, f3 be BinominativeFunction of D; :: thesis: 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 & <*(),f2,r*> is SFHT of D & <*(),f3,w*> is SFHT of D holds
<*p,(PP_composition (f1,f2,f3)),w*> is SFHT of D

let p, q, r, w be PartialPredicate of D; :: thesis: ( <*p,f1,q*> is SFHT of D & <*q,f2,r*> is SFHT of D & <*r,f3,w*> is SFHT of D & <*(),f2,r*> is SFHT of D & <*(),f3,w*> is SFHT of D implies <*p,(PP_composition (f1,f2,f3)),w*> is SFHT of D )
assume that
A1: <*p,f1,q*> is SFHT of D and
A2: <*q,f2,r*> is SFHT of D and
A3: <*r,f3,w*> is SFHT of D and
A4: <*(),f2,r*> is SFHT of D and
A5: <*(),f3,w*> is SFHT of D ; :: thesis: <*p,(PP_composition (f1,f2,f3)),w*> is SFHT of D
<*p,(PP_composition (f1,f2)),r*> is SFHT of D by ;
hence <*p,(PP_composition (f1,f2,f3)),w*> is SFHT of D by ; :: thesis: verum