theorem :: ZMODUL01:17

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 st k in dom F holds
G . k = a * (F /. k) ) holds
Sum G = a * (Sum F)