theorem Th30: :: ZMATRLIN:25

for V1 being free finite-rank Z_Module
for P1, P2 being FinSequence of V1 st len P1 = len P2 holds
Sum (P1 + P2) = (Sum P1) + (Sum P2)