theorem Th29: :: ZMATRLIN:24

for V1 being free finite-rank Z_Module
for M1, M2 being Matrix of the carrier of V1 holds (Sum M1) + (Sum M2) = Sum (M1 ^^ M2)