theorem Th20: :: ZMATRLIN:20

for V1 being free finite-rank Z_Module
for F being FinSequence of V1
for KL being Linear_Combination of V1 st F is one-to-one & Carrier KL c= rng F holds
Sum (KL (#) F) = Sum KL