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