let D be non empty set ; :: thesis: for f1, f2 being BinominativeFunction of D
for p1, p2 being PartialPredicate of D
for q1 being total PartialPredicate of D st <*p1,f1,q1*> is SFHT of D & <*q1,f2,p2*> is SFHT of D holds
<*p1,(PP_composition (f1,f2)),p2*> is SFHT of D
let f1, f2 be BinominativeFunction of D; :: thesis: for p1, p2 being PartialPredicate of D
for q1 being total PartialPredicate of D st <*p1,f1,q1*> is SFHT of D & <*q1,f2,p2*> is SFHT of D holds
<*p1,(PP_composition (f1,f2)),p2*> is SFHT of D
let p1, p2 be PartialPredicate of D; :: thesis: for q1 being total PartialPredicate of D st <*p1,f1,q1*> is SFHT of D & <*q1,f2,p2*> is SFHT of D holds
<*p1,(PP_composition (f1,f2)),p2*> is SFHT of D
let q1 be total PartialPredicate of D; :: thesis: ( <*p1,f1,q1*> is SFHT of D & <*q1,f2,p2*> is SFHT of D implies <*p1,(PP_composition (f1,f2)),p2*> is SFHT of D )
<*(PP_inversion q1),f2,p2*> is SFHT of D by NOMIN_3:19;
hence ( <*p1,f1,q1*> is SFHT of D & <*q1,f2,p2*> is SFHT of D implies <*p1,(PP_composition (f1,f2)),p2*> is SFHT of D ) by NOMIN_3:25; :: thesis: verum