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