theorem :: MATRLIN2:11

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