:: deftheorem defines - MATRIX_4:def 1 :
for K being Field
for M1, M2 being Matrix of K holds M1 - M2 = M1 + (- M2);