for k, m, n being Nat
for K being Field
for V being VectSp of K
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)