A1: ( len A = n & width B = n ) by MATRIX_1:25, MATRIX_1:def 3;
( len (A * B) = len A & width (A * B) = width B ) by Th4;
hence A * B is Matrix of n, REAL by A1, MATRIX_2:7; :: thesis: verum