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