let n be 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_0:25;
A2: len A = n by MATRIX_0:25;
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_0:23
.= len (MXR2MXF B) by MATRIX_0:25 ;
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_0:20, MATRIX_0:25; :: 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_0:def 3
.= len (MXR2MXF B) by A4, MATRIX_0:25 ;
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_0:def 3, MATRIX_3:def 4; :: thesis: verum
end;
end;