theorem :: CLVECT_1:13

for V being ComplexLinearSpace
for z being Complex
for F, G being FinSequence of the carrier 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 = z * v ) holds
Sum F = z * (Sum G)