theorem Th31: :: ZMATRLIN:26

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