:: deftheorem defines lmlt ZMATRLIN:def 6 :
for V1 being free finite-rank Z_Module
for p1 being FinSequence of INT.Ring
for p2 being FinSequence of V1 holds lmlt (p1,p2) = the lmult of V1 .: (p1,p2);