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