for V being ComplexLinearSpace
for L being C_Linear_Combination of V
for v1, v2 being VECTOR of V st Carrier L = {v1,v2} & v1 <> v2 holds
Sum L = ((L . v1) * v1) + ((L . v2) * v2)