theorem Th1: :: INTEGR23:1

for E being Real
for q, S being FinSequence of REAL 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