A1: len M = n by MATRIX_0:def 2;
A2: len (a * M) = len M by MATRIX_3:def 5;

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

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

then a * M = {} by A2, MATRIX_0:def 2;
hence a * M is Matrix of n,m,K by A3, MATRIX_0:13; :: thesis: verum

end;

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

A5: width (a * M) = width M by MATRIX_3:def 5;
width M = m by A4, MATRIX_0:23;
hence a * M is Matrix of n,m,K by A1, A2, A5, MATRIX_0:51; :: thesis: verum

end;

end;