theorem Th30: :: MATRLIN:30

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