theorem Th3:
for
D being non
empty set for
f1,
f2,
f3,
f4,
f5,
f6 being
BinominativeFunction of
D for
p1,
p2,
p3,
p4,
p5,
p6,
p7 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 &
<*(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 holds
<*p1,(PP_composition (f1,f2,f3,f4,f5,f6)),p7*> is
SFHT of
D