let n be Element of NAT ; :: thesis: for A, B being Matrix of n, REAL holds
( len (A * B) = len A & width (A * B) = width B & len (A * B) = n & width (A * B) = n )
let A, B be Matrix of n, REAL ; :: thesis: ( len (A * B) = len A & width (A * B) = width B & len (A * B) = n & width (A * B) = n )
A1: len B = n by MATRIX_1:26;
A2: len A = n by MATRIX_1:26;

per cases ( n > 0 or n <= 0 ) ;

suppose A3: n > 0 ; :: thesis: ( len (A * B) = len A & width (A * B) = width B & len (A * B) = n & width (A * B) = n )

then width (MXR2MXF A) = n by MATRIX_1:24
.= len (MXR2MXF B) by MATRIX_1:26 ;
then ( len (A * B) = len A & width (A * B) = width B ) by MATRIX_3:def 4;
hence ( len (A * B) = len A & width (A * B) = width B & len (A * B) = n & width (A * B) = n ) by A1, A3, MATRIX_1:20, MATRIX_1:26; :: thesis: verum

end;

suppose A4: n <= 0 ; :: thesis: ( len (A * B) = len A & width (A * B) = width B & len (A * B) = n & width (A * B) = n )

then A5: width (MXR2MXF A) = 0 by A2, MATRIX_1:def 4
.= len (MXR2MXF B) by A4, MATRIX_1:26 ;
then len (A * B) = len A by MATRIX_3:def 4;
hence ( len (A * B) = len A & width (A * B) = width B & len (A * B) = n & width (A * B) = n ) by A2, A4, A5, MATRIX_1:def 4, MATRIX_3:def 4; :: thesis: verum

end;

end;