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)