for n, m, k being Nat
for M1 being Matrix of n,k,ExtREAL
for M2 being Matrix of m,k,ExtREAL holds Sum (M1 ^ M2) = (Sum M1) ^ (Sum M2)