len M = n
by MATRIX_0:24;

then A1: len (- M) = n by MATRIX_3:def 2;

width M = n by MATRIX_0:24;

then width (- M) = n by MATRIX_3:def 2;

hence - M is Matrix of n,REAL by A1, MATRIX_0:51; :: thesis: verum

then A1: len (- M) = n by MATRIX_3:def 2;

width M = n by MATRIX_0:24;

then width (- M) = n by MATRIX_3:def 2;

hence - M is Matrix of n,REAL by A1, MATRIX_0:51; :: thesis: verum