theorem :: MATRIX_8:58

for n being Nat
for K being Field
for M1 being Matrix of n,K holds Trace (M1 + (- M1)) = 0. K