theorem Th7: :: MATRLIN2:7

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