theorem Th3: :: INTEGR18:3

for X being RealNormSpace
for R1, R2 being FinSequence of X
for a being Real st R2 = a (#) R1 holds
Sum R2 = a * (Sum R1)