theorem Th25: :: MATRPROB:25

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