for V being free Z_Module
for a being Element of INT.Ring
for KL1, KL2 being Linear_Combination of V
for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & a <> 0. INT.Ring & Sum KL1 = a * (Sum KL2) holds
KL1 = a * KL2