TH2:
for GF being Ring
for V being LeftMod of GF
for L being Linear_Combination of V
for C being finite Subset of V st Carrier L c= C holds
ex F being FinSequence of V st
( F is one-to-one & rng F = C & Sum L = Sum (L (#) F) )
TH3:
for GF being Ring
for V being LeftMod of GF
for L being Linear_Combination of V
for a being Scalar of holds Sum (a * L) = a * (Sum L)