for V being Z_Module
for a being Element of INT.Ring
for L being Linear_Combination of V st a <> 0. INT.Ring holds
Carrier (a * L) = Carrier L