:: deftheorem Def5 defines PP_compositionSeq NOMIN_8:def 5 :
for D being non empty set
for fD being PFuncs (b₁,b₁) -valued FinSequence st 0 < len fD holds
for b₃ being FinSequence of PFuncs (D,D) holds
( b₃ = PP_compositionSeq fD iff ( len b₃ = len fD & b₃ . 1 = fD . 1 & ( for n being Nat st 1 <= n & n < len fD holds
b₃ . (n + 1) = PP_composition ((b₃ . n),(fD . (n + 1))) ) ) );