let D be non empty set ; :: thesis: for f1, f2, f3, f4, f5 being BinominativeFunction of D
for p1, p2 being PartialPredicate of D
for q1, q2, q3, q4 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,p2*> is SFHT of D holds
<*p1,(PP_composition (f1,f2,f3,f4,f5)),p2*> is SFHT of D
let f1, f2, f3, f4, f5 be BinominativeFunction of D; :: thesis: for p1, p2 being PartialPredicate of D
for q1, q2, q3, q4 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,p2*> is SFHT of D holds
<*p1,(PP_composition (f1,f2,f3,f4,f5)),p2*> is SFHT of D
let p1, p2 be PartialPredicate of D; :: thesis: for q1, q2, q3, q4 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,p2*> is SFHT of D holds
<*p1,(PP_composition (f1,f2,f3,f4,f5)),p2*> is SFHT of D
let q1, q2, q3, q4 be total PartialPredicate of D; :: thesis: ( <*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,p2*> is SFHT of D implies <*p1,(PP_composition (f1,f2,f3,f4,f5)),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 ) and
A2: <*q4,f5,p2*> is SFHT of D ; :: thesis: <*p1,(PP_composition (f1,f2,f3,f4,f5)),p2*> is SFHT of D
A3: <*(PP_inversion q4),f5,p2*> is SFHT of D by NOMIN_3:19;
<*p1,(PP_composition (f1,f2,f3,f4)),q4*> is SFHT of D by A1, Th7;
hence <*p1,(PP_composition (f1,f2,f3,f4,f5)),p2*> is SFHT of D by A2, A3, NOMIN_3:25; :: thesis: verum