theorem Th61: :: MATRIXR2:61

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