width A = len B by MATRIX_0:25;
then ( len (A * B) = len A & width (A * B) = width B ) by Def4;
hence A * B is Matrix of len A, width B,K by MATRIX_0:51; :: thesis: verum