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