theorem Th1:
for
D being non
empty set for
f1,
f2,
f3,
f4,
f5 being
BinominativeFunction of
D for
p,
q,
r,
t,
w,
u 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 &
<*t,f5,u*> 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 &
<*(PP_inversion t),f5,u*> is
SFHT of
D holds
<*p,(PP_composition (f1,f2,f3,f4,f5)),u*> is
SFHT of
D