width A = len B by MATRIX_1: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_2:7; :: thesis: verum