theorem :: MATRLIN2:12

for K being Field
for V1 being finite-dimensional VectSp of K
for v1 being Element of V1
for p being FinSequence of K holds Sum (lmlt (p,((len p) |-> v1))) = (Sum p) * v1