theorem Th12: :: MATRLIN:12

for K being Field
for V1 being finite-dimensional VectSp of K
for p2 being FinSequence of V1
for p1 being FinSequence of K st dom p1 = dom p2 holds
dom (lmlt (p1,p2)) = dom p1