:: deftheorem defines lmlt MATRLIN:def 5 :
for K being Field
for V1 being finite-dimensional VectSp of K
for p1 being FinSequence of K
for p2 being FinSequence of V1 holds lmlt (p1,p2) = the lmult of V1 .: (p1,p2);