( width M1 = n & len M2 = n )
by MATRIX_0:24;

then A1: ( len (M1 * M2) = len M1 & width (M1 * M2) = width M2 ) by MATRIX_3:def 4;

width M2 = n by MATRIX_0:24;

hence M1 * M2 is n,n -size by A1, MATRIX_0:24, MATRIX_0:51; :: thesis: verum

then A1: ( len (M1 * M2) = len M1 & width (M1 * M2) = width M2 ) by MATRIX_3:def 4;

width M2 = n by MATRIX_0:24;

hence M1 * M2 is n,n -size by A1, MATRIX_0:24, MATRIX_0:51; :: thesis: verum