A1: len (a * M) = len M by Def5
.= m by MATRIX_0:25 ;
for p being FinSequence of the carrier of K st p in rng (a * M) holds
len p = n

proof

let p be FinSequence of the carrier of K; :: thesis: ( p in rng (a * M) implies len p = n )
assume A2: p in rng (a * M) ; :: thesis: len p = n
then consider i being object such that
A3: ( i in dom (a * M) & p = (a * M) . i ) by FUNCT_1:def 3;

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

suppose len M = 0 ; :: thesis: len p = n

then len (a * M) = 0 by Def5;
then Seg (len (a * M)) = {} ;
then dom (a * M) = {} by FINSEQ_1:def 3;
hence len p = n by A3; :: thesis: verum

end;

suppose A4: len M > 0 ; :: thesis: len p = n

then a4: len (a * M) > 0 by Def5;
len M = m by MATRIX_0:25;
then A6: len (a * M) = m by Def5;
m > 0 by A4, MATRIX_0:25;
then width M = n by MATRIX_0:23;
then width (a * M) = n by Def5;
then a * M is Matrix of m,n, the carrier of K by a4, A6, MATRIX_0:20;
then a * M is m,n -size ;
hence len p = n by A2, MATRIX_0:def 2; :: thesis: verum

end;

end;

end;

hence a * M is Matrix of m,n,K by A1, MATRIX_0:def 2; :: thesis: verum