theorem :: MATRIXR2:60

for k, n, m being Nat
for B being Matrix of n,m,REAL
for A being Matrix of m,k,REAL st n > 0 holds
for i, j being Nat st [i,j] in Indices (B * A) holds
(B * A) * (i,j) = ((Line (B,i)) * A) . j