A1: width (a * M) = width M by MATRIXR1:27;
( width M = n & len (a * M) = len M ) by MATRIXR1:27, MATRIX_1:24;
hence a * M is Matrix of n, REAL by A1, MATRIX_1:24, MATRIX_2:7; :: thesis: verum