let D be non empty set ; :: thesis: for f1, f2, f3, f4, f5, f6, f7 being BinominativeFunction of D
for p1, p2, p3, p4, p5, p6, p7, p8 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 & <*(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 holds
<*p1,(PP_composition (f1,f2,f3,f4,f5,f6,f7)),p8*> is SFHT of D
let f1, f2, f3, f4, f5, f6, f7 be BinominativeFunction of D; :: thesis: for p1, p2, p3, p4, p5, p6, p7, p8 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 & <*(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 holds
<*p1,(PP_composition (f1,f2,f3,f4,f5,f6,f7)),p8*> is SFHT of D
let p1, p2, p3, p4, p5, p6, p7, p8 be PartialPredicate of D; :: thesis: ( <*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 & <*(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 implies <*p1,(PP_composition (f1,f2,f3,f4,f5,f6,f7)),p8*> 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: <*(PP_inversion p2),f2,p3*> is SFHT of D and
A9: <*(PP_inversion p3),f3,p4*> is SFHT of D and
A10: <*(PP_inversion p4),f4,p5*> is SFHT of D and
A11: <*(PP_inversion p5),f5,p6*> is SFHT of D and
A12: <*(PP_inversion p6),f6,p7*> is SFHT of D and
A13: <*(PP_inversion p7),f7,p8*> is SFHT of D ; :: thesis: <*p1,(PP_composition (f1,f2,f3,f4,f5,f6,f7)),p8*> is SFHT of D
<*p1,(PP_composition (f1,f2,f3,f4,f5,f6)),p7*> is SFHT of D by A1, A2, A3, A4, A5, A6, A8, A9, A10, A11, A12, NOMIN_7:3;
hence <*p1,(PP_composition (f1,f2,f3,f4,f5,f6,f7)),p8*> is SFHT of D by A7, A13, NOMIN_3:25; :: thesis: verum