theorem :: MATRIX_8:61

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