A1:
width (a * M) = width M
by MATRIXR1:27;

( width M = n & len (a * M) = len M ) by MATRIXR1:27, MATRIX_0:24;

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

( width M = n & len (a * M) = len M ) by MATRIXR1:27, MATRIX_0:24;

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