len (M1 + (- M2)) = len M1 by MATRIX_3:def 3;
hence M1 - M2 is Matrix of n, REAL by MATRIX_4:def 1; :: thesis: verum