theorem Th53: :: MATRIX_8:53
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K holds Trace (M1 + M2) = (Trace M1) + (Trace M2)