len (M1 + (- M2)) = n by MATRIX_1:24;
hence M1 - M2 is Matrix of n,K ; :: thesis: verum