theorem Th2: :: RLVECT_2:2

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for F, G, H being FinSequence of the carrier of V st len F = len G & len F = len H & ( for k being Nat st k in dom F holds
H . k = (F /. k) + (G /. k) ) holds
Sum H = (Sum F) + (Sum G)