theorem Th9:
for
D being non
empty set for
f1,
f2,
f3,
f4,
f5,
f6 being
BinominativeFunction of
D for
p1,
p2 being
PartialPredicate of
D for
q1,
q2,
q3,
q4,
q5 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,p2*> is
SFHT of
D holds
<*p1,(PP_composition (f1,f2,f3,f4,f5,f6)),p2*> is
SFHT of
D