for K being Field
for V1 being finite-dimensional VectSp of K
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))