:: deftheorem defines mlt MATRIXC1:def 5 :
for F1, F2 being FinSequence of COMPLEX holds mlt (F1,F2) = multcomplex .: (F1,F2);