theorem Th42: :: MATRPROB:42

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 being Nat st i in Seg (len M) holds
Line (M,i) = (Line (M1,i)) * M2 ) ) )