theorem Th2:
for
D being non
empty set for
f1,
f2,
f3,
f4,
f5,
f6,
f7,
f8 being
BinominativeFunction of
D for
p1,
p2,
p3,
p4,
p5,
p6,
p7,
p8,
p9 being
PartialPredicate of
D st
<*p1,f1,p2*> is
SFHT of
D &
<*p2,f2,p3*> is
SFHT of
D &
<*p3,f3,p4*> is
SFHT of
D &
<*p4,f4,p5*> is
SFHT of
D &
<*p5,f5,p6*> is
SFHT of
D &
<*p6,f6,p7*> is
SFHT of
D &
<*p7,f7,p8*> is
SFHT of
D &
<*p8,f8,p9*> is
SFHT of
D &
<*(PP_inversion p2),f2,p3*> is
SFHT of
D &
<*(PP_inversion p3),f3,p4*> is
SFHT of
D &
<*(PP_inversion p4),f4,p5*> is
SFHT of
D &
<*(PP_inversion p5),f5,p6*> is
SFHT of
D &
<*(PP_inversion p6),f6,p7*> is
SFHT of
D &
<*(PP_inversion p7),f7,p8*> is
SFHT of
D &
<*(PP_inversion p8),f8,p9*> is
SFHT of
D holds
<*p1,(PP_composition (f1,f2,f3,f4,f5,f6,f7,f8)),p9*> is
SFHT of
D