theorem Th11: :: MATRIX_3:11

for n being Nat
for K being non empty right_complementable add-associative right_zeroed addLoopStr holds Sum (n |-> (0. K)) = 0. K