theorem Th12: :: MATRIX_3:12

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