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