let D be non empty set ; :: thesis: for f, g being BinominativeFunction of D
for p, q, r being PartialPredicate of D st <*p,f,q*> is SFHT of D & <*q,g,r*> is SFHT of D & <*(PP_inversion q),g,r*> is SFHT of D holds
<*p,(PP_composition (f,g)),r*> is SFHT of D
let f, g be BinominativeFunction of D; :: thesis: for p, q, r being PartialPredicate of D st <*p,f,q*> is SFHT of D & <*q,g,r*> is SFHT of D & <*(PP_inversion q),g,r*> is SFHT of D holds
<*p,(PP_composition (f,g)),r*> is SFHT of D
let p, q, r be PartialPredicate of D; :: thesis: ( <*p,f,q*> is SFHT of D & <*q,g,r*> is SFHT of D & <*(PP_inversion q),g,r*> is SFHT of D implies <*p,(PP_composition (f,g)),r*> is SFHT of D )
PP_or (r,r) = r ;
hence ( <*p,f,q*> is SFHT of D & <*q,g,r*> is SFHT of D & <*(PP_inversion q),g,r*> is SFHT of D implies <*p,(PP_composition (f,g)),r*> is SFHT of D ) by Th24; :: thesis: verum