for V being Z_Module
for F being FinSequence of V st F is one-to-one holds
for L being Linear_Combination of V st Carrier L c= rng F holds
Sum (L (#) F) = Sum L