theorem Th39: :: MATRPROB:39

for M, M1, M2 being Matrix of REAL st width M1 = len M2 holds
( M = M1 * M2 iff ( len M = len M1 & width M = width M2 & ( for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = (Line (M1,i)) "*" (Col (M2,j)) ) ) )