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