for V being RealLinearSpace
for a being Real
for F, G being FinSequence of V st len F = len G & ( for k being Nat st k in dom F holds
G . k = a * (F /. k) ) holds
Sum G = a * (Sum F)