theorem Th10: :: ZMATRLIN:12

for V1 being free finite-rank Z_Module
for a being Element of V1
for F being FinSequence of INT.Ring
for G being FinSequence of V1 st len F = len G & ( for k being Nat st k in dom F holds
G . k = (F /. k) * a ) holds
Sum G = (Sum F) * a