A1: width (a * M) = width M by MATRIX_3:def 5;
A2: len M = n by MATRIX_0:def 2;
A3: len (a * M) = len M by MATRIX_3:def 5;
A4: len M = n by MATRIX_0:def 2;
now :: thesis: ( ( len M > 0 & a * M is Matrix of n,K ) or ( len M <= 0 & a * M is Matrix of n,K ) )
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_0:20;
hence a * M is Matrix of n,K by A2, A3, A1, A5, MATRIX_0: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 object 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_0:def 2; :: thesis: verum
end;
end;
end;
hence a * M is Matrix of n,K ; :: thesis: verum