theorem :: RLVECT_X:1

for X being RealLinearSpace
for R1, R2 being FinSequence of X st len R1 = len R2 holds
Sum (R1 + R2) = (Sum R1) + (Sum R2)