len (a * M) = len M by MATRIX_3:def 5;
hence a * M is Matrix of n,m,K ; :: thesis: verum