theorem Th12: :: ZMODUL01:12

for a being Element of INT.Ring
for V being Z_Module
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)