theorem Th40: :: MATRIXC1:42

for i being Nat
for F being FinSequence of COMPLEX
for M being Matrix of COMPLEX st len F = width M holds
mlt (F,((Line ((M *'),i)) *')) = (mlt ((Line ((M *'),i)),(F *'))) *'