theorem Th55: :: MATRIX11:55

for K being Ring
for A, B being Matrix of K st width A = len B & len B > 0 holds
for i being Nat st i in Seg (len A) holds
ex P being FinSequence of the carrier of K * st
( len P = len B & Line ((A * B),i) = (addFinS K) "**" P & ( for j being Nat st j in Seg (len B) holds
P . j = (A * (i,j)) * (Line (B,j)) ) )