let D be 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
let f1, f2, f3, f4, f5 be 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
let p, q, r, t, w, u be PartialPredicate of D; ( <*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 implies <*p,(PP_composition (f1,f2,f3,f4,f5)),u*> is SFHT of D )
assume that
A1:
<*p,f1,q*> is SFHT of D
and
A2:
<*q,f2,r*> is SFHT of D
and
A3:
<*r,f3,w*> is SFHT of D
and
A4:
<*w,f4,t*> is SFHT of D
and
A5:
<*t,f5,u*> is SFHT of D
and
A6:
<*(PP_inversion q),f2,r*> is SFHT of D
and
A7:
<*(PP_inversion r),f3,w*> is SFHT of D
and
A8:
<*(PP_inversion w),f4,t*> is SFHT of D
and
A9:
<*(PP_inversion t),f5,u*> is SFHT of D
; <*p,(PP_composition (f1,f2,f3,f4,f5)),u*> is SFHT of D
<*p,(PP_composition (f1,f2)),r*> is SFHT of D
by A1, A2, A6, NOMIN_3:25;
then
<*p,(PP_composition ((PP_composition (f1,f2)),f3)),w*> is SFHT of D
by A3, A7, NOMIN_3:25;
then
<*p,(PP_composition ((PP_composition (f1,f2,f3)),f4)),t*> is SFHT of D
by A4, A8, NOMIN_3:25;
hence
<*p,(PP_composition (f1,f2,f3,f4,f5)),u*> is SFHT of D
by A5, A9, NOMIN_3:25; verum