theorem :: MATRLIN2:8

for K being Field
for V1 being finite-dimensional VectSp of K
for R1, R2 being FinSequence of V1
for p being FinSequence of K holds lmlt (p,(R1 + R2)) = (lmlt (p,R1)) + (lmlt (p,R2))