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