theorem Th24: :: ZMODUL05:35

for V being Z_Module
for l being Linear_Combination of V holds l = l ! (Carrier l)