theorem :: NOMIN_8:14

for D being non empty set
for fD being PFuncs (b₁,b₁) -valued FinSequence
for fB being PFuncs (b₁,BOOLEAN) -valued FinSequence st fD,fB are_composable holds
<*(fB . 1),(PP_composition fD),(fB . (len fB))*> is SFHT of D