theorem Th6:
for
D being non
empty set for
f1,
f2,
f3 being
BinominativeFunction of
D for
p1,
p2 being
PartialPredicate of
D for
q1,
q2 being
total PartialPredicate of
D st
<*p1,f1,q1*> is
SFHT of
D &
<*q1,f2,q2*> is
SFHT of
D &
<*q2,f3,p2*> is
SFHT of
D holds
<*p1,(PP_composition (f1,f2,f3)),p2*> is
SFHT of
D