theorem :: MATRLIN2:10

for K being Field
for V1 being finite-dimensional VectSp of K
for R1, R2 being FinSequence of V1 st len R1 = len R2 holds
Sum (R1 + R2) = (Sum R1) + (Sum R2)