for V being ComplexLinearSpace
for L being C_Linear_Combination of V
for v being VECTOR of V st Carrier L = {v} holds
Sum L = (L . v) * v