:: deftheorem defines PP_composition NOMIN_8:def 6 :
for D being non empty set
for fD being PFuncs (b₁,b₁) -valued FinSequence holds PP_composition fD = (PP_compositionSeq fD) . (len (PP_compositionSeq fD));