for V being non empty add-associative right_zeroed addLoopStr
for F, G being FinSequence of V holds Sum (F ^ G) = (Sum F) + (Sum G)