for L being non empty right_complementable add-associative right_zeroed addLoopStr
for r being FinSequence of L st len r >= 2 & ( for k being Element of NAT st 2 < k & k in dom r holds
r . k = 0. L ) holds
Sum r = (r /. 1) + (r /. 2)