theorem Th27: :: ZMATRLIN:23

for k, m, n being Nat
for V being free finite-rank Z_Module
for M1 being Matrix of n,k, the carrier of V
for M2 being Matrix of m,k, the carrier of V holds Sum (M1 ^ M2) = (Sum M1) ^ (Sum M2)