theorem Th17: :: MATRIXC1:18

for F1, F2 being FinSequence of COMPLEX
for i being Nat st i in dom (mlt (F1,F2)) holds
(mlt (F1,F2)) . i = (F1 . i) * (F2 . i)