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