theorem Th2:
for
D being non
empty set for
f1,
f2,
f3,
f4 being
BinominativeFunction of
D for
p,
q,
r,
t,
w being
PartialPredicate of
D st
<*p,f1,q*> is
SFHT of
D &
<*q,f2,r*> is
SFHT of
D &
<*r,f3,w*> is
SFHT of
D &
<*w,f4,t*> is
SFHT of
D &
<*(PP_inversion q),f2,r*> is
SFHT of
D &
<*(PP_inversion r),f3,w*> is
SFHT of
D &
<*(PP_inversion w),f4,t*> is
SFHT of
D holds
<*p,(PP_composition (f1,f2,f3,f4)),t*> is
SFHT of
D