for V being non empty Abelian add-associative right_zeroed addLoopStr
for F, G being FinSequence of V st rng F = rng G & F is one-to-one & G is one-to-one holds
Sum F = Sum G