let D be non empty set ; for f1, f2, f3, f4, f5, f6, f7, f8, f9, f10 being BinominativeFunction of D
for p1, p2 being PartialPredicate of D
for q1, q2, q3, q4, q5, q6, q7, q8, q9 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,q4*> is SFHT of D & <*q4,f5,q5*> is SFHT of D & <*q5,f6,q6*> is SFHT of D & <*q6,f7,q7*> is SFHT of D & <*q7,f8,q8*> is SFHT of D & <*q8,f9,q9*> is SFHT of D & <*q9,f10,p2*> is SFHT of D holds
<*p1,(PP_composition (f1,f2,f3,f4,f5,f6,f7,f8,f9,f10)),p2*> is SFHT of D
let f1, f2, f3, f4, f5, f6, f7, f8, f9, f10 be BinominativeFunction of D; for p1, p2 being PartialPredicate of D
for q1, q2, q3, q4, q5, q6, q7, q8, q9 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,q4*> is SFHT of D & <*q4,f5,q5*> is SFHT of D & <*q5,f6,q6*> is SFHT of D & <*q6,f7,q7*> is SFHT of D & <*q7,f8,q8*> is SFHT of D & <*q8,f9,q9*> is SFHT of D & <*q9,f10,p2*> is SFHT of D holds
<*p1,(PP_composition (f1,f2,f3,f4,f5,f6,f7,f8,f9,f10)),p2*> is SFHT of D
let p1, p2 be PartialPredicate of D; for q1, q2, q3, q4, q5, q6, q7, q8, q9 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,q4*> is SFHT of D & <*q4,f5,q5*> is SFHT of D & <*q5,f6,q6*> is SFHT of D & <*q6,f7,q7*> is SFHT of D & <*q7,f8,q8*> is SFHT of D & <*q8,f9,q9*> is SFHT of D & <*q9,f10,p2*> is SFHT of D holds
<*p1,(PP_composition (f1,f2,f3,f4,f5,f6,f7,f8,f9,f10)),p2*> is SFHT of D
let q1, q2, q3, q4, q5, q6, q7, q8, q9 be total PartialPredicate of D; ( <*p1,f1,q1*> is SFHT of D & <*q1,f2,q2*> is SFHT of D & <*q2,f3,q3*> is SFHT of D & <*q3,f4,q4*> is SFHT of D & <*q4,f5,q5*> is SFHT of D & <*q5,f6,q6*> is SFHT of D & <*q6,f7,q7*> is SFHT of D & <*q7,f8,q8*> is SFHT of D & <*q8,f9,q9*> is SFHT of D & <*q9,f10,p2*> is SFHT of D implies <*p1,(PP_composition (f1,f2,f3,f4,f5,f6,f7,f8,f9,f10)),p2*> is SFHT of D )
assume that
A1:
( <*p1,f1,q1*> is SFHT of D & <*q1,f2,q2*> is SFHT of D & <*q2,f3,q3*> is SFHT of D & <*q3,f4,q4*> is SFHT of D & <*q4,f5,q5*> is SFHT of D & <*q5,f6,q6*> is SFHT of D & <*q6,f7,q7*> is SFHT of D & <*q7,f8,q8*> is SFHT of D & <*q8,f9,q9*> is SFHT of D )
and
A2:
<*q9,f10,p2*> is SFHT of D
; <*p1,(PP_composition (f1,f2,f3,f4,f5,f6,f7,f8,f9,f10)),p2*> is SFHT of D
A3:
<*(PP_inversion q9),f10,p2*> is SFHT of D
by NOMIN_3:19;
<*p1,(PP_composition (f1,f2,f3,f4,f5,f6,f7,f8,f9)),q9*> is SFHT of D
by A1, Th12;
hence
<*p1,(PP_composition (f1,f2,f3,f4,f5,f6,f7,f8,f9,f10)),p2*> is SFHT of D
by A2, A3, NOMIN_3:25; verum