theorem :: MATRIX_4:5
for K being Ring
for M1, M2 being Matrix of K holds M1 - (- M2) = M1 + M2 by Th1;