theorem Th59: :: MATRIX_8:59
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K holds Trace (M1 - M2) = (Trace M1) - (Trace M2)