theorem :: MATRLIN2:13

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