for R being Ring
for a being Element of R
for V being LeftMod of R
for F, G being FinSequence of V st len F = len G & ( for k being Nat
for v being Vector of V st k in dom F & v = G . k holds
F . k = a * v ) holds
Sum F = a * (Sum G)