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