:: deftheorem defines are_composable NOMIN_8:def 7 :
for D being non empty set
for fD being PFuncs (b₁,b₁) -valued FinSequence
for fB being PFuncs (b₁,BOOLEAN) -valued FinSequence holds
( fD,fB are_composable iff ( 1 <= len fD & len fB = (len fD) + 1 & ( for n being Nat st 1 <= n & n <= len fD holds
<*(fB . n),(fD . n),(fB . (n + 1))*> is SFHT of D ) & ( for n being Nat st 2 <= n & n <= len fD holds
<*(PP_inversion (fB . n)),(fD . n),(fB . (n + 1))*> is SFHT of D ) ) );