theorem :: RLVECT_1:39

for a being Real
for V being RealLinearSpace
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)