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