theorem :: MATRIX_4:3
for K being Ring
for M being Matrix of K holds M - M = 0. (K,(len M),(width M)) by Th2;