theorem Th18: :: MATRIXC1:19

for i, j being Nat
for R1, R2 being Element of i -tuples_on COMPLEX holds (mlt (R1,R2)) . j = (R1 . j) * (R2 . j)