for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being FinSequence of L
for n being Element of NAT st ( for k being Element of NAT st k in dom p & k > n holds
p . k = 0. L ) holds
Sum p = Sum (p | n)