theorem Th4: :: RLVECT_2:4

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