for R being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr
for a being Element of R
for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over R
for F, G being FinSequence of V st len F = len G & ( for k being Nat
for v being Element of V st k in dom F & v = G . k holds
F . k = a * v ) holds
Sum F = a * (Sum G)