for K being non empty right_complementable add-associative right_zeroed addLoopStr
for a being Element of K
for p being FinSequence of the carrier of K holds Sum (<*a*> ^ p) = a + (Sum p)