let D be non empty set ; for f1, f2, f3, f4, f5, f6, f7, f8, f9, f10 being BinominativeFunction of D
for p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11 being PartialPredicate of D st <*p1,f1,p2*> is SFHT of D & <*p2,f2,p3*> is SFHT of D & <*p3,f3,p4*> is SFHT of D & <*p4,f4,p5*> is SFHT of D & <*p5,f5,p6*> is SFHT of D & <*p6,f6,p7*> is SFHT of D & <*p7,f7,p8*> is SFHT of D & <*p8,f8,p9*> is SFHT of D & <*p9,f9,p10*> is SFHT of D & <*p10,f10,p11*> is SFHT of D & <*(PP_inversion p2),f2,p3*> is SFHT of D & <*(PP_inversion p3),f3,p4*> is SFHT of D & <*(PP_inversion p4),f4,p5*> is SFHT of D & <*(PP_inversion p5),f5,p6*> is SFHT of D & <*(PP_inversion p6),f6,p7*> is SFHT of D & <*(PP_inversion p7),f7,p8*> is SFHT of D & <*(PP_inversion p8),f8,p9*> is SFHT of D & <*(PP_inversion p9),f9,p10*> is SFHT of D & <*(PP_inversion p10),f10,p11*> is SFHT of D holds
<*p1,(PP_composition (f1,f2,f3,f4,f5,f6,f7,f8,f9,f10)),p11*> is SFHT of D
let f1, f2, f3, f4, f5, f6, f7, f8, f9, f10 be BinominativeFunction of D; for p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11 being PartialPredicate of D st <*p1,f1,p2*> is SFHT of D & <*p2,f2,p3*> is SFHT of D & <*p3,f3,p4*> is SFHT of D & <*p4,f4,p5*> is SFHT of D & <*p5,f5,p6*> is SFHT of D & <*p6,f6,p7*> is SFHT of D & <*p7,f7,p8*> is SFHT of D & <*p8,f8,p9*> is SFHT of D & <*p9,f9,p10*> is SFHT of D & <*p10,f10,p11*> is SFHT of D & <*(PP_inversion p2),f2,p3*> is SFHT of D & <*(PP_inversion p3),f3,p4*> is SFHT of D & <*(PP_inversion p4),f4,p5*> is SFHT of D & <*(PP_inversion p5),f5,p6*> is SFHT of D & <*(PP_inversion p6),f6,p7*> is SFHT of D & <*(PP_inversion p7),f7,p8*> is SFHT of D & <*(PP_inversion p8),f8,p9*> is SFHT of D & <*(PP_inversion p9),f9,p10*> is SFHT of D & <*(PP_inversion p10),f10,p11*> is SFHT of D holds
<*p1,(PP_composition (f1,f2,f3,f4,f5,f6,f7,f8,f9,f10)),p11*> is SFHT of D
let p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11 be PartialPredicate of D; ( <*p1,f1,p2*> is SFHT of D & <*p2,f2,p3*> is SFHT of D & <*p3,f3,p4*> is SFHT of D & <*p4,f4,p5*> is SFHT of D & <*p5,f5,p6*> is SFHT of D & <*p6,f6,p7*> is SFHT of D & <*p7,f7,p8*> is SFHT of D & <*p8,f8,p9*> is SFHT of D & <*p9,f9,p10*> is SFHT of D & <*p10,f10,p11*> is SFHT of D & <*(PP_inversion p2),f2,p3*> is SFHT of D & <*(PP_inversion p3),f3,p4*> is SFHT of D & <*(PP_inversion p4),f4,p5*> is SFHT of D & <*(PP_inversion p5),f5,p6*> is SFHT of D & <*(PP_inversion p6),f6,p7*> is SFHT of D & <*(PP_inversion p7),f7,p8*> is SFHT of D & <*(PP_inversion p8),f8,p9*> is SFHT of D & <*(PP_inversion p9),f9,p10*> is SFHT of D & <*(PP_inversion p10),f10,p11*> is SFHT of D implies <*p1,(PP_composition (f1,f2,f3,f4,f5,f6,f7,f8,f9,f10)),p11*> is SFHT of D )
assume that
A1:
<*p1,f1,p2*> is SFHT of D
and
A2:
<*p2,f2,p3*> is SFHT of D
and
A3:
<*p3,f3,p4*> is SFHT of D
and
A4:
<*p4,f4,p5*> is SFHT of D
and
A5:
<*p5,f5,p6*> is SFHT of D
and
A6:
<*p6,f6,p7*> is SFHT of D
and
A7:
<*p7,f7,p8*> is SFHT of D
and
A8:
<*p8,f8,p9*> is SFHT of D
and
A9:
<*p9,f9,p10*> is SFHT of D
and
A10:
<*p10,f10,p11*> is SFHT of D
and
A11:
<*(PP_inversion p2),f2,p3*> is SFHT of D
and
A12:
<*(PP_inversion p3),f3,p4*> is SFHT of D
and
A13:
<*(PP_inversion p4),f4,p5*> is SFHT of D
and
A14:
<*(PP_inversion p5),f5,p6*> is SFHT of D
and
A15:
<*(PP_inversion p6),f6,p7*> is SFHT of D
and
A16:
<*(PP_inversion p7),f7,p8*> is SFHT of D
and
A17:
<*(PP_inversion p8),f8,p9*> is SFHT of D
and
A18:
<*(PP_inversion p9),f9,p10*> is SFHT of D
and
A19:
<*(PP_inversion p10),f10,p11*> is SFHT of D
; <*p1,(PP_composition (f1,f2,f3,f4,f5,f6,f7,f8,f9,f10)),p11*> is SFHT of D
<*p1,(PP_composition (f1,f2,f3,f4,f5,f6,f7,f8,f9)),p10*> is SFHT of D
by A1, A2, A3, A4, A5, A6, A7, A11, A12, A13, A14, A15, A16, A8, A17, A9, A18, Th3;
hence
<*p1,(PP_composition (f1,f2,f3,f4,f5,f6,f7,f8,f9,f10)),p11*> is SFHT of D
by A10, A19, NOMIN_3:25; verum