theorem :: MATRIXR2:4

for n being Nat
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 )