for L being non empty right_complementable add-associative right_zeroed left_zeroed doubleLoopStr
for m being Element of NAT
for s being FinSequence of L st len s = m & ( for k being Element of NAT st 1 <= k & k <= m holds
s /. k = 1. L ) holds
Sum s = m * (1. L)