theorem Th5: :: ZMODUL03:5

for V being Z_Module
for L being Linear_Combination of V
for F, G being FinSequence of V
for P being Permutation of (dom F) st G = F * P holds
Sum (L (#) F) = Sum (L (#) G)