A1: width (a * M) = width M by MATRIX_3:def 5;
A2: len M = n by MATRIX_1:def 2;
A3: len (a * M) = len M by MATRIX_3:def 5;
A4: len M = n by MATRIX_1:def 2;

now

per cases ( len M > 0 or len M <= 0 ) ;

case A5: len M > 0 ; :: thesis: a * M is Matrix of n,K

then n = width M by A2, MATRIX_1:20;
hence a * M is Matrix of n,K by A2, A3, A1, A5, MATRIX_1:20; :: thesis: verum

end;

case len M <= 0 ; :: thesis: a * M is Matrix of n,K

then A6: len (a * M) = 0 by MATRIX_3:def 5;
then A7: Seg (len (a * M)) = {} ;
for p being FinSequence of K st p in rng (a * M) holds
len p = 0

proof

let p be FinSequence of K; :: thesis: ( p in rng (a * M) implies len p = 0 )
assume p in rng (a * M) ; :: thesis: len p = 0
then ex x being set st
( x in dom (a * M) & p = (a * M) . x ) by FUNCT_1:def 3;
hence len p = 0 by A7, FINSEQ_1:def 3; :: thesis: verum

end;

hence a * M is Matrix of n,K by A4, A3, A6, MATRIX_1:def 2; :: thesis: verum

end;

end;

end;

hence a * M is Matrix of n,K ; :: thesis: verum