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