for V being Z_Module
for L being Linear_Combination of V
for F being FinSequence of V ex K being Linear_Combination of V st
( Carrier K = (rng F) /\ (Carrier L) & L (#) F = K (#) F )