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;