for Y being RealNormSpace
for E being Point of Y
for q being FinSequence of REAL
for S being FinSequence of Y st len S = len q & ( for i being Nat st i in dom S holds
ex r being Real st
( r = q . i & S . i = r * E ) ) holds
Sum S = (Sum q) * E