theorem :: MATRIX_5:26

for i, j being Nat
for M1, M2 being Matrix of COMPLEX st len M2 > 0 holds
ex s being FinSequence of COMPLEX st
( len s = len M2 & s . 1 = (M1 * (i,1)) * (M2 * (1,j)) & ( for k being Nat st 1 <= k & k < len M2 holds
s . (k + 1) = (s . k) + ((M1 * (i,(k + 1))) * (M2 * ((k + 1),j))) ) )