theorem Th7: :: MATRIX15:7

for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for p being FinSequence of K
for i, j being Nat st i in dom p & j in dom p & i <> j & ( for k being Nat st k in dom p & k <> i & k <> j holds
p . k = 0. K ) holds
Sum p = (p /. i) + (p /. j)