:: deftheorem defines - FVSUM_1:def 4 :
for K being non empty addLoopStr
for p being FinSequence of the carrier of K holds - p = (comp K) * p;