theorem Th3: :: RLVECT_X:3

for X being RealLinearSpace
for R1, R2 being FinSequence of X
for a being Element of REAL st R2 = a (#) R1 holds
Sum R2 = a * (Sum R1)