len M1 = n
by MATRIX_0:24;

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

width M1 = n by MATRIX_0:24;

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

hence - M1 is n,n -size by A1, MATRIX_0:51; :: thesis: verum

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

width M1 = n by MATRIX_0:24;

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

hence - M1 is n,n -size by A1, MATRIX_0:51; :: thesis: verum