A1: ( len M1 = n & len M2 = k ) by MATRIX_1:def 3;
then ( width M1 = k & width M2 = m ) by MATRIX_1:20;
then ( len (M1 * M2) = n & width (M1 * M2) = m ) by A1, Th42;
hence M1 * M2 is Matrix of n,m, REAL by MATRIX_2:7; :: thesis: verum