( width M1 = n & len M2 = n ) by MATRIX_1:24;
then A1: ( len (M1 * M2) = len M1 & width (M1 * M2) = width M2 ) by MATRIX_3:def 4;
width M2 = n by MATRIX_1:24;
hence M1 * M2 is Matrix of n,K by A1, MATRIX_1:24, MATRIX_2:7; :: thesis: verum