for V being non empty right_complementable add-associative right_zeroed addLoopStr
for F being FinSequence of V st len F = 1 holds
Sum F = F . 1