len M = n by MATRIX_1:25;
then A1: len (- M) = n by MATRIX_3:def 2;
width M = n by MATRIX_1:25;
then width (- M) = n by MATRIX_3:def 2;
hence - M is Matrix of n, REAL by A1, MATRIX_2:7; :: thesis: verum