theorem :: RLVECT_1:40

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