theorem :: MATRIX_3:35

for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being FinSequence of L st ( for i being Element of NAT st i in dom p holds
p . i = 0. L ) holds
Sum p = 0. L by Lm1;