A1: ( len M = n & len (a * M) = len M ) by MATRIX_1:def 3, MATRIX_3:def 5;

per cases ( n = 0 or n > 0 ) ;

suppose A2: n = 0 ; :: thesis: a * M is Matrix of n,m,K

then a * M = {} by A1;
hence a * M is Matrix of n,m,K by A2, MATRIX_1:13; :: thesis: verum

end;

suppose n > 0 ; :: thesis: a * M is Matrix of n,m,K

then ( width M = m & width (a * M) = width M ) by MATRIX_1:24, MATRIX_3:def 5;
hence a * M is Matrix of n,m,K by A1, MATRIX_2:7; :: thesis: verum

end;

end;